On Proofs of Equality as Paths

Add 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
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• 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.