Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Ninth Annual IEEE Symposium on

Logic in Computer Science (LICS 1994)

Paper: The groupoid model refutes uniqueness of identity proofs (at LICS 1994)

Winner of the Test-of-Time Award in 2014
Authors: Martin Hofmann Thomas Streicher

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

BibTeX

  @InProceedings{HofmannStreicher-Thegroupoidmodelref,
    author = 	 {Martin Hofmann and Thomas Streicher},
    title = 	 {The groupoid model refutes uniqueness of identity proofs},
    booktitle =  {Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994)},
    year =	 {1994},
    month =	 {July}, 
    pages =      {208--212},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2017-04-0512:37
Andrzej Murawski