Skip to main content

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

Lecturer: 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)