Coslice Colimits in Homotopy Type Theory

1. Problem Statement

The paper addresses the construction and characterization of colimits within coslice categories of a type universe ($A/\mathcal{U}$) inside Homotopy Type Theory (HoTT).

• Context: In HoTT, colimits are typically defined as Higher Inductive Types (HITs). While general schemas for HITs exist, they often treat colimits in a "black box" manner.
• The Gap: There is a need to explicitly construct colimits in a coslice category $A/\mathcal{U}$ (types equipped with a map from a fixed type $A$) using only the basic machinery of Martin-Löf Type Theory (MLTT) augmented with pushouts. The goal is to reveal the precise relationship between these "coslice colimits" and ordinary colimits in the underlying universe $\mathcal{U}$.
• Specific Challenges:
  • Coslice categories are not generally Locally Cartesian Closed (LCC), complicating the transfer of properties like universality.
  • Understanding how colimits interact with orthogonal factorization systems (OFS) and cohomology theories in the context of pointed types and higher groups.

2. Methodology

The authors employ a constructive approach within HoTT, avoiding postulation of general HIT schemas in favor of explicit constructions using pushouts and quotients.

• The "Main Connection" (Quotient Construction):
  The core method involves constructing the colimit of a diagram $F$ in $A/\mathcal{U}$ (denoted $\text{colim}_A(F)$) by starting with the ordinary colimit of the underlying diagram in $\mathcal{U}$ ($\text{colim}(F_g(F))$) and then "gluing" the necessary 2-cells to satisfy the coslice structure.

  • They define a map $\psi: \text{colim } A \to \text{colim}(F_g(F))$ induced by the constant diagram at $A$.
  • They form a pushout square (a quotient) involving $\text{colim } A$, $\text{colim}(F_g(F))$, and $A$. This quotient effectively fills the "distinguished loops" in the ordinary colimit that arise from the coslice structure (paths of the form $\eta(\text{pr}_2(F_i)(a))$).
  • This construction is proven to be the colimit in $A/\mathcal{U}$ by establishing an equivalence between the type of maps out of the constructed object and the type of cocones.

• Alternative Construction (Pushout of Coproducts):
  Using the $3 \times 3$ lemma, the authors derive a second construction of coslice colimits as a pushout of coproducts (wedge sums). This mirrors classical lemmas and is crucial for analyzing interactions with cohomology.

• Categorical Framework:
  The paper utilizes wild categories (categories where composition and identities hold up to paths rather than strictly) and wild functors. This framework is necessary because the universe $\mathcal{U}$ and its coslices do not form strict categories in the traditional sense. They also develop the theory of Orthogonal Factorization Systems (OFS) within this wild setting.

3. Key Contributions

A. Characterization of Coslice Colimits

The primary contribution is the explicit construction of $\text{colim}_A(F)$ as a quotient of the ordinary colimit. This establishes a "main connection" showing that coslice colimits are not arbitrary HITs but are structurally derived from ordinary colimits by collapsing specific loops.

B. Creation of Colimits by the Forgetful Functor

The authors prove that the forgetful functor $U: A/\mathcal{U} \to \mathcal{U}$ creates colimits over trees (graphs whose quotient is contractible).

• Result: If $\Gamma$ is a tree, the forgetful functor preserves and reflects colimits.
• Significance: This implies that for tree-shaped diagrams, the coslice colimit is equivalent to the ordinary colimit of the underlying types. This allows the transfer of properties (like universality) from $\mathcal{U}$ to $A/\mathcal{U}$ in these specific cases.

C. Preservation of Connectedness and Factorization Systems

The paper demonstrates that coslice colimits preserve the left class of orthogonal factorization systems on the universe $\mathcal{U}$.

• Theorem: If a diagram consists of $(n, k)$-connected types, its coslice colimit is also $(n, k)$-connected.
• Application: This proves that the category of higher groups (specifically $k$-tuply groupal $n$-groupoids, denoted $(n, k)\text{GType}$) is cocomplete. This is a significant result because these categories are not obviously closed under colimits in standard settings.

D. Weak Continuity of Cohomology

The authors investigate the interaction between colimits and Eilenberg-Steenrod cohomology theories.

• Result: They prove that cohomology functors send finite colimits in $A/\mathcal{U}$ to weak limits in $\text{Set}$.
• Mechanism: By combining the pushout-coproduct construction with the Mayer-Vietoris sequence, they show that the canonical map from the colimit to the limit of cohomology groups is a surjection (epimorphism). Under the assumption of the Axiom of Choice, this implies the existence of a section, making it a weak limit.

4. Key Results

1. Universality over Trees: The forgetful functor $A/\mathcal{U} \to \mathcal{U}$ creates colimits for diagrams indexed by trees. Consequently, colimits over trees in $A/\mathcal{U}$ are universal (pullback-stable).
2. Cocompleteness of Higher Groups: The category $(n, k)\text{GType}$ is cocomplete. This is derived by showing that the subcategory of $(k-1)$-connected types in $A/\mathcal{U}$ is reflective and closed under colimits.
3. Preservation of Connectedness: Colimits of pointed $n$-connected types remain $n$-connected. This generalizes the fact that the suspension of a connected type is connected.
4. Cohomology and Weak Limits: For finite graphs, cohomology theories map colimits to weak limits. This provides a type-theoretic version of the conditions required for the Brown representability theorem.

5. Significance

• Foundational Clarity: The paper demystifies the construction of colimits in coslice categories, moving from abstract existence (via general HIT schemas) to concrete, computable constructions using pushouts. This is vital for formal verification.
• Formalization: Major portions of the work, including the main construction and the preservation of factorization systems, have been formalized in Agda. This provides a verified foundation for synthetic homotopy theory.
• Synthetic Homotopy Theory: The results bridge the gap between classical homotopy theory (where properties like cocompleteness of higher group categories are known or conjectured) and the internal logic of HoTT. It confirms that the internal logic supports these high-level categorical structures.
• Generalizability: The framework of "wild categories" and the specific techniques for handling coslice colimits can be applied to other contexts in HoTT where standard categorical assumptions (like LCC) fail.

In summary, Hart and Favonia provide a rigorous, constructive theory of colimits in coslice categories, proving that they behave well with respect to trees, factorization systems, and cohomology, thereby establishing the cocompleteness of important categories of higher algebraic structures within HoTT.