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.^{1}

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

### 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:
- 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.

- Proposition 2.2.6:
*Reflectivity*:`Sheafification-is-reflective`

*Completeness*:`Sh[]-is-complete`

*Cocompleteness*:`Sh[]-is-cocomplete`

*Cartesian closure*:`Sh[]-cc`

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.