Peter LeFanu Lumsdaine: Logical structure on comprehension categories, part 2
Tid: On 2016-08-31 kl 10.00 - 11.45
Plats: Room 16, building 5, Kräftriket, Department of Mathematics, Stockholm University
Medverkande: Peter LeFanu Lumsdaine
Abstract: Continuing from last week’s seminar, I will use the 2-categorical setting to define a general notion of *rules* and *logical structure* on comprehension categories — general enough to cover most (?all) standard logical constructors of dependent type theory, but (hopefully) specialised enough to still admit various standard constructions and meta-theorems.