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 info@newton.ac.uk. 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. 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
Note that ex-directory lists are not shown. |
## Other listsFERSA 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 |