Impredicative encodings of (higher) inductive types

DOI10.1145/3209108.3209130MaRDI QIDQ5145279zbMATH OpenOpenAlexFDO

Authors Jonas Frey, Sam Speight, Steve Awodey

Publication date 20 January 2021

Published in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1802.02820

zbMATH Keywords

homotopy type theorysystem Finductive typesimpredicativityhigher inductive typesMartin-Löf type theoryimpredicative encodings

Mathematics Subject Classification ID

Homotopical algebra, Quillen model categories, derivators (18N40) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38)

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.

Recommendations

• Semantics of higher inductive types
• Constructions with non-recursive higher inductive types
• Inductive types and exact completion
• On higher inductive types in cubical type theory
• scientific article; zbMATH DE number 1088050

Cited in

(12)

• Mathesis Universalis and Homotopy Type Theory
• Groupoidal realizability for intensional type theory
• Constructing higher inductive types as groupoid quotients
• Parametricity via cohesion
• A denotationally-based program logic for higher-order store
• Towards univalent reference types: the impact of univalence on denotational semantics
• Conservativity of type theory over higher-order arithmetic
• scientific article; zbMATH DE number 7561492 (Why is no real title available?)
• Toward the effective 2-topos
• On generalized algebraic theories and categories with families
• Impredicative encodings of inductive-inductive data in Cedille
• For Finitary Induction-Induction, Induction is Enough

This page was built for publication: Impredicative encodings of (higher) inductive types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145279)