skip to content

Using Agda to Explore Path-Oriented Models of Type Theory

Presented by: 
Andrew Pitts
Tuesday 27th June 2017 - 13:30 to 14:30
INI Seminar Room 2
Homotopy Type Theory (HoTT) has re-invigorated research into the theory and applications of the intensional version of Martin-Löf typetheory. On the one hand, the language of type theory helps to express synthetic constructions and arguments in homotopy theory and higher-dimensional category theory. On the other hand, the geometric and algebraic insights of those highly developed branches of mathematics shed new light on logical and type-theoretic notions. In particular, HoTT takes a path-oriented view of intensional (i.e.proof-relevant) equality: proofs of equality of two elements of a type x,y : A, i.e. elements of a Martin-Löf identity type Id_A x y, behave analogously to paths between two points x, y in a space A. The complicated internal structure of intensional identity types relatesto the homotopy classes of path spaces. To make this analogy preciseand to exploit it, it helps to have a wide range of models ofintensional type theory that embody this path-oriented view ofequality in some way.In this talk I will describe some recent work on path-oriented modelsof type theory carried out with my student Ian Orton and making use of the Agda theorem-prover. I will try to avoid technicalities in favourof describing why Agda in "unsafe" mode is so useful to us while wecreate new mathematics, rather than verifying existing mathematical theorems; and also describe some limitations of Agda (to do with quotient types) in the hope that the audience will tell me about a prover without those limitations. I also want to make some comments about mathematical knowledge representation as it relates to my search, as a homotopical ignoramus, for knowledge that will help in the construction of models of HoTT.
Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons