Mon, 18 May 2026
16:30
16:30
L5
Algebraic type theory
Steve Awodey
(Carnegie Mellon University)
Abstract
A representable natural transformation u : U* —> U in the category Psh(C) of presheaves on a small category C is a “natural model" of dependent type theory. The type-forming operations may be described as an algebraic structure on u, representing corresponding operations on the type-families classified by u. For example, the dependent product or “Pi-type” is an algebra structure for the polynomial endofunctor
P_u : Psh(C) —> Psh(C) .
Similar operations on u represent the other type-formers of unit type, dependent sums, and identity types. The latter are given by a recently determined “path-type” structure, which relates such models to cubical (Quillen) model categories.
