Homology, Homotopy and Applications
Volume 25 (2023)
Constructing coproducts in locally Cartesian closed $\infty$-categories
Pages: 71 – 86
We prove that every locally Cartesian closed $\infty$-category with a subobject classifier has a strict initial object and disjoint and universal binary coproducts.
higher category theory, higher topos theory, homotopy type theory, coproduct, impredicative encoding
2010 Mathematics Subject Classification
Copyright © 2023, Jonas Frey and Nima Rasekh. Permission to copy for private use granted.
Received 1 November 2021
Received revised 9 February 2022
Accepted 11 February 2022
Published 1 March 2023