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 intervallike 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 CoquandDanielsson 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:
Note that exdirectory lists are not shown.
