Post #1846801
2026-04-26 17:34 UTC
@jonmsterling I have always been confused about the "initiality conjecture". From https://www.youtube.com/watch?v=1ogUFFUfU_M, it seemed to me that in the form of "the term model is initial", it was proven by Streicher and Hoffman for MLTT and CC, can be extended heuristically to any reasonable type theory, but is difficult to state (nevermind prove) in a uniform fashion for all reasonable type theories at once.
It is much less clear to me what the important consequences of initiality for HoTT are, and which of those are real or imagined.
Replies (1)
-
@jonmsterling@mathstodon.xyz 2026-04-26 17:40
@zwarich Yes, you surmised correctly. I had many discussions with Peter on this over the years (at least in those days he was a true believer). There was a lot of goalpost-moving: for example, some might say "OK the annotated syntax is obviously fine as you say but what about the unannotated syntax !!!" and the answer to that is obviously "it depends, but that's not what we were originally asking". (It has very recently been proved that the unannotated syntax is also initial! But this is obviously very sensitive to what you put in there.)