DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2025.46

Coslice Colimits in Homotopy Type Theory

Authors: Perry Hart and Kuen-Bang Hou (Favonia)

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract

We contribute to the theory of (homotopy) colimits inside homotopy type theory. The heart of our work characterizes the connection between colimits in coslices of a universe, called coslice colimits, and colimits in the universe (i.e., ordinary colimits). To derive this characterization, we find an explicit construction of colimits in coslices that is tailored to reveal the connection. We use the construction to derive properties of colimits. Notably, we prove that the forgetful functor from a coslice creates colimits over trees. We also use the construction to examine how colimits interact with orthogonal factorization systems and with cohomology theories. As a consequence of their interaction with orthogonal factorization systems, all pointed colimits (special kinds of coslice colimits) preserve n-connectedness, which implies that higher groups are closed under colimits on directed graphs. We have formalized our main construction of the coslice colimit functor in Agda.

Cite as

Perry Hart and Kuen-Bang Hou (Favonia). Coslice Colimits in Homotopy Type Theory. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 46:1-46:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hart_et_al:LIPIcs.CSL.2025.46,
  author =	{Hart, Perry and Hou (Favonia), Kuen-Bang},
  title =	{{Coslice Colimits in Homotopy Type Theory}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{46:1--46:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.46},
  URN =		{urn:nbn:de:0030-drops-228039},
  doi =		{10.4230/LIPIcs.CSL.2025.46},
  annote =	{Keywords: colimits, homotopy type theory, category theory, higher inductive types, synthetic homotopy theory}
}

Search Results

Documents authored by Hart, Perry

Coslice Colimits in Homotopy Type Theory

Abstract

Cite as

Thanks for your feedback!

Could not send message