Morita equivalence of weakly and strictly stable weak identity types

Let CwFws\mathbf{CwF}_{ws} be the category of contextual categories with weakly stable weak identity types, let IwsI_{ws} be the corresponding generating cofibrations, and let LL be the left adjoint in the free-forgetful adjunction between weakly stable and strictly stable structures. For an IwsI_{ws}-cellular model C:CwFws\mathcal{C}:\mathbf{CwF}_{ws}, write η:CL(C)\eta:\mathcal{C}\to L(\mathcal{C}) for the unit.

Morita equivalence conjecture. The theories of weakly stable weak identity types and strictly stable weak identity types are Morita equivalent: for every IwsI_{ws}-cellular model C:CwFws\mathcal{C}:\mathbf{CwF}_{ws}, the unit

η:CL(C)\eta:\mathcal{C}\to L(\mathcal{C})

is a weak equivalence.

This would provide the desired coherence theorem by showing that strictification preserves the homotopical theory of weakly stable identity types. The paper presents this as a goal toward a full coherence theorem, and no proof or resolution is supplied here.

Sources & referencesView supporting material

Primary source

Rafaël Bocquet, “Strictification of weakly stable type-theoretic structures using generic contexts”, arXiv:2111.10862 (2022).

Progress summary

Never refreshed

Nothing recorded yet. Refresh searches the literature and the public web for attempts on this problem, and writes the first summary here.

Solutions 0

No solutions have been posted yet.