Further plans

[Trebor-Huang]

I'm locally famous for making projects that end up totally unrelated to their names :P

• Write up some even more elementary introduction, starting with NbE of arithmetic operations, also include a Haskell version. Hopefully this becomes more accessible.
• Package STLC up with "true" categories. This is important because currently I still did some work that should be free because I didn't prove universal properties --- It's good to see where exactly each part of the labour goes into after a categorical reformulation.
  • This requires the agda/agda-categories library to bump the agda-stdlib version up because I need to use Tactic.Cong and stuff. Or maybe not.
• Reformulate abstract binding syntax using the topos of stuff, i.e. the topos defined by the functor category [Fin, Set]. The idea is described here but I'm not particularly satisfied with their approach. This breaks down into several steps.
  • Syntaxes are like initial algebras in the [Fin, Set] category. Of course, not all endofunctors have initial algebras. But in addition to polynomial functors we need to throw in the weakening endofunctor.
  • We then endow the initial algebra (i.e. presheaf of syntax trees) with typing structures. This should lead smoothly into the initial model of type theory. If this stuff works, then we have a proper path to "ascend into objective metatheory" from raw terms.
• Put my understanding of working with dependent types in Agda. Reading about these on paper is much easier than formalizing them!
  • MLTT (without equality or cumulative universes). If I have the energy, maybe compare some categorical semantics.
  • "Objective metatheory", and the framework by Uemura.
• Hardcore maths
  • Topos. I currently see this as impossible in Agda, unless I can work full-time (and with a plentiful supply of coffee) with a team or something. But maybe I can start to write up some pen-and-paper expositions.
  • How exactly gluing works in STLC. This is already done for directed graphs. Since this is not exactly in a topos it might not work, so maybe we'll just skip to dependent type theories.
  • Manually doing strong normalization of MLTT (is this intractible?).
  • Reformulating into topos and gluing.

I really shouldn't linger now, and I need to do some real math (real a la Kevin Buzzard). So maybe after I read some basics on commutative algebra and algebraic topology and stuff, I'll come back at this.

[ice1000]

I'm locally famous for making projects that end up totally unrelated to their names :P

Disagreed, you're famous for making projects that has a Python file among a bunch of Agda files.