Seminář z Algebry - 11.10.2018 |

We will continue on Thursday, October 11, in M5 at 13.00 by the talk of: ## A. TokarčíkThe 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 Martin-Lö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. |

Aktualizováno Pondělí, 08 Říjen 2018 15:26 |