Topos theory for Lean

This repository contains formal verification of results in Topos Theory, drawing from "Sheaves in Geometry and Logic" and "Sketches of an Elephant".

What's here?

Cartesian closed categories
Sieves and grothendieck topologies including the open set topology
(Trunc) construction of finite products from binary products and terminal
Locally cartesian closed categories and epi-mono factorisations
Many lemmas about pullbacks (for instance the pasting lemma)
Skeleton of a category (assuming choice)
Subobject category
Subobject classifiers and power objects
Reflexive monadicity theorem
(Internal) Beck-Chevalley and Pare's theorem
Definition of a topos
Every topos is finitely cocomplete
Local cartesian closure of toposes and Fundamental Theorem of Topos Theory
Lawvere-Tierney topologies and sheaves
Sheafification of LT topologies
Proof that Lawvere-Tierney topologies generalise Grothendieck topologies

What's coming soon?

Proof that category of coalgebras for a comonad form a topos
Logical functors
Logic internal to a topos
Natural number objects

What might be coming?

Geometric morphisms
Filter/quotient construction on a topos
ETCS
The construction of the Cohen topos to show ZF doesn't prove CH
The construction of a topos to show ZF doesn't prove AC
A topos in which every function R -> R is continuous
Giraud's theorem
Classifying toposes

Build Instructions

EITHER: Install lean and leanproject.

OR: If you have docker, spin up an instance of the edayers/lean image (or build your own using the provided Dockerfile).

FINALLY: run

leanproject get b-mehta/topos
leanproject build