Proofs that need to be added at some point:
- Chapter 5: Tensor Products of Pointed Sets, Theorem 5.5.10.1.1.
- Chapter 5: Tensor Products of Pointed Sets, Theorem 5.5.11.1.1.
- Horizontal composition of natural transformations is associative: Chapter 9: Categories, Item 2 of Proposition 9.9.5.1.3.
- Fully faithful functors are essentially injective: Chapter 9: Categories, Item 4 of Proposition 9.6.3.1.2.
Proofs that would be very nice to be added at some point:
- Properties of pseudomonic functors: Chapter 9: Categories, Proposition 9.7.4.1.2.
- Characterisation of fully faithful functors: Chapter 9: Categories, Item 1 of Proposition 9.6.3.1.2.
- The quadruple adjunction between categories and sets: Chapter 9: Categories, Proposition 9.3.1.1.1.
- $F_{*}$ faithful iff $F$ faithful: Chapter 9: Categories, Item 2 of Proposition 9.6.1.1.2.
- Properties of groupoid completions: Chapter 9: Categories, Proposition 9.4.3.1.3.
- Properties of cores: Chapter 9: Categories, Proposition 9.4.4.1.4.
- $\mathrm{Rel}$ is isomorphic to the category of free algebras of the powerset monad: Chapter 6: Relations, Proposition 6.3.14.1.1.
- Non/existence of left Kan extensions in $\textbf{Rel}$:
- Non/existence of left Kan lifts in $\textbf{Rel}$:
Proofs that would be nice to be added at some point:
- Quotient by an equivalence relation is a coequaliser: Chapter 2: Constructions With Sets, Example 2.2.5.1.4.
- Quotient by an equivalence relation is a coequaliser, repetition: , .
- Properties of posetal categories: Chapter 9: Categories, Proposition 9.2.7.1.2.
- Injective on objects functors are precisely the isocofibrations in $\mathsf{Cats}_{\mathsf{2}}$: Chapter 9: Categories, Item 1 of Proposition 9.8.1.1.2.
- Characterisations of monomorphisms of categories: Chapter 9: Categories, Item 1 of Proposition 9.7.2.1.2.
- Epimorphisms of categories are surjective on objects: Chapter 9: Categories, Item 2 of Proposition 9.7.3.1.2.
- Properties of pseudoepic functors: Chapter 9: Categories, Proposition 9.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 ,\text{pt}\webright )$ is a symmetric bimonoidal category: Chapter 2: Constructions With Sets, Item 14 of Proposition 2.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 ,\text{pt}\webright )$ is a symmetric bimonoidal category: Chapter 3: Monoidal Structures on the Category of Sets, Proposition 3.3.5.1.1.
- Proof that $\webleft (\mathsf{Sets},\times _{X},X\webright )$ is a symmetric monoidal category: Chapter 2: Constructions With Sets, Item 10 of Proposition 2.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 2: Constructions With Sets, Item 5 of Proposition 2.2.3.1.3.
- Proof that $\webleft (\mathsf{Sets},\mathbin {\textstyle \coprod _{X}},X\webright )$ is a symmetric monoidal category: Chapter 2: Constructions With Sets, Item 7 of Proposition 2.2.4.1.6.
Proofs that have been (temporarily) omitted because they are “clear”, “straightforward”, or “tedious”:
-
Properties of products of sets:
- Associativity: Chapter 2: Constructions With Sets, Item 3 of Proposition 2.1.3.1.3.
- Left Unitality: Chapter 2: Constructions With Sets, of Proposition 2.1.3.1.3.
- Right Unitality: Chapter 2: Constructions With Sets, of Proposition 2.1.3.1.3.
- Commutativity: Chapter 2: Constructions With Sets, Item 5 of Proposition 2.1.3.1.3.
- Left Distributivity Over Coproducts: Chapter 2: Constructions With Sets, of Proposition 2.1.3.1.3.
- Right Distributivity Over Coproducts: Chapter 2: Constructions With Sets, of Proposition 2.1.3.1.3.
- Left Annihilation With the Empty Set: Chapter 2: Constructions With Sets, of Proposition 2.1.3.1.3.
- Right Annihilation With the Empty Set: Chapter 2: Constructions With Sets, of Proposition 2.1.3.1.3.
- Symmetric Monoidality: Chapter 2: Constructions With Sets, Item 13 of Proposition 2.1.3.1.3.
- Symmetric Bionoidality: Chapter 2: Constructions With Sets, Item 14 of Proposition 2.1.3.1.3.
-
Properties of coproducts of sets:
- Associativity: Chapter 2: Constructions With Sets, Item 2 of Proposition 2.2.3.1.3.
- Left unitality: Chapter 2: Constructions With Sets, of Proposition 2.2.3.1.3.
- Right unitality: Chapter 2: Constructions With Sets, of Proposition 2.2.3.1.3.
- Commutativity: Chapter 2: Constructions With Sets, Item 4 of Proposition 2.2.3.1.3.
-
Properties of pushouts of sets:
- Associativity: Chapter 2: Constructions With Sets, Item 2 of Proposition 2.2.4.1.6.
- Unitality: Chapter 2: Constructions With Sets, Item 4 of Proposition 2.2.4.1.6.
- Commutativity: Chapter 2: Constructions With Sets, Item 5 of Proposition 2.2.4.1.6.
- Pushout of sets over the empty set recovers the coproduct of sets: Chapter 2: Constructions With Sets, Item 6 of Proposition 2.2.4.1.6.
-
Properties of coequalisers of sets:
- Associativity: Chapter 2: Constructions With Sets, Item 1 of Proposition 2.2.5.1.5.
- Unitality: Chapter 2: Constructions With Sets, Item 2 of Proposition 2.2.5.1.5.
- Commutativity: Chapter 2: Constructions With Sets, Item 3 of Proposition 2.2.5.1.5.
- Interaction with composition: Chapter 2: Constructions With Sets, Item 4 of Proposition 2.2.5.1.5.
- Properties of set differences:
- Complements and characteristic functions: Chapter 2: Constructions With Sets, Item 4 of Proposition 2.3.11.1.2.
-
Properties of symmetric differences:
- Chapter 2: Constructions With Sets, Item 1 of Proposition 2.3.12.1.2.
- Chapter 2: Constructions With Sets, Item 1 of Proposition 2.3.12.1.2.
- Chapter 2: Constructions With Sets, Item 16 of Proposition 2.3.12.1.2.
- Chapter 2: Constructions With Sets, Item 18 of Proposition 2.3.12.1.2.
- Chapter 2: Constructions With Sets, Item 19 of Proposition 2.3.12.1.2.
- The Yoneda lemma for sets: Chapter 2: Constructions With Sets, Proposition 2.5.5.1.1.
- Co/completeness of powersets: Chapter 2: Constructions With Sets, of .
-
Properties of direct images:
- Functoriality: Chapter 2: Constructions With Sets, Item 1 of Proposition 2.6.1.1.4.
- Interaction with coproducts: Chapter 2: Constructions With Sets, Item 15 of Proposition 2.6.1.1.4.
- Interaction with products: Chapter 2: Constructions With Sets, Item 16 of Proposition 2.6.1.1.4.
-
Properties of inverse images:
- Functoriality: Chapter 2: Constructions With Sets, Item 1 of Proposition 2.6.2.1.3.
- Interaction with coproducts: Chapter 2: Constructions With Sets, Item 15 of Proposition 2.6.2.1.3.
- Interaction with products; Chapter 2: Constructions With Sets, Item 16 of Proposition 2.6.2.1.3.
-
Properties of direct images with compact support:
- Functoriality: Chapter 2: Constructions With Sets, Item 1 of Proposition 2.6.3.1.6.
- Lax preservation of colimits: Chapter 2: Constructions With Sets, Item 10 of Proposition 2.6.3.1.6.
- Interaction with coproducts: Chapter 2: Constructions With Sets, Item 14 of Proposition 2.6.3.1.6.
- Interaction with products: Chapter 2: Constructions With Sets, Item 15 of Proposition 2.6.3.1.6.
- 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 3: Monoidal Structures on the Category of Sets, Definition 3.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 3: Monoidal Structures on the Category of Sets, Definition 3.3.2.1.1.
- Left annihilator of $\times $ is a natural isomorphism: Chapter 3: Monoidal Structures on the Category of Sets, Definition 3.3.3.1.1.
- Right annihilator of $\times $ is a natural isomorphism: Chapter 3: Monoidal Structures on the Category of Sets, Definition 3.3.4.1.1.
-
Properties of wedge products of pointed sets:
- Associativity: Chapter 4: Pointed Sets, Item 2 of Proposition 4.3.3.1.2.
- Unitality: Chapter 4: Pointed Sets, Item 3 of Proposition 4.3.3.1.2.
- Commutativity: Chapter 4: Pointed Sets, Item 4 of Proposition 4.3.3.1.2.
- Symmetric monoidality: Chapter 4: Pointed Sets, Item 5 of Proposition 4.3.3.1.2.
-
Properties of pushouts of pointed sets:
- Interaction with coproducts: Chapter 4: Pointed Sets, Item 5 of Proposition 4.3.4.1.2.
- Symmetric monoidality: Chapter 4: Pointed Sets, Item 6 of Proposition 4.3.4.1.2.
-
Properties of free pointed sets:
- Functoriality: Chapter 4: Pointed Sets, Item 1 of Proposition 4.4.1.1.2.
- $\mathrm{Rel}$ with $\times $ is closed symmetric monoidal: Chapter 6: Relations, Proposition 6.2.3.8.1.
-
Properties of graphs:
- Functoriality: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.3.1.1.2.
- Interaction With Inverses: Chapter 7: Constructions With Relations, Item 4 of Proposition 7.3.1.1.2.
-
Properties of inverses of functions (as relations):
- Functoriality: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.3.2.1.2.
- Interaction With Inverses of Relations: Chapter 7: Constructions With Relations, Item 3 of Proposition 7.3.2.1.2.
- Binary unions of relations and inverses: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.3.5.1.2.
- Unions of relations and inverses: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.3.6.1.2.
- Binary Intersections of relations and inverses: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.3.7.1.2.
- Intersections of relations and inverses: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.3.8.1.2.
- Properties of inverses of relations: all items of Chapter 7: Constructions With Relations, Proposition 7.3.11.1.3.
- Properties of composition of relations: some items of Chapter 7: Constructions With Relations, Proposition 7.3.12.1.3.
- Properties of collages of relations: all items of Chapter 7: Constructions With Relations, Proposition 7.3.13.1.2.
-
Properties of direct images of relations:
- Functoriality: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.4.1.1.3.
- Oplax Preservation of Limits: Chapter 7: Constructions With Relations, Item 4 of Proposition 7.4.1.1.3.
-
Properties of strong inverse images of relations:
- Functoriality: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.4.2.1.3.
- Lax Preservation of Colimits: Chapter 7: Constructions With Relations, Item 3 of Proposition 7.4.2.1.3.
-
Properties of weak inverse images of relations:
- Functoriality: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.4.3.1.3.
- Oplax Preservation of Limits: Chapter 7: Constructions With Relations, Item 4 of Proposition 7.4.3.1.3.
-
Properties of direct images with compact support of relations:
- Functoriality: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.4.4.1.3.
- Lax Preservation of Colimits: Chapter 7: Constructions With Relations, Item 3 of Proposition 7.4.4.1.3.
- Functoriality of Powersets II: Chapter 7: Constructions With Relations, Proposition 7.4.6.1.3.
- Proof that the reflexive closure of a relation satisfies the appropriate universal property: Chapter 8: Equivalence Relations and Apartness Relations, Construction 8.1.2.1.2.
- Properties of Symmetric Relations, Chapter 8: Equivalence Relations and Apartness Relations, Proposition 8.2.1.1.4.
- Proof that the symmetric closure of a relation satisfies the appropriate universal property: Chapter 8: Equivalence Relations and Apartness Relations, Construction 8.2.2.1.2.
- Properties of the symmetric closure of a relation:
- Properties of transitive relations, Chapter 8: Equivalence Relations and Apartness Relations, Proposition 8.3.1.1.4.
- Proof that the transitive closure of a relation satisfies the appropriate universal property: Chapter 8: Equivalence Relations and Apartness Relations, Construction 8.3.2.1.2.
- Properties of the transitive closure of a relation:
- Chapter 8: Equivalence Relations and Apartness Relations, of .
- Properties of Quotient Sets, Chapter 8: Equivalence Relations and Apartness Relations, Proposition 8.5.2.1.3: