Niccolò Veltri ; Niels van der Weide - Constructing Higher Inductive Types as Groupoid Quotients

lmcs:6607 - Logical Methods in Computer Science, April 22, 2021, Volume 17, Issue 2 - https://doi.org/10.23638/LMCS-17(2:8)2021
Constructing Higher Inductive Types as Groupoid Quotients

Authors: Niccolò Veltri ; Niels van der Weide

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 algebras in 1-types and in groupoids. We continue by proving initial algebra semantics for our signatures. After that, we show that the groupoid quotient induces a biadjunction between the bicategories of algebras in 1-types and in groupoids. Then we construct a biinitial object in the bicategory of algebras in groupoids, which gives the desired algebra. From all this, we conclude that all finitary 1-truncated HITs can be constructed from the groupoid quotient. We present several examples of HITs which are definable using our notion of signature. In particular, we show that each signature gives rise to a HIT corresponding to the freely generated algebraic structure over it. We also start the development of universal algebra in 1-types. We show that the bicategory of algebras has PIE limits, i.e. products, inserters and equifiers, and we prove a version of the first isomorphism theorem for 1-types. Finally, we give an alternative characterization of the foundamental groups of some HITs, exploiting our construction of HITs via the groupoid quotient. All the results are formalized over the UniMath library of univalent mathematics in Coq.


Volume: Volume 17, Issue 2
Published on: April 22, 2021
Accepted on: March 5, 2021
Submitted on: June 30, 2020
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 95 times.
This article's PDF has been downloaded 53 times.