Post #3066770
2026-05-21 15:39 UTC
@olynch@mathstodon.xyz uh elaborate please
Replies (2)
-
@olynch@mathstodon.xyz 2026-05-21 16:03
@mc@mathstodon.xyz Yeah exactly, you need a well-behaved notion of definitional equality in order to elaborate
-
@cbaberle@mathstodon.xyz 2026-05-21 22:24
@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.