Proofs that need to be added at some point:

  1. Chapter 5: Tensor Products of Pointed Sets, Theorem 5.5.10.1.1.
  2. Chapter 5: Tensor Products of Pointed Sets, Theorem 5.5.11.1.1.
  3. Horizontal composition of natural transformations is associative: Chapter 9: Categories, Item 2 of Proposition 9.9.5.1.3.
  4. 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:

  1. Properties of pseudomonic functors: Chapter 9: Categories, Proposition 9.7.4.1.2.
  2. Characterisation of fully faithful functors: Chapter 9: Categories, Item 1 of Proposition 9.6.3.1.2.
  3. The quadruple adjunction between categories and sets: Chapter 9: Categories, Proposition 9.3.1.1.1.
  4. $F_{*}$ faithful iff $F$ faithful: Chapter 9: Categories, Item 2 of Proposition 9.6.1.1.2.
  5. Properties of groupoid completions: Chapter 9: Categories, Proposition 9.4.3.1.3.
  6. Properties of cores: Chapter 9: Categories, Proposition 9.4.4.1.4.
  7. $\mathrm{Rel}$ is isomorphic to the category of free algebras of the powerset monad: Chapter 6: Relations, Proposition 6.3.14.1.1.
  8. Non/existence of left Kan extensions in $\textbf{Rel}$:
    1. Chapter 7: Constructions With Relations, Item 1 of Proposition 7.2.1.1.1.
    2. Chapter 7: Constructions With Relations, Item 2 of Proposition 7.2.1.1.1.
  9. Non/existence of left Kan lifts in $\textbf{Rel}$:
    1. Chapter 7: Constructions With Relations, Item 1 of Proposition 7.2.2.1.1.
    2. Chapter 7: Constructions With Relations, Item 2 of Proposition 7.2.2.1.1.

Proofs that would be nice to be added at some point:

  1. Quotient by an equivalence relation is a coequaliser: Chapter 2: Constructions With Sets, Example 2.2.5.1.4.
  2. Quotient by an equivalence relation is a coequaliser, repetition: , .
  3. Properties of posetal categories: Chapter 9: Categories, Proposition 9.2.7.1.2.
  4. 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.
  5. Characterisations of monomorphisms of categories: Chapter 9: Categories, Item 1 of Proposition 9.7.2.1.2.
  6. Epimorphisms of categories are surjective on objects: Chapter 9: Categories, Item 2 of Proposition 9.7.3.1.2.
  7. 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:

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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”:

  1. Properties of products of sets:
    1. Associativity: Chapter 2: Constructions With Sets, Item 3 of Proposition 2.1.3.1.3.
    2. Left Unitality: Chapter 2: Constructions With Sets, of Proposition 2.1.3.1.3.
    3. Right Unitality: Chapter 2: Constructions With Sets, of Proposition 2.1.3.1.3.
    4. Commutativity: Chapter 2: Constructions With Sets, Item 5 of Proposition 2.1.3.1.3.
    5. Left Distributivity Over Coproducts: Chapter 2: Constructions With Sets, of Proposition 2.1.3.1.3.
    6. Right Distributivity Over Coproducts: Chapter 2: Constructions With Sets, of Proposition 2.1.3.1.3.
    7. Left Annihilation With the Empty Set: Chapter 2: Constructions With Sets, of Proposition 2.1.3.1.3.
    8. Right Annihilation With the Empty Set: Chapter 2: Constructions With Sets, of Proposition 2.1.3.1.3.
    9. Symmetric Monoidality: Chapter 2: Constructions With Sets, Item 13 of Proposition 2.1.3.1.3.
    10. Symmetric Bionoidality: Chapter 2: Constructions With Sets, Item 14 of Proposition 2.1.3.1.3.
  2. Properties of coproducts of sets:
    1. Associativity: Chapter 2: Constructions With Sets, Item 2 of Proposition 2.2.3.1.3.
    2. Left unitality: Chapter 2: Constructions With Sets, of Proposition 2.2.3.1.3.
    3. Right unitality: Chapter 2: Constructions With Sets, of Proposition 2.2.3.1.3.
    4. Commutativity: Chapter 2: Constructions With Sets, Item 4 of Proposition 2.2.3.1.3.
  3. Properties of pushouts of sets:
    1. Associativity: Chapter 2: Constructions With Sets, Item 2 of Proposition 2.2.4.1.6.
    2. Unitality: Chapter 2: Constructions With Sets, Item 4 of Proposition 2.2.4.1.6.
    3. Commutativity: Chapter 2: Constructions With Sets, Item 5 of Proposition 2.2.4.1.6.
    4. 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.
  4. Properties of coequalisers of sets:
    1. Associativity: Chapter 2: Constructions With Sets, Item 1 of Proposition 2.2.5.1.5.
    2. Unitality: Chapter 2: Constructions With Sets, Item 2 of Proposition 2.2.5.1.5.
    3. Commutativity: Chapter 2: Constructions With Sets, Item 3 of Proposition 2.2.5.1.5.
    4. Interaction with composition: Chapter 2: Constructions With Sets, Item 4 of Proposition 2.2.5.1.5.
  5. Properties of set differences:
    1. Chapter 2: Constructions With Sets, Item 4 of Proposition 2.3.10.1.2.
    2. Chapter 2: Constructions With Sets, Item 11 of Proposition 2.3.10.1.2.
    3. Chapter 2: Constructions With Sets, Item 15 of Proposition 2.3.10.1.2.
  6. Complements and characteristic functions: Chapter 2: Constructions With Sets, Item 4 of Proposition 2.3.11.1.2.
  7. Properties of symmetric differences:
    1. Chapter 2: Constructions With Sets, Item 1 of Proposition 2.3.12.1.2.
    2. Chapter 2: Constructions With Sets, Item 1 of Proposition 2.3.12.1.2.
    3. Chapter 2: Constructions With Sets, Item 16 of Proposition 2.3.12.1.2.
    4. Chapter 2: Constructions With Sets, Item 18 of Proposition 2.3.12.1.2.
    5. Chapter 2: Constructions With Sets, Item 19 of Proposition 2.3.12.1.2.
  8. The Yoneda lemma for sets: Chapter 2: Constructions With Sets, Proposition 2.5.5.1.1.
  9. Co/completeness of powersets: Chapter 2: Constructions With Sets, of .
  10. Properties of direct images:
    1. Functoriality: Chapter 2: Constructions With Sets, Item 1 of Proposition 2.6.1.1.4.
    2. Interaction with coproducts: Chapter 2: Constructions With Sets, Item 15 of Proposition 2.6.1.1.4.
    3. Interaction with products: Chapter 2: Constructions With Sets, Item 16 of Proposition 2.6.1.1.4.
  11. Properties of inverse images:
    1. Functoriality: Chapter 2: Constructions With Sets, Item 1 of Proposition 2.6.2.1.3.
    2. Interaction with coproducts: Chapter 2: Constructions With Sets, Item 15 of Proposition 2.6.2.1.3.
    3. Interaction with products; Chapter 2: Constructions With Sets, Item 16 of Proposition 2.6.2.1.3.
  12. Properties of direct images with compact support:
    1. Functoriality: Chapter 2: Constructions With Sets, Item 1 of Proposition 2.6.3.1.6.
    2. Lax preservation of colimits: Chapter 2: Constructions With Sets, Item 10 of Proposition 2.6.3.1.6.
    3. Interaction with coproducts: Chapter 2: Constructions With Sets, Item 14 of Proposition 2.6.3.1.6.
    4. Interaction with products: Chapter 2: Constructions With Sets, Item 15 of Proposition 2.6.3.1.6.
  13. 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.
  14. 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.
  15. Left annihilator of $\times $ is a natural isomorphism: Chapter 3: Monoidal Structures on the Category of Sets, Definition 3.3.3.1.1.
  16. Right annihilator of $\times $ is a natural isomorphism: Chapter 3: Monoidal Structures on the Category of Sets, Definition 3.3.4.1.1.
  17. Properties of wedge products of pointed sets:
    1. Associativity: Chapter 4: Pointed Sets, Item 2 of Proposition 4.3.3.1.2.
    2. Unitality: Chapter 4: Pointed Sets, Item 3 of Proposition 4.3.3.1.2.
    3. Commutativity: Chapter 4: Pointed Sets, Item 4 of Proposition 4.3.3.1.2.
    4. Symmetric monoidality: Chapter 4: Pointed Sets, Item 5 of Proposition 4.3.3.1.2.
  18. Properties of pushouts of pointed sets:
    1. Interaction with coproducts: Chapter 4: Pointed Sets, Item 5 of Proposition 4.3.4.1.2.
    2. Symmetric monoidality: Chapter 4: Pointed Sets, Item 6 of Proposition 4.3.4.1.2.
  19. Properties of free pointed sets:
    1. Functoriality: Chapter 4: Pointed Sets, Item 1 of Proposition 4.4.1.1.2.
  20. $\mathrm{Rel}$ with $\times $ is closed symmetric monoidal: Chapter 6: Relations, Proposition 6.2.3.8.1.
  21. Properties of graphs:
    1. Functoriality: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.3.1.1.2.
    2. Interaction With Inverses: Chapter 7: Constructions With Relations, Item 4 of Proposition 7.3.1.1.2.
  22. Properties of inverses of functions (as relations):
    1. Functoriality: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.3.2.1.2.
    2. Interaction With Inverses of Relations: Chapter 7: Constructions With Relations, Item 3 of Proposition 7.3.2.1.2.
  23. Binary unions of relations and inverses: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.3.5.1.2.
  24. Unions of relations and inverses: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.3.6.1.2.
  25. Binary Intersections of relations and inverses: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.3.7.1.2.
  26. Intersections of relations and inverses: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.3.8.1.2.
  27. Properties of inverses of relations: all items of Chapter 7: Constructions With Relations, Proposition 7.3.11.1.3.
  28. Properties of composition of relations: some items of Chapter 7: Constructions With Relations, Proposition 7.3.12.1.3.
  29. Properties of collages of relations: all items of Chapter 7: Constructions With Relations, Proposition 7.3.13.1.2.
  30. Properties of direct images of relations:
    1. Functoriality: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.4.1.1.3.
    2. Oplax Preservation of Limits: Chapter 7: Constructions With Relations, Item 4 of Proposition 7.4.1.1.3.
  31. Properties of strong inverse images of relations:
    1. Functoriality: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.4.2.1.3.
    2. Lax Preservation of Colimits: Chapter 7: Constructions With Relations, Item 3 of Proposition 7.4.2.1.3.
  32. Properties of weak inverse images of relations:
    1. Functoriality: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.4.3.1.3.
    2. Oplax Preservation of Limits: Chapter 7: Constructions With Relations, Item 4 of Proposition 7.4.3.1.3.
  33. Properties of direct images with compact support of relations:
    1. Functoriality: Chapter 7: Constructions With Relations, Item 1 of Proposition 7.4.4.1.3.
    2. Lax Preservation of Colimits: Chapter 7: Constructions With Relations, Item 3 of Proposition 7.4.4.1.3.
  34. Functoriality of Powersets II: Chapter 7: Constructions With Relations, Proposition 7.4.6.1.3.
  35. 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.
  36. Properties of Symmetric Relations, Chapter 8: Equivalence Relations and Apartness Relations, Proposition 8.2.1.1.4.
  37. 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.
  38. Properties of the symmetric closure of a relation:
    1. Chapter 8: Equivalence Relations and Apartness Relations, Item 2 of Proposition 8.2.2.1.3.
    2. Chapter 8: Equivalence Relations and Apartness Relations, Item 4 of Proposition 8.2.2.1.3.
  39. Properties of transitive relations, Chapter 8: Equivalence Relations and Apartness Relations, Proposition 8.3.1.1.4.
  40. 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.
  41. Properties of the transitive closure of a relation:
    1. Chapter 8: Equivalence Relations and Apartness Relations, Item 2 of Proposition 8.3.2.1.3.
  42. Chapter 8: Equivalence Relations and Apartness Relations, of .
  43. Properties of Quotient Sets, Chapter 8: Equivalence Relations and Apartness Relations, Proposition 8.5.2.1.3:
    1. Chapter 8: Equivalence Relations and Apartness Relations, Item 1 of Proposition 8.5.2.1.3.
    2. Chapter 8: Equivalence Relations and Apartness Relations, Item 2 of Proposition 8.5.2.1.3.
    3. Chapter 8: Equivalence Relations and Apartness Relations, Item 3 of Proposition 8.5.2.1.3.


Noticed something off, or have any comments? Feel free to reach out!


You can also use the contact form below: