[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Formation rules for bracket types $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash [A] \; \mathrm{type}}$$ Introduction rules for bracket types $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A \vdash \mathrm{isInhabited}(a):[A]} \quad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:[A], b:[A] \vdash \mathrm{proptrunc}(a, b):a =_{[A]} b}$$ $\sqrt{x, 1}$ category: redirected to nlab