Thierry Coquand: A model of Type Theory in cubical sets
Thierry Coquand, Göteborg
Tid: On 2013-10-30 kl 10.00 - 11.45
Plats: Room 16, building 5, Kräftriket, Department of mathematics, Stockholm university
We present a model of Type Theory where a type is interpreted as a cubical set satisfying the Kan condition. This can be seen both as a refinement of Bishop's definition of a set as a collection with an equivalence relation and as a constructive version of Voevodsky's Kan simplicial set model. We use cubical sets with non ordered dimensions, and explain the connection with the notion of nominal sets. Finally, we show how to use this model to give a new explanation of the axiom of description.