Topos is a category with some properties such that it behaves like sets. So we can do mathematics in such category.
Definitions:
Elementatry toposis more general, used in logicGrothendieck topos (sheaf topos)more specialized for application in geometry - it has natural number object. Adding natural number object to definition of elementary topos givesW-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 (pdf), (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