3 ms·
> Rust > No HKTs > Category Theory
by pshirshov 5mo ago
> Rust
> No HKTs
> Category Theory
- lambdas 5mo agoEh. 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.
- TimorousBestie 5mo agoThat sounds really cool, do you mind dropping a link if the work is public?