open import Cat.Instances.Elements.Covariant
open import Cat.Site.Instances.Canonical
open import Cat.CartesianClosed.Locally
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” in a single place.1

A. Toposes as categories🔗

A1 Regular and cartesian closed categories🔗

A1.1 Preliminary assumptions🔗

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


A1.2 Cartesian Categories🔗

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


A1.3 Regular Categories🔗

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


A1.5 Cartesian closed categories🔗

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


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


C2.2 The topos of sheaves🔗

See topos of sheaves.

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


1. It also serves as an excellent place to find possible contributions!↩︎

References

• Johnstone, Peter T. 2002. Sketches of an Elephant: a Topos Theory Compendium. Oxford Logic Guides. New York, NY: Oxford Univ. Press. https://cds.cern.ch/record/592033.