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 listsFuture of Sentience CAPE-CIKC Advanced Technology Lectures Meeting the Challenge of Healthy Ageing in the 21st Century## Other talksThe Weaponisation of Human Rights MicroRNAs as circulating biomarkers in cancer Title: Lynch Syndrome Jerrard Hayes - Title to Be Confirmed Julia Guarneri Book Launch: Newsprint Metropolis: City Papers and the Making of Modern Americans "Intestinal epithelial cells: at the interface of the microbiota and mucosal immunity" |