Topos.md

Topos

Topos is a category with some properties such that it behaves like sets. So we can do mathematics in such category.

Definitions:

• Elementatry topos is more general, used in logic
• Grothendieck topos (sheaf topos) more specialized for application in geometry - it has natural number object. Adding natural number object to definition of elementary topos gives W-topos

Elementary topos is a category that:

• has finite limits
• is cartesian closed
• has subobject classifier

Resources:

• vpatryshev/Categories Topos Grothendieck Topos, Subobject Classifier, Topology, Lawvere-Tierney topology
• (Agda) agda/agda-categories Topos Subobject Classifier
• (Coq) UniMath/UniMath Grothendieck Topos Subobject Classifier
• (Haskell) brunjlar/protop
• Category Theory for Computing Science - Michael Barr Charles Wells (pdf) Chapter 15 Toposes
• 7Sketches Chapter 7 Logic of behavior: Sheaves, toposes, and internal languages (arxiv), (video 1), (video 2)
• (Category Theory, Haskell) Topoi - Bartosz Milewski (blog post)
• Category Theory: Toposes - MathProofsable (video playlist)
• Computational Quadrinitarianism (Curious Correspondences go Cubical) - Gershom Bazerman (blog post)
• fdilke/bewl (A DSL for the internal language of a topos)
• resources about topos theory
• nLab Topos, Subobject Classifier, Lawvere-Tierney topology