Andrew Swan: Identity types in Algebraic Model Structures

The original Bezem-Coquand-Huber cubical set model promised to give a constructive model of homotopy type theory. However, in its original form there was a notable shortcoming: one of the definitional equalities usually included in type theory, the J computation rule was absent. One way to fix this is to use an alternative definition of identity type in which we keep track more carefully of degenerate paths. The new identity type has a nice presentation in the setting of algebraic model structures. To model identity types what we need is very good path objects: a factorisation of each diagonal as a trivial cofibration followed by a fibration. I'll show a general way to create very good path objects from path objects in the weaker sense of factorisations of diagonals as weak equivalence followed by fibration, and that under certain reasonable conditions on an ams this can be carried out "stably and functorially" allowing us to satisfy the Garner-van den Berg notion of "stable functorial choice of diagonal factorisation." I'll use these ideas to show that in particular cubical sets with Kan fibrations satisfy Garner and van den Berg's notion of homotopy theoretic model of identity types. In this way we get a constructive proof that cubical sets model intensional type theory including all definitional equalities, dealing with coherence issues directly without using universes or local universes and retaining any propositions from the original BCH model, including univalence.