By constructing a model of type theory where types are interpreted as groupoids (categories where all arrows are isomorphisms) Hofmann and Streicher (1998) showed that it cannot be proved in intuitionistic type theory that all proofs of \(I(A,a,b)\) are identical. This may seem as an incompleteness of the theory and Streicher suggested a new axiom \(\K\) from which it follows that all proofs of \(\I(A,a,b)\) are identical to \(\r\).