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🔗

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.