axiom UIP

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** =

**propositions as types** +**programs as proofs** +**relation type theory/category theory**

In type theory what is called the *UIP axiom*, the axiom of *uniqueness of identity proofs* is an axiom that when added to intensional type theory turns it into a propositionally extensional type theory.

The axiom asserts that any two terms of the same identity type $Id_A(x,y)$ are themselves propositionally equal (in the corresponding higher identity type).

This is contrary to the univalence axiom, which makes sense only in the absence of UIP.

The *UIP axiom* (for types in a universe “$Type$”) posits that the type

$\underset{A \colon Type}{\prod}
\underset{x,y \colon A}{\prod}
\underset{p,q \colon Id_A(x,y)}{\prod}
Id_{Id_A(x,y)}(p,q)$

has a term. In other words, we add to our type theory the rule

$\frac{}{
\vdash uip
\colon
\underset{A \colon Type}{\prod}
\underset{x,y \colon A}{\prod}
\underset{p,q \colon Id_A(x,y)}{\prod}
Id_{Id_A(x,y)}(p,q)}$

We can modify this by making the hypotheses of the axiom into premises of the rule, if we wish. In particular, this can be used to give a version of the rule that applies to all types not necessarily belonging to some fixed universe, using the judgment “$A\;type$” for “$A$ is a type” (as distinguished from “$A:Type$” for “$A$ belongs to the universe type $Type$”).

$\frac{\Gamma\vdash A\; type \quad \Gamma\vdash x : A \quad \Gamma \vdash y:A \quad \Gamma \vdash p : Id_A(x,y) \quad \Gamma \vdash q:Id_A(x,y)}{
\Gamma\vdash uip : Id_{Id_A(x,y)}(p,q)}$

Discussion in Coq is in

- Pierre Corbineau,
*The K axiom in Coq (almost) for free*(pdf)

Last revised on August 9, 2018 at 17:39:26. See the history of this page for a list of all contributions to it.