University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > On Proofs of Equality as Paths

On Proofs of Equality as Paths

Add to your list(s) Download to your calendar using vCal

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2020 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity