Strict Rezk completions of models of HoTT and homotopy canonicity
Rafaël Bocquet
我们为同源类型理论(HoTT)提供了新的建设性证明。 正法证明通常涉及对类型理论语法的粘合结构。 相反,我们使用粘合结构来“严格Rezk完成”的HoTT语法。 严格的Rezk完成是在笛卡立方集的托普中指定和构建的。 它完成了HoTT模型,相当于一个满足完整性条件的模型,提供了身份类型和术语之间的立方路径之间的等价。 这概括了普通Rezk完成1类。
We give a new constructive proof of homotopy canonicity for homotopy type theory (HoTT). Canonicity proofs typically involve gluing constructions over the syntax of type theory. We instead use a gluing construction over a "strict Rezk completion" of the syntax of HoTT. The strict Rezk completion is specified and constructed in the topos of cartesian cubical sets. It completes a model of HoTT to an equivalent model satisfying a completeness condition, providing an equivalence between terms of ide...