axiom K (type theory)

**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**

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

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

See also at *extensional type theory – Propositional extensionality*.

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

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.)

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