skip to content

Using Agda to Explore Path-Oriented Models of Type Theory

Presented by: 
Andrew Pitts University of Cambridge
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.
The video for this talk should appear here if JavaScript is enabled.
If it doesn't, something may have gone wrong with our embedded player.
We'll get it fixed as soon as possible.
Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons