Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Coslice Colimits in Homotopy Type Theory

Perry Hart, Kuen-Bang Hou

Abstract

We contribute to the theory of (homotopy) colimits inside homotopy type theory. The heart of our work characterizes the connection between (graph-indexed) colimits in a type universe and colimits in coslices of the universe, called coslice colimits. To derive this characterization, we give a construction of coslice colimits that is tailored to reveal the connection. We use the construction to prove that the forgetful functor from a coslice creates colimits over trees. We also use it to study how coslice colimits interact with orthogonal factorization systems and with cohomology theories. As a result of their interaction with orthogonal factorization systems, all colimits of pointed types preserve $n$-connectedness, which implies that higher groups, in the sense of Buchholtz, van Doorn, and Rijke, are closed under colimits. We have formalized major portions of this work (see https://github.com/PHart3/colimits-agda for the Agda code), including our main construction of the coslice colimit functor.

Coslice Colimits in Homotopy Type Theory

Abstract

We contribute to the theory of (homotopy) colimits inside homotopy type theory. The heart of our work characterizes the connection between (graph-indexed) colimits in a type universe and colimits in coslices of the universe, called coslice colimits. To derive this characterization, we give a construction of coslice colimits that is tailored to reveal the connection. We use the construction to prove that the forgetful functor from a coslice creates colimits over trees. We also use it to study how coslice colimits interact with orthogonal factorization systems and with cohomology theories. As a result of their interaction with orthogonal factorization systems, all colimits of pointed types preserve -connectedness, which implies that higher groups, in the sense of Buchholtz, van Doorn, and Rijke, are closed under colimits. We have formalized major portions of this work (see https://github.com/PHart3/colimits-agda for the Agda code), including our main construction of the coslice colimit functor.

Paper Structure

This paper contains 23 sections, 57 theorems, 81 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Type system
  3. Categorical background
  4. Wild categories and functors
  5. Reflective subcategories
  6. Orthogonal factorization systems
  7. Coslices of a universe
  8. Diagrams in coslices
  9. Graphs and trees
  10. Colimits
  11. Ordinary colimits
  12. Coslice colimits
  13. Coslice coproducts
  14. Quotient construction of coslice colimits
  15. Pushout-coproduct construction of coslice colimits
  16. ...and 8 more sections

Key Result

Lemma 3.1.3

Let $\mathcal{C}$ be a bicategory. For all $A, B, C : \mathop{\mathrm{\mathsf{Ob}}}\nolimits(\mathcal{C})$, $f : \mathop{\mathrm{\mathsf{hom}}}\nolimits_{\mathcal{C}}(A,B)$, $g : \mathop{\mathrm{\mathsf{hom}}}\nolimits_{\mathcal{C}}(B,C)$,

Figures (2)

  • Figure 1: $C_{\Xi}(a)$
  • Figure 2: reduction to canonical $\mathop{\mathrm{\mathsf{PI}}}\nolimits$ term

Theorems & Definitions (129)

  • Definition 3.1.1
  • Definition 3.1.2
  • Lemma 3.1.3
  • proof
  • Definition 3.1.4
  • Example 3.1.5
  • Definition 3.1.6
  • Definition 3.1.7
  • Definition 3.2.1
  • Proposition 3.2.2
  • ...and 119 more