Morita equivalence of weakly and strictly stable weak identity types
Morita equivalence of weakly and strictly stable weak identity types
Let be the category of contextual categories with weakly stable weak identity types, let be the corresponding generating cofibrations, and let be the left adjoint in the free-forgetful adjunction between weakly stable and strictly stable structures. For an -cellular model , write 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 -cellular model , the unit
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
Nothing recorded yet. Refresh searches the literature and the public web for attempts on this problem, and writes the first summary here.
Solutions 0
Sign in to submit a solution.
No solutions have been posted yet.