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.