Post #1846802

2026-04-26 17:40 UTC

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

Replies (2)

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

@zwarich The good thing that came out of these years of "doubt" was that general techniques emerged to replicate what Streicher and Hofmann did in much greater generality. For example, Taichi Uemura's 2021 PhD thesis gave a fully general account that applies to any second-order generalised algebraic theory (which is the doctrine where dependent type theories live). In some sense this was kind of overkill, but it is something I'm very grateful to have in my pocket today.

Open ##1846803
@zwarich@hachyderm.io 2026-04-26 17:46

@jonmsterling This also touches on another point I like to trawl out on here from time to time, which is that despite technically being mathematics, type theory often doesn't feel very mathematical because it doesn't adopt the standard structuralist methods of ordinary mathematics, i.e. by coming up with simple definitions for a structure capturing a class of mathematical objects, and refining those structures with additional axioms that enable one to prove stronger theorems about them. I suspect that the difficulty of proving initiality in general for "reasonable type theories" is more a matter of defining a "reasonable type theory" than coming up with some truly novel mathematical content. [Edit: I just saw your post about Uemura's thesis; I'll have to take a look.] In the context of HoTT this is extremely ironic, given that one of the most mathematically enticing promises of univalence is enabling structuralism without the accounting overhead of isomorphisms.

Open ##1846804