Post #1816213

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