Mirqāt The Ascent of Logic

Specialized · a field of logic

Category Theory

Objects and arrows, toposes and type theory: an abstract language for structure, and an alternative foundation for mathematics.

The problem
Can mathematics be founded on structure and transformation (arrows) rather than on membership in sets?
The turning point
The Curry–Howard–Lambek correspondence: proofs, programs, and arrows in a cartesian-closed category are one and the same.
An open question
How far can ∞-categories and topos theory serve as the working foundation for everyday mathematics?

The Canon

  • Mac Lane Categories for the Working Mathematician 1971
  • Lawvere & Schanuel Conceptual Mathematics
  • Martin-Löf Intuitionistic Type Theory 1984

To study it

  • Awodey Category Theory
  • Goldblatt Topoi: The Categorial Analysis of Logic