Post #1846798

2026-04-26 17:05 UTC

@zwarich To my recollection, he viewed the possibly unsoundness of type theory in classical mathematics as a special case of a more general problem that he claimed was open (his "initiality conjecture"), which was also not an open problem. (And even if it was an open problem, that would not have implied that the soundness was open.) This is of course separate from the weird PA-inconsistency talk that he gave. But I guess my point is, he said a lot of weird and damaging stuff.

Replies (2)

@jonmsterling@mathstodon.xyz 2026-04-26 17:09

@zwarich After he tragically passed away, the impact of his misinformation campaign was felt for many years. I started my PhD in the year he died (or the year before?), and it was not until the very end of my PhD that I could even say out loud things like “the syntax of type theory is initial” without people jumping on me and pointing out that a Great Man of Mathematics has said otherwise, and who are we to question it?? It made it very difficult to publish papers on type theory in those days. Some people who knew better just would pay homage to his misinformation, and write things like "Our results depend on a solution to Voevodsky's Conjecture" etc., and I understand why they did it to save their own skins, but this was naturally very damaging to the field. The questions he was raising had been resolved in 1978. I'm not joking. I had to be at war for three years straight. And then all of a sudden, sometime around 2021-2022, the scales fell away and people stopped bringing that shit up. It was kind of anti-climactic for me, but I am grateful now that I can say this shit out loud without getting jumped on.

Open ##1846799
@zwarich@hachyderm.io 2026-04-26 17:34

@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.

Open ##1846801