Post #2652247
2026-05-11 11:09 UTC
@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?
Replies (1)
-
@dwarn@mathstodon.xyz 2026-05-11 11:37
@jonmsterling@mathstodon.xyz Rewrite rules would probably work. Currently, we are experimenting with something like Licata's trick, relying on private modules. The idea is that Cat models simple type theory, and Agda already implements type checking for simple type theory (+ a lot more). So we privately define Cat to be Type, and expose only the intended operations. Here's an implementation: https://codeberg.org/dwarn/axcat/src/branch/main/src/Cat/Base.agda To be clear, I don't know if this is robust!