Peter LeFanu Lumsdaine: Basic metatheorems for general type theories

Tid: On 2019-03-06 kl 10.00 - 11.45

Föreläsare: Peter LeFanu Lumsdaine

Plats: Room 16, building 5, Kräftriket, Department of Mathematics, Stockholm University

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)

Tillhör: Institutionen för matematik
Senast ändrad: 2019-03-01