Impredicative Encodings of (Higher) Inductive Types
Logic in Computer Science
2024-02-22 v1 Category Theory
Logic
Abstract
Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant {\eta}-equalities and consequently do not admit dependent eliminators. To recover {\eta} 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.
Keywords
Cite
@article{arxiv.1802.02820,
title = {Impredicative Encodings of (Higher) Inductive Types},
author = {Steve Awodey and Jonas Frey and Sam Speight},
journal= {arXiv preprint arXiv:1802.02820},
year = {2024}
}