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.
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.