Category Theory Illustrated – Types (abuseofnotation.github.io)

The article explains how “types” serve as an alternative foundation for mathematics by preventing Russell’s paradox from arising. It contrasts set theory (notably ZFC) with Russell’s type theory, emphasizing that terms are restricted to specific types, which blocks self-containing constructions. It also situates types within category-theoretic thinking by framing types as the sources and targets of functions (arrows) and notes that there are many related type-theory formulations (type systems).