topos
topos copied to clipboard
Topos theory in lean
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