Post #1846814
2026-04-26 16:20 UTC
@MartinEscardo @carloangiuli One aspect that she informed me of, which I hadn't been aware of before, is that from her point of view it is very philosophically important that there be a combinatorial presentation of the type theory; this is the "justification" of defying the xi-rule. Martin-Löf also talked about this, of course, in “About models for intuitionistic type theories and the notion of definitional equality”, if I recall correctly.
Now, I do not share this goal, but I can see how starting there would lead to a lot of firm positions that seem almost unconscionable to someone who has a different starting point.
Replies (2)
-
@carloangiuli@mathstodon.xyz 2026-04-26 16:36
@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...)
-
@jeanas@mathstodon.xyz 2026-04-27 22:16
@jonmsterling What do you mean by a “combinatorial presentation of the type theory”? @MartinEscardo @carloangiuli