202508272308

Tags : Homotopy Type Theory

Axiom K

---

Axiom K is an elimination rule for equality types that was added by Thomas Streicher in 1993 which when added to intentional type theory converts it to set level type theory, the axiom infomally states:

Axiom

Given any type $A$ and any element $x:A$, the type $x=x$ is inhabited by exactly 1 element, which is ${\text{refl}}_x$.

Formally, the axiom writes as:

$$K:\prod _{(A:\mathcal{U})}\prod _{(x:A)}\prod _{(P:x=x\to \mathcal{U})}P({\text{refl}}_x)\to \prod _{h:x=x}P(h)$$

This reads as, given any type $A$ and any $x:A$ and any type family over $x=x$, to define a function out of the type family, it suffices to define it for ${\text{refl}}_x$. Since ${\text{refl}}_x$ cannot generate any elements other than itself, this states that all witness of equality of $x$ are propositionally equal.

---

References

• Streicher 1993
• Identity Type