J Eliminator

Definition

The J eliminator (or J rule) is the Elimination Rule for identity types in Type Theory. It expresses the principle of path induction or identity elimination.

Given a type $A$ and a type family $C:{\prod }_{x,y:A}(x=y)\to \mathcal{U}$, the J eliminator states that to construct an element of $C(x,y,p)$ for any $x,y:A$ and $p:x=y$, it suffices to handle the reflexivity case.

$J:{\prod }_{C:{\prod }_{x,y:A}(x=y)\to \mathcal{U}}\left({\prod }_{x:A}C(x,x,{\text{refl}}_x)\right)\to {\prod }_{x,y:A}{\prod }_{p:x=y}C(x,y,p)$

Computation Rule

The J eliminator satisfies the following Computation Rule:

$J(C,c,x,x,{\text{refl}}_x)\equiv c(x)$

Intuition

The J eliminator embodies the principle that the only way to construct a path is via reflexivity. To prove a property holds for all paths, it suffices to prove it for reflexivity paths.

Alternative Forms

The J eliminator can be presented in several equivalent forms:

• Based path induction: Fixing one endpoint
• Paulin-Mohring J: A simplified version used in some proof assistants
• Transport: Moving along paths in type families

Related Concepts

• Identity Type: The type for which J is the eliminator
• Path Induction: Another name for the J eliminator principle
• Elimination Rule: J as an instance of elimination
• Refl: The reflexivity constructor for identity types
• Transport: A consequence of the J eliminator
• Homotopy Type Theory: Where J has homotopy-theoretic interpretation