Eh. I’ve been writing a small HoTT language over the past two years based on schemes, stacks, and sites and anything short of Agda or Lean falls short in terms of Real™ Category Theory.
So much has to be pragmatised, carefully considered and made concrete categories anyway that much of the category theory exists in the documentation rather in the actual code.
Comments
Eh. I’ve been writing a small HoTT language over the past two years based on schemes, stacks, and sites and anything short of Agda or Lean falls short in terms of Real™ Category Theory.
So much has to be pragmatised, carefully considered and made concrete categories anyway that much of the category theory exists in the documentation rather in the actual code.
That sounds really cool, do you mind dropping a link if the work is public?