Seminar series
Date
Fri, 24 Feb 2012
Time
14:00 -
15:30
Location
Comlab
Speaker
Kobi Kremnizer
Organisation
Oxford
In recent years, surprising connections between type theory and homotopy theory have been discovered. In this talk I will recall the notions of intensional type theories and identity types. I will describe "infinity groupoids", formal algebraic models of topological spaces, and explain how identity types carry the structure of an infinity groupoid. I will finish by discussing categorical semantics of intensional type theories.
The talk will take place in Lecture Theatre B, at the Department of Computer Science.