Impredicative Encodings of (Higher) Inductive Types

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 η-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.

References in corpus (1)

• Impredicative Encodings of (Higher) Inductive Types

Cited by in corpus (7)

• Impredicative Encodings of (Higher) Inductive Types
• Large and Infinitary Quotient Inductive-Inductive Types
• Constructing Higher Inductive Types as Groupoid Quotients
• A denotationally-based program logic for higher-order store
• A proposition is the (homotopy) type of its proofs
• A Note on Generalized Algebraic Theories and Categories with Families
• Parametricity via Cohesion