open import Cat.Instances.Elements.Covariant
open import Cat.Functor.Adjoint.Reflective
open import Cat.Site.Instances.Canonical
open import Cat.CartesianClosed.Locally
open import Cat.Functor.Monadic.Crude
open import Cat.Diagram.Limit.Finite
open import Cat.Diagram.Exponential
open import Cat.Diagram.Congruence
open import Cat.Instances.Karoubi
open import Cat.Instances.Sheaves
open import Cat.Functor.Algebra
open import Cat.Site.Closure
open import Cat.Site.Base
open import Cat.Regular

open import Topoi.Base

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🔗

_ = FG-iso→is-reflective
_ = crude-monadicity
_ = ∫
_ = Karoubi-is-completion
_ = lambek

• 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🔗

_ = Finitely-complete→is-finitely-complete
_ = with-equalisers
_ = with-pullbacks

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

A1.3 Regular Categories🔗

_ = is-strong-epi→is-regular-epi
_ = is-congruence

• 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🔗

_ = exponentiable→constant-family⊣product
_ = dependent-product→lcc
_ = lcc→dependent-product

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

A1.6 Subobject classifiers🔗

C Toposes as spaces🔗

C2 Sheaves on a site🔗

C2.1 Sites and coverages🔗

_ = Coverage
_ = Patch
_ = is-separated₁
_ = is-sheaf
_ = is-separated
_ = is-sheaf-maximal
_ = is-sheaf-factor
_ = is-sheaf-transitive
_ = is-colim
_ = is-universal-colim

• Definition 2.1.1: Coverage
• Definition 2.1.2:
  • Compatible families: Patch
  • Separated presheaves: is-separated₁
  • Sheaves on a site: is-sheaf, is-separated
• Lemma 2.1.5: is-sheaf-maximal
• Lemma 2.1.6: is-sheaf-factor
• Lemma 2.1.7: is-sheaf-transitive, though see the warning there.
• Example 2.1.12, (universally) effective-epimorphic sieves: is-colim, is-universal-colim

C2.2 The topos of sheaves🔗

See topos of sheaves.

_ = Sheafification-is-reflective
_ = Sh[]-is-complete
_ = Sh[]-is-cocomplete
_ = Sh[]-cc

• Proposition 2.2.6:
  • Reflectivity: Sheafification-is-reflective
  • Completeness: Sh[]-is-complete
  • Cocompleteness: Sh[]-is-cocomplete
  • Cartesian closure: Sh[]-cc