van der Weide, Niels 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). Cited in 2 Documents MSC: 03B38 Type theory 18N10 2-categories, bicategories, double categories 55U35 Abstract and axiomatic homotopy theory in algebraic topology Keywords:Coq; bicategories; higher inductive types; homotopy type theory Software:Coq PDFBibTeX XMLCite \textit{N. van der Weide}, in: 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; Zbl 1498.03036) Full Text: DOI