![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Friday 07 October 2016, 14:00-15:00
On Proofs of Equality as Paths
- 👤 Speaker: Andy Pitts, Computer Laboratory 🔗 Website
- 📅 Date & Time: Friday 07 October 2016, 14:00 - 15:00
- 📍 Venue: FW26
Abstract
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.)
Series This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Computing and Mathematics
- Department of Computer Science and Technology talks and seminars
- FW26
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- Martin's interesting talks
- School of Technology
- tcw57’s list
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.