Peter LeFanu Lumsdaine: Basic metatheorems for general type theories
Time: Wed 2019-03-06 10.00 - 11.45
Location: Room 16, building 5, Kräftriket, Department of Mathematics, Stockholm University
Participating: 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)