Constructing Higher Inductive Types as Groupoid Quotients

DOI10.1145/3373718.3394803zbMath1498.03036OpenAlexW3032100515MaRDI QIDQ5145692

Niels van der Weide

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://doi.org/10.1145/3373718.3394803

zbMATH Keywords

homotopy type theoryCoqbicategorieshigher inductive types

Mathematics Subject Classification ID

Abstract and axiomatic homotopy theory in algebraic topology (55U35) 2-categories, bicategories, double categories (18N10) Type theory (03B38)

Related Items (2)

Unnamed Item ⋮ Unnamed Item

Uses Software

• Coq

This page was built for publication: Constructing Higher Inductive Types as Groupoid Quotients