Impredicative Encodings of (Higher) Inductive Types

DOI10.1145/3209108.3209130zbMath1452.03030arXiv1802.02820OpenAlexW2963511234MaRDI QIDQ5145279

Sam Speight, Jonas Frey, Steven 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

inductive typesMartin-Löf type theoryhomotopy type theorysystem Fimpredicativityhigher inductive typesimpredicative encodings

Mathematics Subject Classification ID

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

Related Items (5)

On generalized algebraic theories and categories with families ⋮ Unnamed Item ⋮ Mathesis Universalis and Homotopy Type Theory ⋮ For Finitary Induction-Induction, Induction is Enough ⋮ Unnamed Item

This page was built for publication: Impredicative Encodings of (Higher) Inductive Types