Toposes and Univalent Foundations

Two categorical lenses on the foundations of mathematics. A topos is a category that behaves enough like to interpret logic inside itself; univalent foundations is a type-theoretic stance in which the identity of two objects is an equivalence between them. Both replace a fixed set-theoretic universe with a structured category whose internal language is the object of study.

Definition of an (elementary) topos

A topos is a category with finite limits, exponentials, and a subobject classifier , so that subobjects of correspond to maps and the internal logic is at least intuitionistic. Grothendieck toposes are categories of sheaves; the reference points are Sheaves in Geometry and Logic for the geometric side and the first-order categorical logic of Makkai–Reyes for the model-theoretic side.

Remark on univalence and proofs as objects

Univalent foundations reads as the type of equivalences , so equal things are exactly interchangeable things. Turned toward proof, this invites a “proofs as objects” reading. An atomic proof is an inference rule, a single given spider connecting hypotheses to a conclusion. A derivation is a composite . The reasoning about which composites are admissible is carried out one level up, at the meta level.