[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] ## In type theory In type theory, there are broadly three different notions of equality: which could be distinguished: **judgmental equality**, **propositional equality**, and **typal equality**. Judgmental equality is defined as a basic judgment in type theory. Propositional equality is defined as a proposition in any two-layered type theory with a layer of types and a layer of propositions. Typal equality is the [[identity type]] or [[path type]] in type theory. These three different notions of equality could then be used in definitions, where the equality is called **definitional equality**, as well as in the computation and uniqueness rules of type formers, where the equality is called **computational equality**, **conversional equality**, or **reductional equality**. ### Judgmental equality ## Comparison of judgmental and propositional equality * Judgmental equality of terms: $$a \equiv b:A$$ * Propositional equality of terms: $$p:a =_A b$$ * Judgmental equality of types: $$A \equiv B \; \mathrm{type}$$ * [[equivalence of types]] (i.e. propositional equality of types): $$P:A \simeq B$$ * Substitution of judgmental equal terms: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a \equiv b : A \quad \Gamma, x:A, \Delta \vdash B \; \mathrm{type}}{\Gamma, \Delta[a/x] \vdash B[a/x] \equiv B[b/x] \; \mathrm{type}}$$ * Substitution of propositional equal terms: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \quad \Gamma, x:A, \Delta \vdash B \; \mathrm{type}}{\Gamma, \Delta[a/x] \vdash \mathrm{tr}(x.B, a, b, p):B[a/x] \simeq B[b/x] \; \mathrm{type}}$$ category: redirected to nlab