Post #2652246
2026-05-11 11:06 UTC
@dwarn@mathstodon.xyz Pretty cool! Looking forward to digging into this.
Replies (1)
-
@jonmsterling@mathstodon.xyz 2026-05-11 11:09
@dwarn@mathstodon.xyz One quick question: I understand the point about judgemental associativity and unit laws being fine in the semantics. I also know how to implement a type checker for a system with your Cat + laws. But you also mention that you could do this in existing proof assistants. Is the idea to use some kind of 'yoneda' trick to get the judgemental laws? Or to use REWRITE in Agda?