Category Theory and Logic

Toposes are 'parallel mathematical universes'. Each topos supports its own mathematics with its own truths. In sheaves on a circle, 'true' means 'true everywhere around the circle'-geometry dictates logic.

• **Programming language semantics:** the denotational semantics of Haskell is a CCC; monads are isomorphic to monads in categories
• **HoTT in Agda/Lean:** identification of isomorphic structures as 'the same' - Voevodsky's univalent foundations of mathematics
• **Functorial databases:** DB schema as a category, data as a functor - schema migrations = natural transformations

Предварительные знания

• Intuitionistic logic
• Type Theory

Categories and Logic: Basic Vocabulary

Haskell's type system is a Cartesian closed category - every function type is an exponential object. JAX's functional transformations (jit, grad, vmap) form a monoidal category with 10M+ daily computations. The Curry-Howard-Lambek correspondence: types = propositions = objects, programs = proofs = morphisms.

A CCC is a category with finite products and exponential objects. Such categories correspond exactly to the simply typed λ-calculus: objects = types, morphisms = programs, exponential B^A = the type A→B.

Toposes and Internal Logic

A topos (Grothendieck, Lawvere, Tierney) is a category that generalizes the category of sets Set. Every topos has an **internal logic**: intuitionistic higher-order logic. Toposes allow doing mathematics in 'non-standard universes'.

In Set, the truth object is {⊤, ⊥} = 2. In an arbitrary topos, Ω can be any object-for instance, the set of open subsets of a topological space. This gives 'intermediate' truth values.

Heyting Algebras and Lattices

A Heyting algebra is the algebraic model of intuitionistic propositional logic. Boolean algebra is a special case. The lattice of open sets of a topological space forms a Heyting algebra, making topology and logic two views of the same thing.

In a Heyting algebra, the operation ¬a = a→0 is called the pseudocomplement. Unlike Boolean algebra, a∨¬a ≠ 1 in general-this is the absence of LEM. Only in complete Boolean algebras does the pseudocomplement coincide with the complement.

Applications: Geometry, Logic, CS

Categorical logic unites algebraic geometry (Grothendieck sheaves), programming language theory (monads, types), and logic (intuitionism). HoTT (Homotopy Type Theory) is the latest synthesis: types = spaces, equality = path.

In Homotopy Type Theory (Voevodsky, 2010), a type A is a topological space. Elements a:A are points. The identity type Id(a,b) is the space of paths from a to b. Equality is not a binary relation but a rich geometric structure.

Key Ideas

• **CCC**: cartesian closed category = STLC; objects=types, morphisms=programs, exponential=function type
• **Topos**: generalizes Set with internal intuitionistic logic; the truth object Ω can be non-trivial
• **Heyting algebra**: algebraic model of intuitionistic logic; Boolean = special case where ¬¬a = a
• **HoTT**: isomorphic types are equal (Univalence); path = identity; a new foundation for mathematics

Related Topics

Categorical logic is a crossroads of algebra, geometry, and logic:

• Intuitionistic Logic — The internal logic of every topos is intuitionistic; Heyting algebras = semantics of IL
• Type Theory (CHI, MLTT) — CCC = STLC; MLTT = LCC (locally cartesian closed categories); HoTT unifies everything
• Model Theory — Topos semantics generalizes model theory; functors as interpretations

Вопросы для размышления

• If every topos defines its own mathematics, in what sense is mathematics 'objective'? Or is truth relative to the chosen topos?
• HoTT declares isomorphic structures equal. What does this change in mathematical practice? Give an example.
• How does the categorical viewpoint ('structures through morphisms, not elements') change the way one think about programs?

Связанные уроки

• plt-07-algebraic-types