[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] $$x =_A y \coloneqq \mathrm{Id}_A(\mathrm{rec}_\mathbb{2}^A(x, y))$$ ### With inference rules {#ExplicitDefinition} The [[inference rules]] for forming identity types and terms are as follows. First the rule that defines the identity type itself, as a [[dependent type]], in some [[context]] $\Gamma$. **[[type formation]]** $$\frac{\Gamma \vdash A:Type} {\Gamma, f:\mathbb{2} \to A \vdash Id_A(f):Type}$$ Now the basic "introduction" rule, which says that everything is equal to itself in a canonical way. **[[term introduction]]** $$\frac{\Gamma \vdash A:Type} {\Gamma, x:A \vdash r(x) : Id_A(\lambda b:\mathbb{2}.x)}$$ To a category theorist, it might be more natural to call this $1_X$. The traditional notation $r(x)$ indicates that this is a canonical proof of the *[[reflexive relation|reflexivity]]* of equality. Then there are the "elimination" rule and the "computation" or [[beta-reduction]] rule of identity types, which together result in the induction principle of identity types. The following rules may seem a little ad-hoc, but they are actually a particular case of the general notion of [[inductive type]]. Then we have the “elimination” rule, which is easily the most subtle and powerful. $$\frac{\Gamma, f:\mathbb{2} \to A, p:Id_A(f), \Delta(f,p) \vdash C(f,p):Type \quad \Gamma, x:A, \Delta(\lambda b:\mathbb{2}.x,r(x)) \vdash t(x):C(\lambda b:\mathbb{2}.x,r(x))} {\Gamma, f:\mathbb{2} \to A, p:Id_A(f) \vdash J^{\underline{ }.t}(f,p) : C(f,p)}$$ Ignore the presence of the additional context $\Delta$ for now; it is unnecessary if we also have [[dependent product types]]. The elimination rule then says that if: 1. for any $f:\mathbb{2} \to A$ and any reason $p:Id_A(f)$ why they are the same, we have a type $C(f,p)$ 1. for any $x:A$ we have a $t(x):C(\lambda b:\mathbb{2}.x,r(x))$, we can construct a canonically defined term $J^{\underline{ }.t}(f,p):C(f,p)$ for *any* $f$ and $p:Id_A(f)$, by "[[transport|transporting]]" the family of terms $t(x)$ dependent upon $x:A$ along the proof of equality $p$. In homotopical or categorical models, this can be viewed as a "path-lifting" property, i.e. that the [[display map]]s are some sort of [[fibration]], which can be made precise with the [[identity type weak factorization system]]. A particular case is when $C$ is a term representing a proposition according to the propositions-as-types philosophy. In this case, the elimination rule says that in order to prove a statement is true about all $f,p$, it suffices to prove it in the special case for $\lambda b:\mathbb{2}.x,r(x)$. Finally, we have the "computation" or [[beta-reduction]] rule. There are two possible computation rules, which result in strict and weak identity types respectively. The computation rule for strict identity types says that if we substitute along a [[reflexive relation|reflexivity]] proof, nothing happens. **[[computation rule]] for strict identity types** $$\frac{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash C(x,y,p):Type \qquad \Gamma, x:A, \Delta(x,x,r(x)) \vdash t(x):C(x,x,r(x))} {\Gamma, x:A, \Delta(x,x,r(x)) \vdash J^{\underline{ }.t}(x,x,r(x)) = t(x)}$$ Note that the equality $=$ in the conclusion of this computation rule is [[judgmental equality]], not an instance of the identity/equality type itself. The computation rule for weak identity types says that there is a witness that the substitution along a [[reflexive relation|reflexivity]] proof is equal to the original $t(x)$. **[[computation rule]] for weak identity types** $$\frac{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash C(x,y,p):Type \qquad \Gamma, x:A, \Delta(x,x,r(x)) \vdash t(x):C(x,x,r(x))} {\Gamma, x:A, \Delta(x,x,r(x)) \vdash \beta^{\underline{ }.t}(x):Id_{C(x,x,r(x))}(J^{\underline{ }.t}(x,x,r(x)),t(x))}$$ If we have [[dependent product types]], we can directly use the [[dependent function]] $\Gamma \vdash t:\prod_{x:A} C(x,x,r(x))$ instead of the family of terms $t(x)$ dependent upon $x:A$ in the hypothesis. Then the canonically defined term is given by $J(t,x,y,p):C(x,y,p)$ and is dependent upon dependent function $t:\prod_{x:A} C(x,x,r(x))$ rather than annotated with the family $t(x)$. $$\frac{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash C(x,y,p):Type \quad \Gamma \vdash t:\prod_{x:A} C(x,x,r(x))} {\Gamma, x:A, y:A, p:Id_A(x,y) \vdash J(t,x,y,p) : C(x,y,p)}$$ $$\frac{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash C(x,y,p):Type \qquad \Gamma \vdash t:\prod_{x:A} C(x,x,r(x))} {\Gamma, x:A, \Delta(x,x,r(x)) \vdash J(t,x,x,r(x)) = t(x)}$$ The original inference rules using the family of terms $t(x)$ dependent upon $x:A$ is then given by $J(\lambda x:A.t(x),x,y,p):C(x,y,p)$ and $J(\lambda x:A.t(x),x,x,r(x)) \equiv t(x):C(x,x,r(x))$. . Similarly, the canonically defined term in the propositional computation rule is given by the identification $\beta(t,x):Id_{C(x,x,r(x))}(J(t,x,x,r(x)),t(x))$ and is dependent upon dependent function $t:\prod_{x:A} C(x,x,r(x))$ rather than annotated with the family $t(x)$. $$\frac{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash C(x,y,p):Type \qquad \Gamma \vdash t:\prod_{x:A} C(x,x,r(x))} {\Gamma, x:A, \Delta(x,x,r(x)) \vdash \beta(t,x):Id_{C(x,x,r(x))}(J(t,x,x,r(x)),t(x))}$$ The original inference rules using the family of terms $t(x)$ dependent upon $x:A$ is then given by $\beta(\lambda x:A.t(x),x):\mathrm{Id}_{C(x,x,r(x))}(J(\lambda x:A.t(x),x,x,r(x)),t(x))$. . category: redirected to nlab