I’ve put together a note on the Frobenius property for weak factorisaion systems and it’s relation to models of type theory. Awodey and Warren described a way of obtaining a model of type theory with identity types from a model category structure/weak factorisation system. However, in absence of axioms for other type formers (specifically, Π-types), one is required to put an additional restriction on the weak factorisation system, in order to model identity elimination in an arbitrary context/with arbitrary parameters; specifically, it is required that cofibrations are stable under pullbacks along fibrations. In presence of Π-types, however, this is not necessary, as I tried to explain in the note.

Advertisements