module Elephant where

Sketching the elephant🔗

Though the 1Lab is not purely a formalization of category theory, it does aim to be a useful reference on the subject. However, the 1Lab organizes content in a highly non-linear fashion; this can make it somewhat difficult to use as a companion to more traditional resources.

This page attempts to (somewhat) rectify this situation by gathering all of the results from “Sketches of an Elephant – A Topos Theory Compendium” (Johnstone 2002) in a single place.¹

A. Toposes as categories🔗

A1 Regular and cartesian closed categories🔗

A1.1 Preliminary assumptions🔗

• Lemma 1.1.1: FG-iso→is-reflective
• Lemma 1.1.2: crude-monadicity
• Lemma 1.1.4: lambek
• Proposition 1.1.7: ∫
• Lemma 1.1.8: Karoubi-is-completion

A1.2 Cartesian Categories🔗

• Lemma 1.2.1:
  1. Finitely-complete→is-finitely-complete
  2. with-equalisers
  3. with-pullbacks

A1.3 Regular Categories🔗

• Proposition 1.3.4: is-strong-epi→is-regular-epi
• Definition 1.3.6: is-congruence

A1.4 Coherent Categories🔗

A1.5 Cartesian closed categories🔗

• Lemma 1.5.2:
  1. (⇐) exponentiable→constant-family⊣product
• Corollary 1.5.3: (⇒) dependent-product→lcc (⇐) lcc→dependent-product

A1.6 Subobject classifiers🔗