Post #2652250
2026-05-11 11:50 UTC
@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?
Replies (1)
-
@dwarn@mathstodon.xyz 2026-05-11 12:00
@SamToth@mathstodon.xyz Maybe... So far I've been a bit more conservative, not allowing any kind of dependency on "category variables".