Logic in Computer Science (LICS 1994)

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

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 Symp. on Logic in Computer Science, {LICS} 1994},
    year =	 1994,
    editor =	 {Samson Abramsky},
    month =	 {July}, 
    pages =      {208--212},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}
  }