We will continue on Thursday, October 11, in M5 at 13.00 by the talk of:
A. Tokarčík
The aim of this lecture is to present the main results of van den Berg's paper "Path categories and propositional identity types," discussing an approach to providing a categorical model for perhaps the most intriguing aspect of intensional MartinLöf type theory, (a variant of) the inductively defined family of identity types. In particular, a precise link between the syntactic category of a type theory with propositional identity types, (Joyal's) tribes with propositional identity types, path tribes and path categories is established. The material will be accompanied by a short introduction to the rules of the type theory and its categorical semantics.
