Category Theory

Abstract

Category theory is a mathematical framework for studying structures and their relationships. It abstracts specific mathematical contexts (e.g., sets, groups, topological spaces) into systems of objects and morphisms. It provides the language for HoTT through categorical semantics and serves as a foundation for understanding type theories as categories. Riehl describes category theory as the “study of mathematical analogy”. ¹

Definition

A category $\mathcal{C}$ is made up of:

• A type of objects $|\mathcal{C}|:\mathrm{Set}$
• A type of hom-sets ($\mathcal{C}[\_,\_]:|\mathcal{C}|\to |\mathcal{C}|\to \mathrm{Set}$)
• $\mathrm{id}:\forall a\to \mathcal{C}[a,a]$ identity morphism
• $\circ :\mathcal{C}[b,c]\to \mathcal{C}[a,b]\to \mathcal{C}[a,c]$ composition operator Such that,
• ${\mathrm{id}}_a$ is a left- and right-inverse of $\circ$.
• $\circ$ is associative.

Link to original

Core Concepts

Functors and Natural Transformations

• Functor: A mapping between categories $F:\mathcal{C}\to \mathcal{D}$ that preserves composition and identities.
• Natural Transformation: A way of transforming one functor into another while preserving the categorical structure.
• Equivalence of Categories: A notion of “sameness” for categories that is weaker than isomorphism, requiring a natural isomorphism between compositions and identities.

Limits and Colimits

These generalize universal constructions:

• Terminal Object: An object $1$ such that for every object $X$, there is a unique morphism $X\to 1$.
• Products: Generalization of cartesian products $A\times B$.
• equalizer: Categorical generalization of the set of elements where two functions agree.
• pullback: A limit of a diagram consisting of two morphisms with a common codomain.

Adjunctions

An adjunction between functors $F:\mathcal{C}\to \mathcal{D}$ and $G:\mathcal{D}\to \mathcal{C}$ is a natural isomorphism $ho{m}_{\mathcal{D}}(FA,B)\cong ho{m}_{\mathcal{C}}(A,GB)$. Adjunctions can capture the notion of most efficient solutions to optimization problems in mathematics. [^3]

Categorical Logic and Type Theory

The correspondence between categories and type theories allows for geometric and algebraic reasoning about logic:

Category Theory	Type Theory
Category	Type System / Context
Object	Type
Morphism	Term / Program
Product	Product Type
Exponential Object	Function Type
Subobject Classifier	Prop / Truth Values

Cartesian Closed Category (CCC)

A category with a terminal object, binary products, and exponentials. CCCs provide the categorical semantics for the Simply-Typed Lambda Calculus.

Topos Theory

A topos is a category that behaves like the Set and possesses a Subobject Classifier. Elementary topoi serve as models for Intuitionistic Logic.

Higher Category Theory

n-Categories

Generalizations where morphisms exist between morphisms (2-morphisms), and so on.

Weak Infinity Groupoid

In Homotopy Type Theory, types are viewed as $\infty$-groupoids, where all $n$-morphisms are invertible up to a higher morphism.

Model Category

A category equipped with three classes of morphisms (weak equivalences, fibrations, and cofibrations) used to perform Homotopy Theory.

Models

• Categorical Model of Type Theory: Interpretation of types as objects.
• Presheaf: Functors $F:{\mathcal{C}}^{op}\to Set$ used to build models of Cubical Type Theory.
• Categorical Interpretation of Identity: Identity types correspond to path objects or factorizations in a model category.

History

• Foundations (1945): Samuel Eilenberg and Saunders Mac Lane introduced categories, functors, and natural transformations in General Theory of Natural Equivalences.
• Adjoint Functor (1958): Daniel Kan formulated adjunctions, identifying them as a central theme in mathematics.
• Elementary Topos (1960s): William Lawvere and Miles Tierney axiomatized topoi, linking geometry and logic.
• Higher Category Theory (1990s-Present): Development of $(\infty ,1)$-categories by Joyal and Jacob Lurie, providing the machinery for Homotopy Type Theory.

Resources

• Categories for the Working Mathematician
• Prof. Thorsten Altenkirch’s lecture notes: Categories for the Lazy Functional Programmer - type theoretic view of categories
• Topoi - Goldblatt
• Category Theory in Context by Emily Riehl - providing motivation through analogy
• Basic Category Theory by Tom Leinster
• Higher Topos Theory by Jacob Lurie
• Sheaves in Geometry and Logic by Saunders Mac Lane and Leke Moerdijk

References

maclane1978-categories awodey2010-category-theory riehl2016-category-theory goldblatt2006-topoi leinster2014-basic-category-theory lurie2009-higher-topos-theory

Footnotes

1. Citation needed. ↩