Seminar series
Date
Mon, 18 May 2026
16:30
16:30
Location
L5
Speaker
Steve Awodey
Organisation
Carnegie Mellon University
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.