Strict Rezk completions of models of HoTT and homotopy canonicity

Rafaël Bocquet

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…