On Higher Inductive Types in Cubical Type Theory

DOI10.1145/3209108.3209197zbMath1452.03036arXiv1802.01170OpenAlexW2964029175MaRDI QIDQ5145298

Thierry Coquand, Simon Huber, Anders Mörtberg

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

zbMATH Keywords

homotopy type theoryunivalent foundationshigher inductive typescubical type theory

Mathematics Subject Classification ID

Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38)

Related Items (23)

The construction of set-truncated higher inductive types ⋮ Cubical methods in homotopy type theory and univalent foundations ⋮ On Church’s thesis in cubical assemblies ⋮ Naive cubical type theory ⋮ Unnamed Item ⋮ Constructive sheaf models of type theory ⋮ Unnamed Item ⋮ A class of higher inductive types in Zermelo‐Fraenkel set theory ⋮ Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda ⋮ The compatibility of the minimalist foundation with homotopy type theory ⋮ Two-level type theory and applications ⋮ Canonicity and homotopy canonicity for cubical type theory ⋮ Type-theoretic approaches to ordinals ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ An introduction to univalent foundations for mathematicians ⋮ Semantics of higher inductive types ⋮ Unnamed Item ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types ⋮ Model structure on the universe of all types in interval type theory ⋮ Syntax and models of Cartesian cubical type theory

This page was built for publication: On Higher Inductive Types in Cubical Type Theory