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 (10)

• Free higher groups in homotopy type theory
• Title not available (Why is that?)
• A construction method for induced types and its application to \(G_2\)
• Large and infinitary quotient inductive-inductive types
• Semantics of higher inductive types
• Quotients, inductive types, and quotient inductive types
• Constructions with non-recursive higher inductive types
• Constructing higher inductive types as groupoid quotients
• The integers as a higher inductive type
• Coherence for monoidal groupoids in HoTT

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)