Peter LeFanu Lumsdaine: Basic metatheorems for general type theories
Tid: On 2019-03-06 kl 10.00 - 11.45
Plats: Room 16, building 5, Kräftriket, Department of Mathematics, Stockholm University
Medverkande: Peter LeFanu Lumsdaine
Abstract: I will recall the definition of general type theories I presented in October, and look at the proofs of basic fitness-for-purpose metathorems for them — uniqueness of typing, admissibility of substitution, derivability of presuppositions, and so on. In particular, I’ll look at where the proofs of these in wider generality need to differ from their proofs for individual type theories.
(Joint work with Andrej Bauer, Philipp Haselwarter)