Post #1846815
2026-04-26 16:36 UTC
@jonmsterling @MartinEscardo I find this a very perplexing requirement, especially because no fully combinatory presentation of the typing rules of dependent type theory has been developed, IIUC? (I realize you are only the messenger, just thinking aloud here...)
Replies (1)
-
@jonmsterling@mathstodon.xyz 2026-04-26 16:36
@carloangiuli @MartinEscardo Well, I asked about this, and it sounds like it is an important open question in some circles.