Volume I · Experimental web edition

Exercises

Chapters 1 and 2 use the rebuild2 formalization. Agda links for Chapter 3 remain temporarily unavailable.

3.8 Exercises Chapter 3

Exercise 3.8.1. Consider a category \(\Gamma \), a category \(D\) and a category \(q\colon E\to \Gamma \) over \(\Gamma \). Put \(D_\Gamma :=D\times \Gamma \to \Gamma \). Define a category \(\ulFun _\Gamma (D_\Gamma ,E)\) over \(\Gamma \) by the pullback square

Commutative diagram from the manuscript; its arrows and comparisons are described in the surrounding text.

where \(\delta _\Gamma \) is the currying of the projection \(\Gamma \times D\to \Gamma \). Show that this category has the universal property of the relative functor category from \(D_\Gamma \) to \(E\) over \(\Gamma \).

Exercise 3.8.2. Prove Lemma 3.2.10: show that for embeddings \(\Gamma \hookrightarrow C^{\simeq }\) and \(\Lambda \hookrightarrow D^{\simeq }\) the projections \(C \times D \to C\) and \(C \times D \to D\) induce an equivalence \[ \langle \Gamma \times \Lambda \subseteq C \times D \rangle \iso \langle \Gamma \subseteq C \rangle \times \langle \Lambda \subseteq D \rangle . \]

Exercise 3.8.3. Prove the assertions from Remark 3.1.17: given a functor \(f\colon C \to D\) sending a collection of morphisms \(M\) in \(C\) to a collection of morphisms \(N\) in \(D\), we have:

(1)

The map \(f\vert \colon \lra {M}_C \to \lra {N}_D\) is uniquely determined by \(f\).

(2)

Given an identification \(f = f'\), we obtain an induced identification \(f\vert = f'\vert \).

(3)

The construction is compatible with identities and composition: we have identifications \((\id _C)\vert = \id _{\lra {M}_C}\) and \((g \circ f)\vert = g\vert \circ f \vert \) if \(g\colon D \to E\) is another functor preserving a collection of morphisms.

(4)

If the functors \(f\colon C \to D\) and \(\tilde {f}\colon M \to N\) are equivalences, then also \(f\vert \colon \lra {M}_C \to \lra {N}_D\) is an equivalence.

Exercise 3.8.4. Let \(W\) be a collection of morphisms in a category \(C\), and let \(l\colon C \to L\) and \(l'\colon C \to L'\) be two localizations of \(C\) at \(W\). Construct an equivalence \(L \iso L'\).

Exercise 3.8.5. Let \(W\) be a collection of morphisms in a category \(C\), and let \(C \to C[W^{-1}]\) be a localization of \(C\) at \(W\). Construct a pushout square

Commutative diagram from the manuscript; its arrows and comparisons are described in the surrounding text.

where the map \(\tilde {w}\) is obtained by uncurrying the composite \(W \xrightarrow {w} \Map ([1],C) \to \Fun ([1],C)\).

Exercise 3.8.6. Let \(p\colon S \to T\) be a functor, and let \(f\colon C \to S\) be a category over \(S\). Let \(g\colon D \to T\) and \(g'\colon D' \to T\) be categories over \(T\) that are both a dependent product of \(C\) along \(p\). Show that there is an equivalence \(D \iso D'\) of categories over \(T\) (in the sense of Definition 4.3.3 (outside selection)).

Bibliography

[Awo14]

Steve Awodey. “Structuralism, invariance, and univalence”. Philos. Math. (3) 22.1 (2014), pp. 1–11.

[Bar+16]

Clark Barwick, Emanuele Dotto, Saul Glasman, Denis Nardin, and Jay Shah. “Parametrized higher category theory and higher algebra: Exposé I - Elements of parametrized higher category theory”. arXiv preprint arXiv:1608.03657 (2016).

[BFM24]

Thibaut Benjamin, Eric Finster, and Samuel Mimram. “Globular weak \(\omega \)-categories as models of a type theory”. High. Struct. 8.2 (2024), pp. 1–69.

[Cis19]

Denis-Charles Cisinski. Higher categories and homotopical algebra. Vol. 180. Cambridge studies in advanced mathematics. Cambridge University Press, Cambridge, 2019.

[CN22]

Denis-Charles Cisinski and Hoang Kim Nguyen. The universal coCartesian fibration. 2022. arXiv: 2210.08945. url: https://arxiv.org/abs/2210.08945.

[FM17]

Eric Finster and Samuel Mimram. “A type-theoretical definition of weak \(\infty \)-categories”. English. Proceedings of the 2017 32nd annual ACM/IEEE symposium on logic in computer science, LICS 2017, Reykjavík University, Reykjavík, Iceland, June 20–23, 2017. Piscataway, NJ: IEEE Press, 2017, p. 12. isbn: 978-1-5090-3018-7.

[GWB24]

Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchholtz. Directed univalence in simplicial homotopy type theory. 2024. arXiv: 2407.09146 [cs.LO]. url: https://arxiv.org/abs/2407.09146.

[GWB26]

Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchholtz. The \(\infty \)-category of \(\infty \)-categories in simplicial type theory. 2026. arXiv: 2602.02218. url: https://arxiv.org/abs/2602.02218.

[Joy08]

André Joyal. “Notes on quasi-categories”. preprint (2008).

[KL21]

Krzysztof Kapulkin and Peter Lefanu Lumsdaine. “The simplicial model of univalent foundations (after Voevodsky)”. J. Eur. Math. Soc. (JEMS) 23.6 (2021), pp. 2071–2126. issn: 1435-9855.

[LM05]

Elaine Landry and Jean-Pierre Marquis. “Categories in context: historical, foundational, and philosophical”. Philos. Math. (3) 13.1 (2005), pp. 1–43.

[Lur09]

Jacob Lurie. Higher topos theory. Vol. 170. Ann. Math. Stud. Princeton, NJ: Princeton University Press, 2009.

[Lur17]

Jacob Lurie. “Higher algebra”. https://www.math.ias.edu/~lurie/papers/HA.pdf (2017).

[Mak98]

M. Makkai. “Towards a categorical foundation of mathematics”. Logic colloquium ’95. Proceedings of the Annual European Summer Meeting of the Association of Symbolic Logic, Haifa, Israel, August 9–18, 1995. Berlin: Springer, 1998, pp. 153–190.

[Mar13]

Jean-Pierre Marquis. “Categorical foundations of mathematics. Or how to provide foundations for abstract mathematics.” Rev. Symb. Log. 6.1 (2013), pp. 51–86.

[MW24]

Louis Martini and Sebastian Wolf. “Colimits and cocompletions in internal higher category theory”. High. Struct. 8.1 (2024), pp. 97–192. doi: 10.21136/HS.2024.0398. url: https://doi.org/10.21136/HS.2024.0398.

[Rod14]

Andrei Rodin. Axiomatic method and category theory. Vol. 364. Synth. Libr. Cham: Springer, 2014.

[RS17]

Emily Riehl and Michael Shulman. “A type theory for synthetic \(\infty \)-categories”. High. Struct. 1.1 (2017), pp. 147–224.

[RV22]

Emily Riehl and Dominic Verity. Elements of \(\infty \)-category theory. Vol. 194. Camb. Stud. Adv. Math. Cambridge: Cambridge University Press, 2022.

[Tse17]

Dimitris Tsementzis. “Univalent foundations as structuralist foundations”. Synthese 194.9 (2017), pp. 3583–3617.

[Uni13]

The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study: https://homotopytypetheory.org/book, 2013.

Supplementary notes