Equality Reflection

In type theory, the equality reflection rule states that if we can derive a term $\Gamma\vdash p:x=_{A}y$ of the Identity Type of $A$, then the two terms $x$ and $y$ are Definitionally Equal. Explicitly, we have the rule

This has some immediate consequences:

• A complete typechecking algorithm immediately becomes Undecidable, as Conversion Checking will require us to synthesize proofs of the Identity Type.

• The type theory validates Axiom K.

  To see why, suppose that we have $p:x=_{A}y$. Note that equality reflection means that the iterated identity type $p=_{x=y}\mathsf{refl}$ is well-typed. This means that we can this as the motive to J Rule; which gives the following term:

  $\par K\;p=J(\lambda y\;p.\;p=_{x=y}\mathsf{refl})\;\mathsf{refl}\;p:p=_{x=y} \mathsf{refl}\par$

• This gives us an Eta Rule for the Identity Type, and is in fact equivalent to the existence of such an eta rule.

Examples

• NuPRL and its descendents support equality reflection.