• DocumentCode
    1996341
  • Title

    The groupoid model refutes uniqueness of identity proofs

  • Author

    Hofmann, Martin ; Streicher, Thomas

  • Author_Institution
    Dept. of Comput. Sci., Edinburgh Univ., UK
  • fYear
    1994
  • fDate
    4-7 Jul 1994
  • Firstpage
    208
  • Lastpage
    212
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 1994. LICS '94. Proceedings., Symposium on
  • Conference_Location
    Paris
  • Print_ISBN
    0-8186-6310-3
  • Type

    conf

  • DOI
    10.1109/LICS.1994.316071
  • Filename
    316071
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=1996341