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}$ consists of:

• A type of objects $|\mathcal{C}|:\mathrm{Set}$
• A type of hom-sets $\mathcal{C}[\_,\_]:|\mathcal{C}|\to |\mathcal{C}|\to \mathrm{Set}$
• Identity morphisms: $\mathrm{id}:\forall a\to \mathcal{C}[a,a]$
• Composition: $\circ :\mathcal{C}[b,c]\to \mathcal{C}[a,b]\to \mathcal{C}[a,c]$

Such that:

• $\mathrm{id}$ is a left- and right-Isomorphism of $\circ$
• $\circ$ is associative

Link to original

Concepts

Category

• Category
• Groupoid: Category with only isomorphisms.
• Monoid: Category with a single object.
• Duality (Category Theory): ${\mathcal{C}}^{\mathrm{op}}$ is a category for any category $\mathcal{C}$.

Morphism

• Homset: Morphisms between fixed domain/codomains.
• Endomorphism: Morphisms where dom = cod.
• isos, monos, epis: Kinds of morphisms.

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:

• Limit, colimit
• Terminal, initial objects: Limit and colimit of the empty diagram.
• Products, coproducts: Limit and colimit of diagrams without any (non-identity morphisms).
• Equalizer, Coequalizer: Limit and colimit of
• Pullback, pushout: A limit of a diagram consisting of two morphisms with a common codomain, and its dual.

Adjunctions and Algebras

• 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)$.
• Algebra on an endofunctor
• Algebra over a monad
• Eilenberg-Moore Category
• Monad, and Kleisli Category

Kan Extensions

Kan Extension

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. ↩