Post #2652248
2026-05-11 11:37 UTC
@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!
Replies (2)
-
@jonmsterling@mathstodon.xyz 2026-05-11 11:45
@dwarn@mathstodon.xyz That's a very interesting trick...
-
@SamToth@mathstodon.xyz 2026-05-11 11:50
@dwarn@mathstodon.xyz Looks very interesting. I suspect it wouldn’t be so difficult to add a new sort to Agda that disallows dependent function types. Would this be enough to get what you need?