The Integers as a Higher Inductive Type

DOI10.1145/3373718.3394760zbMath1498.03028arXiv2007.00167OpenAlexW3032285962MaRDI QIDQ5145619

Thorsten Altenkirch, Luis Nerio Scoccola

Publication date: 21 January 2021

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

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

zbMATH Keywords

truncationcoherence probleminitialityhigher inductive type

Mathematics Subject Classification ID

Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Related Items (2)

Unnamed Item ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types

This page was built for publication: The Integers as a Higher Inductive Type