Constructing higher inductive types as groupoid quotients

DOI10.1145/3373718.3394803zbMATH Open1498.03036OpenAlexW3032100515MaRDI QIDQ5145692FDOQ5145692

Authors: 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

Recommendations

• Constructing higher inductive types as groupoid quotients
• Quotient inductive-inductive types
• Semantics of higher inductive types
• Higher inductive types as homotopy-initial algebras
• Quotients, inductive types, and quotient inductive types

zbMATH Keywords

Coqbicategorieshomotopy type theoryhigher inductive types

Mathematics Subject Classification ID

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

Cited In (3)

• Title not available (Why is that?)
• Title not available (Why is that?)
• A construction method for induced types and its application to \(G_2\)

Uses Software

• Coq

This page was built for publication: Constructing higher inductive types as groupoid quotients

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145692)