Propositional equality, identity types, and direct computational paths

Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira

In 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 syntactic…