Till innehåll på sidan

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

Exportera till kalender

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)