Impredicative Encodings of (Higher) Inductive Types
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2018
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866913238042542080 |
|---|---|
| author | Awodey, Steve Frey, Jonas Speight, Sam |
| author_facet | Awodey, Steve Frey, Jonas Speight, Sam |
| contents | Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant η-equalities and consequently do not admit dependent eliminators. To recover η and dependent elimination, we present a method to construct refinements of these impredicative encodings, using ideas from homotopy type theory. We then extend our method to construct impredicative encodings of some higher inductive types, such as 1-truncation and the unit circle S1. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_1802_02820 |
| institution | arXiv |
| publishDate | 2018 |
| record_format | arxiv |
| spellingShingle | Impredicative Encodings of (Higher) Inductive Types Awodey, Steve Frey, Jonas Speight, Sam Logic in Computer Science Category Theory Logic Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant η-equalities and consequently do not admit dependent eliminators. To recover η and dependent elimination, we present a method to construct refinements of these impredicative encodings, using ideas from homotopy type theory. We then extend our method to construct impredicative encodings of some higher inductive types, such as 1-truncation and the unit circle S1. |
| title | Impredicative Encodings of (Higher) Inductive Types |
| topic | Logic in Computer Science Category Theory Logic |
| url | https://arxiv.org/abs/1802.02820 |