nLab
axiom UIP

Idea

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.

Statement

Definition

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)}$$

Related concepts

• axiom K

References

Discussion in Coq is in

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