Department of

October 2013 November 2013 December 2013 Su Mo Tu We Th Fr Sa Su Mo Tu We Th Fr Sa Su Mo Tu We Th Fr Sa 1 2 3 4 5 1 2 1 2 3 4 5 6 7 6 7 8 9 10 11 12 3 4 5 6 7 8 9 8 9 10 11 12 13 14 13 14 15 16 17 18 19 10 11 12 13 14 15 16 15 16 17 18 19 20 21 20 21 22 23 24 25 26 17 18 19 20 21 22 23 22 23 24 25 26 27 28 27 28 29 30 31 24 25 26 27 28 29 30 29 30 31

Tuesday, November 12, 2013

**Abstract:** Every category C looks locally like a category of sets and further structure on C determines what logic one can use to reason about these ``sets''. For example, if C is a topos, one can use full (higher order) intuitionistic logic. Similarly, one expects that every $\infty$-category looks locally like an $\infty$-category of spaces. A natural question then is: what sort of logic can we use to reason about these ``spaces''? It has been conjectured that such logics are provided by variants of Homotopy Type Theory, a formal logical system, recently proposed as a foundation of mathematics by Vladimir Voevodsky. After explaining the necessary background, I will report on the progress towards this conjecture.