Post #3066774

@mc@mathstodon.xyz @olynch@mathstodon.xyz If you do the usual categorical thing and define (e.g.) the action of substitution on types only up to isomorphism (i.e. as pullback, but without a strictly-functorial *choice* of pullbacks) then you run into coherence issues trying to interpret type theory soundly, since type theory models substitution as strictly associative, whereas it's generally only associative up to coherent iso in categorical models. Of course, you *could* work with strict categories, split fibrations, etc. But then univalence-pilled people will look at you funny.