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

Authors

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

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

Abstract

We prove that every locally Cartesian closed $\infty$-category with a subobject classifier has a strict initial object and disjoint and universal binary coproducts.

Keywords

higher category theory, higher topos theory, homotopy type theory, coproduct, impredicative encoding

2010 Mathematics Subject Classification

03G30, 18B25

Full Text (PDF format)

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