Post #1816212
2026-02-18 15:52 UTC
I rarely formalise things, so whenever I do get to be reminded of what it's like. My takeaway this time is how amazing it is that MLTT lets us reason about path algebra completely rigorously and with sol little friction.
Replies (1)
-
@MartinEscardo@mathstodon.xyz 2026-02-24 19:30
@dwarn writes "My takeaway this time is how amazing it is that MLTT lets us reason about path algebra completely rigorously and with sol little friction." You are actually using a rather spartan MLTT. Your Agda file uses only Π-types and identity types. Nothing else. The magic is the identity type, really.