[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Formation rules for the natural numbers type: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{N} \; \mathrm{type}}$$ Introduction rules for the natural numbers type: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{N}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N} \vdash s(n):\mathbb{N}}$$ Rules for universes $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, i:\mathbb{N} \vdash U(i) \; \mathrm{type}}$$ $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{level}_A:\mathbb{N}} \quad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash A:U(\mathrm{level}_A)}$$ $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash A:U(i)}{\Gamma \vdash A \; \mathrm{type}}$$ Formation rules for function types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \to B \; \mathrm{type}}$$ Lifts for universes: $$\frac{\Gamma \vdash i:\mathbb{N}}{\Gamma \vdash \mathrm{Lift}(i):U(i) \to U(s(i))}$$ Formation rules for identification types: $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash A:U(i)}{\Gamma, x:A, y:A \vdash x =_A y \; \mathrm{type}}$$ Levels for universes: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, i:\mathbb{N} \vdash \mathrm{defLevelU}(i):\mathrm{level}_{U(i)} =_{\mathbb{N}} s(i)}$$ Introduction rules for function types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, x:A \vdash b(x):B}{\Gamma \vdash \lambda(x:A).b(x):A \to B}$$ Elimination rules for function types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, f:A \to B, a:A \vdash \mathrm{ind}_{A \to B}(f, a):B}$$ Computation rules for function types $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma, x:A \vdash b(x):B}{\Gamma, a:A \vdash \beta_{A \to_i B}^{x:A.b(x)}(a):\mathrm{ind}_{A \to B}(\lambda(x:A).b(x), a) =_{B} b(a)}$$ Uniqueness rules for function types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, f:A \to B \vdash \eta_{A \to B}(f):f =_{A \to B} \lambda(x:A).\mathrm{ind}_{A \to B}(f, x)}$$ Universe levels for function types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash \mathrm{defLevel}_{A \to B}:\mathrm{level}_{A \to B} =_{\mathbb{N}} \max(\mathrm{level}_A, \mathrm{level}_B)}$$ Formation rules for dependent function types: $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash A:U(i) \quad \Gamma \vdash B:A \to U(i)}{\Gamma \vdash \Pi(i, A, B) \; \mathrm{type}}$$ Introduction rules for dependent function types: $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash A:U(i) \quad \Gamma \vdash B:A \to U(i) \quad \Gamma, x:A \vdash b(x):\mathrm{ind}_{A \to U(i)}(B, x)}{\Gamma \vdash \lambda(x:A).b(x):\Pi(i, A, B)}$$ Elimination rules for dependent function types: $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash A:U(i) \quad \Gamma \vdash B:A \to U(i)}{\Gamma, f:\Pi(i, A, B), a:A \vdash \mathrm{ind}_{\Pi(i, A, B)}(f, a):B(a)}$$ Computation rules for dependent function types $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash A:U(i) \quad \Gamma \vdash B:A \to U(i) \quad \Gamma, x:A \vdash b(x):\mathrm{ind}_{A \to U(i)}(B, x)}{\Gamma, a:A \vdash \beta_{\Pi(i, A, B)}^{x:A.b(x)}(a):\mathrm{ind}_{\Pi(i, A, B)}(\lambda(x:A).b(x), a) =_{\mathrm{ind}_{A \to U(i)}(B, a)} b(a)}$$ Uniqueness rules for dependent function types: $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash A:U(i) \quad \Gamma \vdash B:A \to U(i)}{\Gamma, f:\Pi(i, A, B) \vdash \eta_{\Pi(i, A, B)}(f):f =_{\Pi(i, A, B)} \lambda(x:A).\mathrm{ind}_{\Pi(i, A, B)}(f, x)}$$ Universe levels for dependent function types: $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash A:U(i) \quad \Gamma \vdash B:A \to U(i)}{\Gamma \vdash \mathrm{defLevel}_{\Pi(i, A, B)}:\mathrm{level}_{\Pi(i, A, B)} =_{\mathbb{N}} i}$$ Elimination rule for the natural numbers type: $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash C:\mathbb{N} \to U(i) \quad \Gamma \vdash c_0:\mathrm{ind}_{\mathbb{N} \to U(i)}(C, 0) \quad \Gamma \vdash c_s:\Pi\left(i, \mathbb{N}, \mathrm{ind}_{\mathbb{N} \to U(i)}(C, x) \to \mathrm{ind}_{\mathbb{N} \to U(i)}(C, s(x))\right)}{\Gamma, n:\mathbb{N} \vdash \mathrm{ind}_\mathbb{N}(i, C, c_0, c_s, n):\mathrm{ind}_{\mathbb{N} \to U(i)}(C, n)}$$ Computation rule for the natural numbers type: $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash C:\mathbb{N} \to U(i) \quad \Gamma \vdash c_0:\mathrm{ind}_{\mathbb{N} \to U(i)}(C, 0) \quad \Gamma \vdash c_s:\Pi\left(i, \mathbb{N}, \mathrm{ind}_{\mathbb{N} \to U(i)}(C, x) \to \mathrm{ind}_{\mathbb{N} \to U(i)}(C, s(x))\right)}{\Gamma \vdash \beta_\mathbb{N}^0(i, C, c_0, c_s):\mathrm{ind}_\mathbb{N}(i, C, c_0, c_s, 0) =_{\mathrm{ind}_{\mathbb{N} \to U(i)}(C, 0)} c_0}$$ $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash C:\mathbb{N} \to U(i) \quad \Gamma \vdash c_0:\mathrm{ind}_{\mathbb{N} \to U(i)}(C, 0) \quad \Gamma \vdash c_s:\Pi\left(i, \mathbb{N}, \mathrm{ind}_{\mathbb{N} \to U(i)}(C, x) \to \mathrm{ind}_{\mathbb{N} \to U(i)}(C, s(x))\right)}{\Gamma, n:\mathbb{N} \vdash \beta_\mathbb{N}^s(i, C, c_0, c_s, n):\mathrm{ind}_\mathbb{N}(i, C, c_0, c_s, s(n)) =_{\mathrm{ind}_{\mathbb{N} \to U(i)}(C, s(n))} \mathrm{ind}_{\Pi\left(i, \mathbb{N}, \mathrm{ind}_{\mathbb{N} \to U(i)}(C, x) \to \mathrm{ind}_{\mathbb{N} \to U(i)}(C, s(x))\right)}(c_s, \mathrm{ind}_\mathbb{N}(i, C, c_0, c_s, s(n)))}$$ Universe level for the natural numbers type: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{defLevel}_\mathbb{N}:\mathrm{level}_{\mathbb{N}} =_{\mathbb{N}} 0}$$ Formation rules for dependent pair types: $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash A:U(i) \quad \Gamma \vdash B:A \to U(i)}{\Gamma \vdash \Sigma(i, A, B) \; \mathrm{type}}$$ Introduction rules for dependent pair types: $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash A:U(i) \quad \Gamma \vdash B:A \to U(i)}{\Gamma, x:A, y:B(x) \vdash \mathrm{in}(i, A, B, x, y):\Sigma(i, A, B)}$$ Elimination rules for dependent pair types: $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash A:U(i) \quad \Gamma \vdash B:A \to U(i)}{\Gamma, z:\Sigma(i, A, B) \vdash \mathrm{ind}_{\Sigma(i, A, B)}^A(z):A} \qquad \frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash A:U(i) \quad \Gamma \vdash B:A \to U(i)}{\Gamma, z:\Sigma(i, A, B) \vdash \mathrm{ind}_{\Sigma(i, A, B)}^B(z):\mathrm{ind}_{A \to U(i)}(B, \mathrm{ind}_{\Sigma(i, A, B)}^A(z))}$$ Computation rules for dependent pair types: $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash A:U(i) \quad \Gamma \vdash B:A \to U(i)}{\Gamma, x:A, y:\mathrm{ind}_{A \to U(i)}(B, x) \vdash \beta_{\Sigma(i, A, B)}^A(x, y):\mathrm{ind}_{\Sigma(i, A, B)}^A(\mathrm{in}(i, A, B, x, y)) =_A x}$$ $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash A:U(i) \quad \Gamma \vdash B:A \to U(i)}{\Gamma, x:A, y:\mathrm{ind}_{A \to U(i)}(B, x) \vdash \beta_{\Sigma(i, A, B)}^B(x, y):\mathrm{ind}_{\Sigma(i, A, B)}^B(\mathrm{in}(i, A, B, x, y)) =_{\mathrm{ind}_{A \to U(i)}(B, \mathrm{ind}_{\Sigma(i, A, B)}^A(\mathrm{in}(i, A, B, x, y)))} y}$$ Uniqueness rules for dependent pair types: $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash A:U(i) \quad \Gamma \vdash B:A \to U(i)}{\Gamma, z:\Sigma(i, A, B) \vdash \eta_{\Sigma(i, A, B)}(z):z =_{\Sigma(i, A, B)} \mathrm{in}(i, A, B, \mathrm{ind}_{\Sigma(i, A, B)}^A(z), \mathrm{ind}_{\Sigma(i, A, B)}^B(z))}$$ Introduction rules for identification types: $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash A:U(i)}{\Gamma, x:A \vdash \mathrm{refl}_A(x) : x =_A x}$$ Elimination rule for identification types: $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash A:U(i) \quad \Gamma \vdash C:\Pi\left(s(i), A, \lambda(x:A.\Pi(s(i), A, \lambda(y:A).(x =_A y) \to U(i))\right) \quad \Gamma \vdash c:\prod_{x:A} C(x, x, \mathrm{refl}_A(x))}{\Gamma, x:A, y:A, p:x =_A y \vdash \mathrm{ind}_{=}(i, A, C, c, x, y, p):C(x, y, p)}$$ Computation rules for identification types: $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash A:U(i) \quad \Gamma \vdash C:\Pi\left(s(i), A, \lambda(x:A.\Pi(s(i), A, \lambda(y:A).(x =_A y) \to U(i))\right) \quad \Gamma \vdash c:\prod_{x:A} C(x, x, \mathrm{refl}_A(x))}{\Gamma, x:A \vdash \beta_{=}(i, A, C, c, x):\mathrm{ind}_{=}(i, A, C, c, x, x, \mathrm{refl}_A(x)) =_{C(x, x, \mathrm{refl}_A(x))} c(x)}$$ Universe levels for identification types: $$\frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash A:U(i)}{\Gamma, x:A, y:A \vdash \mathrm{defLevel}_{x =_A y}:\mathrm{level}_{x =_A y} =_\mathbb{N} i}$$ category: redirected to nlab