COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Using Agda to Explore Path-Oriented Models of Type Theory

## Using Agda to Explore Path-Oriented Models of Type TheoryAdd 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. |
## Other listsC2AD seminar Series Lord Martin Rees: “Looking towards 2050” Bio-Inspired Robotics Lab (BIRL) Seminar Series FERSA Workshops Darwin Society (Christ's) Oliver Wyman lecture : "The economic outlook: The news behind the headlines"## Other talksHornby Model Railways Reconciling centennial-scale climate variation during the last millennium in reconstructions and simulations St Catharine’s Political Economy Seminar - ‘Technological Unemployment: Myth or Reality’ by Robert Skidelsky How archaeologists resolve the inductive risk argument CGHR Practitioner Series: Andrea Coomber, JUSTICE MEASUREMENT SYSTEMS AND INSTRUMENTATION IN THE OIL AND GAS INDUSTRY |