Logic Seminar - Jesse Sigal
| Dates: | 18 March 2026 |
|---|
| Times: | 15:00 - 16:00 |
|---|
| What is it: | Seminar |
|---|
| Organiser: | Department of Mathematics |
|---|
| Who is it for: | University staff, External researchers, Current University students |
|---|
|
Speaker: Jesse Sigal (University of Edinburgh)
Title: How not to choose in the semantics of dependent types
Abstract: Many constructions in the semantics of logics and programming languages involve universal properties. These universal constructions allow us not to care about the choice of "implementation", the universal property alone is sufficient. However, in order to define a standard semantics of a logic or language, we must actually choose a universal arrow for each type to make a model. For example, interpreting the simply-typed lambda calculus requires chosen products and exponentials. Intuitively, a choice of universal objects shouldn't matter. Makkai formally showed in "Avoiding the axiom of choice in general category theory" (1996) that this intuition is correct for simply-typed lambda calculus.
We extend Makkai's work to the comprehension category semantics of extensional Martin-Löf dependent type theory, although we do not fret over avoiding the axiom of choice nor size issues.
Travel and Contact Information
Find event
Frank Adams 1
Alan Turing Building
Manchester
