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 > Logic and Semantics Seminar (Computer Laboratory) > On Proofs of Equality as Paths

## On Proofs of Equality as PathsAdd to your list(s) Download to your calendar using vCal - Andy Pitts, Computer Laboratory
- Friday 07 October 2016, 14:00-15:00
- FW26.
If you have a question about this talk, please contact Dominic Mulligan. In the Type Theoretic approach to mathematical foundations, proofs about properties of mathematical objects can have the same status as the objects themselves. In particular, proofs of equality become mathematical objects that can be studied. The homotopical approach to Type Theory views proofs of equality as paths, possibly in an abstract sense. Taking this view literally, what is required of an interval-like object II in order to give a model of Type Theory in which elements of identity types really are just functions on II? I will discuss this question and introduce a surprisingly simple theory of the interval that suffices to model the recent Coquand-Danielsson axiomatization of propositional identity types. (Joint work with Ian Orton.) This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Cambridge talks
- Computer Laboratory talks
- Computing and Mathematics
- FW26
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsCamtessential Group The Kate Pretty Lecture Experience Islam Week 2008## Other talksOpportunities and Challenges in Generative Adversarial Networks: Looking beyond the Hype Recent Advances in Solid State Batteries and Beyond Li Technologies - Challenges for Fundamental Science Deep supervised level set method: an approach to fully automated segmentation of cardiac MR images in patients with pulmonary hypertension Source-and-Sink Models for Molecular Conduction Back on the Agenda? Industrial Policy revisited Conference Breast cancer - demographics, presentation, diagnosis and patient pathway |