|
|
|
|
|
|
by lambdas
32 days ago
|
|
|
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. |
|
|