Strict Rezk completions of models of HoTT and homotopy canonicity
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918156489981952 |
|---|---|
| author | Bocquet, Rafaël |
| author_facet | Bocquet, Rafaël |
| contents | 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 identity types and cubical paths between terms. This generalizes the ordinary Rezk completion of a 1-category. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2311_05849 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Strict Rezk completions of models of HoTT and homotopy canonicity Bocquet, Rafaël Category Theory Logic in Computer Science 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 identity types and cubical paths between terms. This generalizes the ordinary Rezk completion of a 1-category. |
| title | Strict Rezk completions of models of HoTT and homotopy canonicity |
| topic | Category Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2311.05849 |