nLab axiom K (type theory)

Disambiguation: For axiom K as a principle of modal logic, see axiom K (modal logic)

Contents

Idea

In type theory, the axiom K is an axiom that when added to intensional type theory turns it into extensional type theory — or more precisely, what is called here “propositionally extensional type theory”. In the language of homotopy type theory, this means that all types are h-sets, accordingly axiom K is incompatible with the univalence axiom.

Heuristically, the axiom asserts that each term of each identity type $Id_A(x,x)$ (of equivalences of a term $x \colon A$) is propositionally equal to the canonical reflexivity equality proof $refl_x \colon Id_A(x,x)$.

Statement

$K \colon \underset{A \colon Type}{\prod} \underset{x \colon A}{\prod} \underset{P \colon Id_A(x,x) \to Type}{\prod} \left( P(refl_A x) \to \underset{h \colon Id_A(x,x)}{\prod} P(h) \right)$

Properties

Unlike its logical equivalent axiom UIP, axiom K can be endowed with computational behavior: $K(A,x,P,d,refl_A x)$ computes to $d$. This gives a way to specify a computational propositionally extensional type theory.

This sort of computational axiom K can also be implemented with, and is sufficient to imply, a general scheme of function definition by pattern-matching. This is implemented in the proof assistant Agda. (The flag --without-K alters Agda’s pattern-matching scheme to a weaker version appropriate for intensional type theory, including homotopy type theory.)

References

The axiom K was introduced in

• Thomas Streicher, Investigations into intensional type theory Habilitation thesis (1993) (pdf)

For a review and discussion of the implementation in Coq, see

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

Discussion in the context of homotopy type theory is in

around theorem 7.2.1