Links und Funktionen
Sprachumschaltung

Navigationspfad
You are here: Home / Publikationen / The Groupoid Model Refutes Uniqueness of Identity Proofs


Inhaltsbereich

Martin Hofmann and Thomas Streicher (1994)

The Groupoid Model Refutes Uniqueness of Identity Proofs

In: LICS, pp. 208-212.

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.

Document Actions


Funktionsleiste