Proofs that need to be added at some point:
-
•
Extra proof of Chapter 7: Tensor Products of Pointed Sets, Theorem 7.5.10.1.1 using the machinery of presentable categories, following Maxime Ranzi’s answer to MO 466593
.
-
•
Horizontal composition of natural transformations is associative: Chapter 11: Categories, Item 2 of Proposition 11.9.5.1.3.
-
•
Fully faithful functors are essentially injective: Chapter 11: Categories, Item 4 of Proposition 11.6.3.1.2.
Proofs that would be very nice to be added at some point:
-
•
Properties of pseudomonic functors: Chapter 11: Categories, Proposition 11.7.4.1.2
.
-
•
Characterisation of fully faithful functors: Chapter 11: Categories, Item 1 of Proposition 11.6.3.1.2.
-
•
The quadruple adjunction between categories and sets: Chapter 11: Categories, Proposition 11.3.1.1.1.
-
•
$F_{*}$ faithful iff $F$ faithful: Chapter 11: Categories, Item 2 of Proposition 11.6.1.1.2.
-
•
Properties of groupoid completions: Chapter 11: Categories, Proposition 11.4.3.1.3.
-
•
Properties of cores: Chapter 11: Categories, Proposition 11.4.4.1.4.
-
•
$\mathrm{Rel}$ is isomorphic to the category of free algebras of the powerset monad: Chapter 8: Relations, Proposition 8.4.14.1.1
.
-
•
Non/existence of left Kan extensions in $\boldsymbol {\mathsf{Rel}}$:
-
•
Non/existence of left Kan lifts in $\boldsymbol {\mathsf{Rel}}$:
Proofs that would be nice to be added at some point:
-
•
Properties of posetal categories: Chapter 11: Categories, Proposition 11.2.7.1.2.
-
•
Injective on objects functors are precisely the isocofibrations in $\mathsf{Cats}_{\mathsf{2}}$: Chapter 11: Categories, Item 1 of Proposition 11.8.1.1.2
.
-
•
Characterisations of monomorphisms of categories: Chapter 11: Categories, Item 1 of Proposition 11.7.2.1.2.
-
•
Epimorphisms of categories are surjective on objects: Chapter 11: Categories, Item 2 of Proposition 11.7.3.1.2.
-
•
Properties of pseudoepic functors: Chapter 11: Categories, Proposition 11.7.5.1.2
.
Proofs that would be nice but not essential to be added at some point:
-
•
Proof that $\webleft (\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\text{Ø},\times ,\mathrm{pt}\webright )$ is a symmetric bimonoidal category: Chapter 4: Constructions With Sets, Item 15 of Proposition 4.1.3.1.3
.
-
•
Proof that $\webleft (\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\text{Ø},\times ,\mathrm{pt}\webright )$ is a symmetric bimonoidal category: Chapter 5: Monoidal Structures on the Category of Sets, Proposition 5.3.5.1.1
.
-
•
Proof that $\webleft (\mathsf{Sets},\times _{X},X\webright )$ is a symmetric monoidal category: Chapter 4: Constructions With Sets, Item 11 of Proposition 4.1.4.1.5
.
-
•
Proof that $\webleft (\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\text{Ø}\webright )$ is a symmetric monoidal category: Chapter 4: Constructions With Sets, Item 6 of Proposition 4.2.3.1.3
.
-
•
Proof that $\webleft (\mathsf{Sets},\mathbin {\textstyle \coprod _{X}},X\webright )$ is a symmetric monoidal category: Chapter 4: Constructions With Sets, Item 8 of Proposition 4.2.4.1.6
.
Proofs that have been (temporarily) omitted because they are “clear”, “straightforward”, or “tedious”:
-
•
Properties of pushouts of sets:
-
•
Associativity: Chapter 4: Constructions With Sets, Item 3 of Proposition 4.2.4.1.6.
-
•
Unitality: Chapter 4: Constructions With Sets, Item 5 of Proposition 4.2.4.1.6.
-
•
Commutativity: Chapter 4: Constructions With Sets, Item 6 of Proposition 4.2.4.1.6.
-
•
Pushout of sets over the empty set recovers the coproduct of sets: Chapter 4: Constructions With Sets, Item 7 of Proposition 4.2.4.1.6.
-
•
-
•
Properties of coequalisers of sets:
-
•
Associativity: Chapter 4: Constructions With Sets, Item 1 of Proposition 4.2.5.1.5.
-
•
Unitality: Chapter 4: Constructions With Sets, Item 2 of Proposition 4.2.5.1.5.
-
•
Commutativity: Chapter 4: Constructions With Sets, Item 3 of Proposition 4.2.5.1.5.
-
•
Interaction with composition: Chapter 4: Constructions With Sets, Item 4 of Proposition 4.2.5.1.5.
-
•
-
•
Properties of set differences:
-
•
Complements and characteristic functions: Chapter 4: Constructions With Sets, Item 4 of Proposition 4.3.11.1.2.
-
•
Properties of symmetric differences:
-
•
Properties of direct images:
-
•
Functoriality: Chapter 4: Constructions With Sets, Item 1 of Proposition 4.6.1.1.5.
-
•
Interaction with coproducts: Chapter 4: Constructions With Sets, Item 15 of Proposition 4.6.1.1.5.
-
•
Interaction with products: Chapter 4: Constructions With Sets, Item 16 of Proposition 4.6.1.1.5.
-
•
-
•
Properties of inverse images:
-
•
Functoriality: Chapter 4: Constructions With Sets, Item 1 of Proposition 4.6.2.1.3.
-
•
Interaction with coproducts: Chapter 4: Constructions With Sets, Item 15 of Proposition 4.6.2.1.3.
-
•
Interaction with products; Chapter 4: Constructions With Sets, Item 16 of Proposition 4.6.2.1.3.
-
•
-
•
Properties of codirect images:
-
•
Functoriality: Chapter 4: Constructions With Sets, Item 1 of Proposition 4.6.3.1.7.
-
•
Lax preservation of colimits: Chapter 4: Constructions With Sets, Item 10 of Proposition 4.6.3.1.7.
-
•
Interaction with coproducts: Chapter 4: Constructions With Sets, Item 14 of Proposition 4.6.3.1.7.
-
•
Interaction with products: Chapter 4: Constructions With Sets, Item 15 of Proposition 4.6.3.1.7.
-
•
-
•
Left distributor of $\times $ over $\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}$ is a natural isomorphism: Chapter 5: Monoidal Structures on the Category of Sets, Definition 5.3.1.1.1.
-
•
Right distributor of $\times $ over $\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}$ is a natural isomorphism: Chapter 5: Monoidal Structures on the Category of Sets, Definition 5.3.2.1.1.
-
•
Left annihilator of $\times $ is a natural isomorphism: Chapter 5: Monoidal Structures on the Category of Sets, Definition 5.3.3.1.1.
-
•
Right annihilator of $\times $ is a natural isomorphism: Chapter 5: Monoidal Structures on the Category of Sets, Definition 5.3.4.1.1.
-
•
Properties of wedge products of pointed sets:
-
•
Associativity: Chapter 6: Pointed Sets, Item 2 of Proposition 6.3.3.1.3.
-
•
Unitality: Chapter 6: Pointed Sets, Item 3 of Proposition 6.3.3.1.3.
-
•
Commutativity: Chapter 6: Pointed Sets, Item 4 of Proposition 6.3.3.1.3.
-
•
Symmetric monoidality: Chapter 6: Pointed Sets, Item 5 of Proposition 6.3.3.1.3.
-
•
-
•
Properties of pushouts of pointed sets:
-
•
Interaction with coproducts: Chapter 6: Pointed Sets, Item 5 of Proposition 6.3.4.1.3.
-
•
Symmetric monoidality: Chapter 6: Pointed Sets, Item 6 of Proposition 6.3.4.1.3.
-
•
