[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] * Judgmental introduction definition rule $$\frac{\Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \; \mathrm{type}} \qquad \frac{\Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A = B \; \mathrm{type}}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash b:A}{\Gamma \vdash a:A} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash b:A}{\Gamma \vdash a = b:A}$$ * Propositional introduction and definition rules: $$\frac{\Gamma \vert \Phi \vdash B \; \mathrm{type}}{\Gamma \vert \Phi \vdash A \; \mathrm{type}} \qquad \frac{\Gamma \vert \Phi \vdash B \; \mathrm{type}}{\Gamma \vert \Phi \vdash A = B\; \mathrm{true}}$$ $$\frac{\Gamma \vert \Phi \vdash A \; \mathrm{type} \quad \Gamma \vert \Phi \vdash b:A}{\Gamma \vert \Phi \vdash a:A} \qquad \frac{\Gamma \vert \Phi \vdash A \; \mathrm{type} \quad \Gamma \vert \Phi \vdash b:A}{\Gamma \vert \Phi \vdash a =_A b\; \mathrm{true}}$$ * Typal introduction and definition rules: $$\frac{\Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \; \mathrm{type}} \qquad \frac{\Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash P:A \simeq B}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma\vdash a:A }{\Gamma \vdash b:A} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash b:A}{\Gamma \vdash p:a =_A b}$$ category: redirected to nlab