Post #1846806

@zwarich Of course, we completely buried them in the end. There was a very silly "collective initiality project" that the pure mathematicians started, where they basically said they were going to try and resolve the conjecture by cosplaying whatever the fuck logicians do when faced with a problem like this. It was really funny to watch them scrambling, saying things like "It's not a proof unless it uses names and capture avoiding substitutions" and then a month later like "oh man that sucks so bad, I think de bruijn indices might actually be valid" and then two months later the project died. And then we resolved all the major conjectures in the syntactic metatheory of HoTT using ..... structural mathematics. (These would be: homotopy canonicity of HoTT, initiality of all conceivable type theories, normalisation and decidability of cubical type theory, not in that order.)