Contents

# Contents

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

## References

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.