[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Formation rules for cofiber types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B}{\Gamma \vdash \mathrm{cofib}_{A, B}(f)}$$ Introduction rules for cofiber types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B}{\Gamma \vdash i:B \to \mathrm{cofib}_{A, B}(f)}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B}{\Gamma \vdash *_{\mathrm{im}(f)}:\mathrm{cofib}_{A, B}(f)}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B}{\Gamma, x:A \vdash \mathcal{g}:\mathrm{Id}_{\mathrm{cofib}_{A, B}(f)}(i(f(x)), *_{\mathrm{im}(f)})}$$ category: redirected to nlab