Title :
The groupoid model refutes uniqueness of identity proofs
Author :
Hofmann, Martin ; Streicher, Thomas
Author_Institution :
Dept. of Comput. Sci., Edinburgh Univ., UK
Abstract :
We give a model of intensional Martin-Lof type theory based on groupoids and fibrations of groupoids in which identity types may contain two distinct elements which are not even prepositionally equal. This shows that the principle of uniqueness of identity proofs is not derivable in the syntax
Keywords :
computation theory; formal logic; type theory; fibrations; groupoid model; identity proofs; intensional Martin-Lof type theory; syntax; uniqueness; Computer science; Logic;
Conference_Titel :
Logic in Computer Science, 1994. LICS '94. Proceedings., Symposium on
Conference_Location :
Paris
Print_ISBN :
0-8186-6310-3
DOI :
10.1109/LICS.1994.316071
