[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] ## 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