Post #1846803

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