A parametricity-based formalization of semi-simplicial and semi-cubical sets
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2023
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866915398745587712 |
|---|---|
| author | Herbelin, Hugo Ramachandra, Ramkumar |
| author_facet | Herbelin, Hugo Ramachandra, Ramkumar |
| contents | Semi-simplicial and semi-cubical sets are commonly defined as presheaves over respectively, the semi-simplex or semi-cube category. Homotopy Type Theory then popularized an alternative definition, where the set of n-simplices or n-cubes are instead regrouped into the families of the fibers over their faces, leading to a characterization we call indexed. Moreover, it is known that semi-simplicial and semi-cubical sets are related to iterated Reynolds parametricity, respectively in its unary and binary variants. We exploit this correspondence to develop an original uniform indexed definition of both augmented semi-simplicial and semi-cubical sets, and fully formalize it in Coq. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_00512 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | A parametricity-based formalization of semi-simplicial and semi-cubical sets Herbelin, Hugo Ramachandra, Ramkumar Logic in Computer Science F.4.1 Semi-simplicial and semi-cubical sets are commonly defined as presheaves over respectively, the semi-simplex or semi-cube category. Homotopy Type Theory then popularized an alternative definition, where the set of n-simplices or n-cubes are instead regrouped into the families of the fibers over their faces, leading to a characterization we call indexed. Moreover, it is known that semi-simplicial and semi-cubical sets are related to iterated Reynolds parametricity, respectively in its unary and binary variants. We exploit this correspondence to develop an original uniform indexed definition of both augmented semi-simplicial and semi-cubical sets, and fully formalize it in Coq. |
| title | A parametricity-based formalization of semi-simplicial and semi-cubical sets |
| topic | Logic in Computer Science F.4.1 |
| url | https://arxiv.org/abs/2401.00512 |