Constructing higher inductive types as groupoid quotients

DOI10.1145/3373718.3394803MaRDI QIDQ5145692zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(11)

• Constructing infinitary quotient-inductive types
• Free higher groups in homotopy type theory
• A construction method for induced types and its application to G₂
• scientific article; zbMATH DE number 7168146 (Why is no real title available?)
• 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

Describes a project that uses

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)