Algebraic type theory
Add to your list(s)
Download to your calendar using vCal
 Steve Awodey, Carnegie Mellon University
 Tuesday 30 August 2022, 14:0015:00
 FW26.
If you have a question about this talk, please contact Jamie Vicary.
A type theoretic universe
E —> U
bears an algebraic structure resulting from the typeforming operations of unit type, identity type, dependent sum, and dependent product,
which may be generalized to form the concept of a “MartinLöf algebra”. A free MLalgebra is then a model of type theory with special properties. The general theory of such MLalgebras can be seen as a proofrelevant version of the theory of ZermeloFraenkel algebras from the algebraic set theory of Joyal & Moerdijk.
(This is work in progress.)
This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.
This talk is included in these lists:
Note that exdirectory lists are not shown.
