Geometric Type Theory, Done Two Ways
A topos can be specified by the geometric theory that it classifies. Though the sequents of a theory are described formally and syntactically, its interaction with the world of sets (through set-indexed disjunctions and axiom schemas) is often a little hand-wavy. In this post I describe two ways…




















![The map of mathematics [Source]](../../blog/2023-01-05-preparing-for-networked-mathematics/map.jpg)








![The cohort of Em-Cats speakers and their talk titles/topics. [PDF]](../../blog/2021-08-24-em-cats-announcement/em-cats-poster.png)



