Homology, Homotopy and Applications

Volume 25 (2023)

Number 1

Constructing coproducts in locally Cartesian closed $\infty$-categories

Pages: 71 – 86

DOI: https://dx.doi.org/10.4310/HHA.2023.v25.n1.a4


Jonas Frey (Department of Philosophy, Carnegie Mellon University, Pittsburgh, Pennsylvania, U.S.A.)

Nima Rasekh (École Polytechnique Fédérale de Lausanne, Lausanne, Switzerland)


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

03G30, 18B25

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