Post #1846755
2026-04-30 09:56 UTC
@jonmsterling I think that (with enough personpower) it should be possible in Agda to control which subtype theory of Agda one wants to work with, in particular to disable everything that is not MLTT.
Replies (1)
-
@jonmsterling@mathstodon.xyz 2026-04-30 10:00
@MartinEscardo I understand — but I don’t agree :)