Ruy de Queiroz (Universidade Federal de Pernambuco)
In structural proof theory the notion of canonical proof is rather basic, and it is usually taken for granted that a canonical proof of a sentence must be unique up to certain minor syntactical details. When setting up a proof theory for equality one is faced with a somewhat unexpected situation where there may not be a unique canonical proof of an equality statement. Indeed, in a (1994) proposal for the formalisation of proofs of propositional equality in the Curry-Howard style, we have already uncovered such a peculiarity. Totally independently, and in a different setting, Hofmann & Streicher (1994) have shown how to build a model of Martin-Löf's Type Theory (with the so-called Identity Type) in which uniqueness of canonical proofs of identity statements does not hold. The intention here is to show that, by considering proofs of equality as sequences of rewrites and substitution, it comes a rather natural fact that two distinct proofs may be canonical and yet none is to be preferred over the other. By looking at proofs of equality as rewriting (or computational) paths this approach is in line with the recently proposed connections between type theory and homotopy theory via identity types, since elements of identity types will be, concretely, paths (or homotopies), with unbounded iteration of this (paths between paths, etc.). By introducing terms representing paths, the notion of 'paths between paths' becomes rather natural, and thus a syntactical counterpart to the notion of homotopy emerges quite straightforward. Recent results giving a categorical interpretation of identity types as types of computational paths will also be touched upon, time permitting.
Room 6.2.33 [⤴]