Constructing Higher Inductive Types as Groupoid Quotients
In this paper, we study finitary 1-truncated higher inductive types (HITs) in homotopy type theory. We start by showing that all these types can be constructed from the groupoid quotient. We define an internal notion of signatures for HITs, and for each signature, we construct a bicategory of algebr...
Main Authors: | Niccolò Veltri, Niels van der Weide |
---|---|
Format: | Article |
Language: | English |
Published: |
Logical Methods in Computer Science e.V.
2021-04-01
|
Series: | Logical Methods in Computer Science |
Subjects: | |
Online Access: | https://lmcs.episciences.org/6607/pdf |
Similar Items
-
Quotients, inductive types, and quotient inductive types
by: Marcelo P. Fiore, et al.
Published: (2022-06-01) -
On the Taylor expansion of $\lambda$-terms and the groupoid structure of their rigid approximants
by: Federico Olimpieri, et al.
Published: (2022-01-01) -
Signatures and Induction Principles for Higher Inductive-Inductive Types
by: Ambrus Kaposi, et al.
Published: (2020-02-01) -
On Second-Order Monadic Monoidal and Groupoidal Quantifiers
by: Juha Kontinen, et al.
Published: (2010-09-01) -
Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory
by: Bassel Mannaa, et al.
Published: (2020-12-01)