Using Agda to Explore Path-Oriented Models of Type Theory

Add to your list(s) Download to your calendar using vCal

• Andrew Pitts (University of Cambridge)
• Tuesday 27 June 2017, 13:30-14:30
• Seminar Room 2, Newton Institute.

If you have a question about this talk, please contact INI IT.

BPR - Big proof

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.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 2, Newton Institute
• bld31

Note that ex-directory lists are not shown.