[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Formation rules for cone types: $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{cone}_{A}}$$ Introduction rules for cone types: $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash *:\mathrm{cone}_{A}}$$ $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash i:A \to \mathrm{cone}_{A}}$$ $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathcal{g}:\prod_{x:A} * =_{\mathrm{cone}_{A}} i(x)}$$ Elimination rules for cone types: $$\frac{\begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, y:\mathrm{cone}_{A} \vdash C(y) \; \mathrm{type} \\ \Gamma \vdash c_*:C(*) \quad \Gamma \vdash c_i:\prod_{x:A} C(i(x)) \\ \Gamma \vdash c_\mathcal{g}:\prod_{x:A} c_* =_{y:\mathrm{cone}_{A}.C(y)}^{\mathcal{g}(x)} c_i(x) \end{array}}{\Gamma \vdash \mathrm{ind}_{\mathrm{cone}_{A}}(c_*, c_i, c_\mathcal{g}):\prod_{y:\mathrm{cone}_{A}} C(y)}$$ Computation rules for cone types: $$\frac{\begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, y:\mathrm{cone}_{A} \vdash C(y) \; \mathrm{type} \\ \Gamma \vdash c_*:C(*) \quad \Gamma \vdash c_i:\prod_{x:A} C(i(x)) \\ \Gamma \vdash c_\mathcal{g}:\prod_{x:A} c_* =_{y:\mathrm{cone}_{A}.C(y)}^{\mathcal{g}(x)} c_i(x) \end{array}}{\Gamma \vdash \beta_{\mathrm{cone}_{A}}^{*}(c_*, c_i, c_\mathcal{g}):\mathrm{ind}_{\mathrm{cone}_{A}}(c_*, c_i, c_\mathcal{g})(*) =_{C(*)} c_*}$$ $$\frac{\begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, y:\mathrm{cone}_{A} \vdash C(y) \; \mathrm{type} \\ \Gamma \vdash c_*:C(*) \quad \Gamma \vdash c_i:\prod_{x:A} C(i(x)) \\ \Gamma \vdash c_\mathcal{g}:\prod_{x:A} c_* =_{y:\mathrm{cone}_{A}.C(y)}^{\mathcal{g}(x)} c_i(x) \end{array}}{\Gamma \vdash \beta_{\mathrm{cone}_{A}}^{i}(c_*, c_i, c_\mathcal{g}):\prod_{x:A} \mathrm{ind}_{\mathrm{cone}_{A}}(c_*, c_i, c_\mathcal{g})(i(x)) =_{C(i(x))} c_i(x)}$$ $$\frac{\begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, y:\mathrm{cone}_{A} \vdash C(y) \; \mathrm{type} \\ \Gamma \vdash c_*:C(*) \quad \Gamma \vdash c_i:\prod_{x:A} C(i(x)) \\ \Gamma \vdash c_\mathcal{g}:\prod_{x:A} c_* =_{y:\mathrm{cone}_{A}.C(y)}^{\mathcal{g}(x)} c_i(x) \end{array}}{\Gamma \vdash \beta_{\mathrm{cone}_{A}}^{\mathcal{g}}(c_*, c_i, c_\mathcal{g}):\prod_{x:A} \mathrm{apd}_{y:\mathrm{cone}_{A}.C(y)}(\mathrm{ind}_{\mathrm{cone}_{A}}(c_*, c_i, c_\mathcal{g}), *, i(x), \mathcal{g}(x)) =_{y:\mathrm{cone}_{A}.C(y)}^{\mathcal{g}(x)} c_\mathcal{g}(x)}$$ Uniqueness rules for cone types: $$\frac{\begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, y:\mathrm{cone}_{A} \vdash C(y) \; \mathrm{type} \\ \Gamma \vdash c:\prod_{y:\mathrm{cone}_{A}} C(y) \quad \Gamma \vdash p:\mathrm{cone}_{A} \end{array}}{\Gamma \vdash \eta_{\mathrm{cone}_{A}}(c, p):\mathrm{ind}_{\mathrm{cone}_{A}}(c_*, c_i, c_\mathcal{g})(p) =_{C(y)} c(p)}$$ category: redirected to nlab