Post #1846813
2026-04-26 16:15 UTC
@MartinEscardo @carloangiuli At your birthday meeting, I had a very long discussion with Milly about these issues... I did not come away convinced, but I think I got a bit closer to understanding her point of view.
Replies (1)
-
@jonmsterling@mathstodon.xyz 2026-04-26 16:20
@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.