×

Constructing higher inductive types as groupoid quotients. (English) Zbl 1498.03036

Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM). 929-943 (2020).

MSC:

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

Software:

Coq
PDFBibTeX XMLCite
Full Text: DOI