[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Type theory (dependent function types, dependent sum types, identity types, function extensionality) -> Predicate logic -> Set theory -> Number theory ## Dependent type theory The problem is that we need to define type families $$A:U \vdash A \to U \; \mathrm{type}$$ $$\prod_{A:U} A \to U$$ $$A:U, B:\prod_{A:U} A \to U \vdash \prod_{A:U} B(A) \to U$$ We have a dependent type theory with 1. A separate type judgment 2. Function types 3. A Russell universe 4. Small dependent product types 5. Small identity types for each type in the type theory 6. Small dependent sum types 7. Identity types for the Russell universe, which are small relative to the Russell universe. This makes sense because by univalence the identity types are essentially small. 8. Univalence axiom, which could be expressed internally in the universe. #### Russell universe $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash U \; \mathrm{type}} \qquad \frac{\Gamma \vdash A:U}{\Gamma \vdash A \; \mathrm{type}}$$ #### Formation rules Type of type families: $$\frac{\Gamma \vdash A:U}{\Gamma \vdash A \to U \; \mathrm{type}}$$ Type family of type families: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \Pi(U, \lambda A:U.A \to U) \; \mathrm{type}}$$ Identity type of universe: $$\frac{\Gamma \vdash A:U \quad \Gamma \vdash B:U}{\Gamma \vdash A =_U B:U}$$ Identity type of type families: $$\frac{\Gamma \vdash A:U \quad \Gamma \vdash B:A \to U \quad \Gamma \vdash C:A \to U}{\Gamma \vdash B =_{A \to U} C:U}$$ Dependent product types: $$\frac{\Gamma \vdash A:U \quad \Gamma \vdash B:A \to U}{\Gamma \vdash \Pi(A, B):U}$$ Identity types of types: $$\frac{\Gamma \vdash A:U \quad \Gamma \vdash x:A \quad \Gamma \vdash y:A}{\Gamma \vdash x =_A y:U}$$ #### Introduction rules Type of type families: $$\frac{\Gamma \vdash A:U \quad \Gamma, x:A \vdash B(x):U}{\Gamma \vdash \lambda(x:A).B(x):A \to U}$$ Type family of type families: $$\frac{\Gamma, A:U \vdash B(A):A \to U}{\Gamma \vdash \lambda A:U.B(x):\Pi(U, (-) \to U) \; \mathrm{type}}$$ Identity type of universes: $$\frac{\Gamma \vdash A:U}{\Gamma \vdash \mathrm{refl}_U(A):A =_U A}$$ Identity type of type families: $$\frac{\Gamma \vdash A:U \quad \Gamma \vdash B:A \to U}{\Gamma \vdash \mathrm{refl}_{A \to U}(B):B =_{A \to U} B}$$ Dependent product types: $$\frac{\Gamma \vdash A:U \quad \Gamma \vdash B:A \to U \quad \Gamma, x:A \vdash b(x):B(x)}{\Gamma \vdash \lambda x:A.b(x):\Pi(A)(B)}$$ Identity types of types: $$\frac{\Gamma \vdash A:U \quad \Gamma \vdash x:A}{\Gamma \vdash \mathrm{refl}(A, x):x =_A x}$$ #### Elimination rules Type of type families: $$\frac{\Gamma \vdash A:U \quad \Gamma \vdash B:A \to U}{\Gamma, x:A \vdash B(x):U}$$ Identity type of universes: $$\frac{\Gamma \vdash C:\Pi(U, \lambda A:U.\Pi(U, \lambda B:U.(A =_U B) \to U)) \quad \Gamma \vdash D:\Pi(U, \lambda A:U.C(A)(A)(\mathrm{refl}_U(A)))}{\Gamma \vdash \mathrm{ind}_{=_U}(C, D):\Pi(U, \lambda A:U.\Pi(U, \lambda B:U.\Pi(A =_U B,\lambda p:A =_U B.C(A, B, p))))}$$ #### Computation rules Type of type families: $$\frac{\Gamma \vdash A:U \quad \Gamma, x:A \vdash B(x):U}{\Gamma, x:A \vdash \beta(x:A).B(x):(\lambda(x:A).B(x))(x) =_{U} B(x)}$$ Identity type of universes: $$\frac{\Gamma \vdash C:\Pi(U, \lambda A:U.\Pi(U, \lambda B:U.(A =_U B) \to U)) \quad \Gamma \vdash D:\Pi(U, \lambda A:U.C(A)(A)(\mathrm{refl}_U(A)))}{\Gamma, A:U \vdash \beta_{=_U}(C, D, A):\mathrm{ind}_{=_U}(C, D, A, A, \mathrm{refl}_U(A)) =_{C(A, A, \mathrm{refl}_U(A))} D(A)}$$ #### Uniqueness rules Type of type families: $$\frac{\Gamma \vdash A:U}{\Gamma, B:A \to U \vdash B \equiv \lambda(x:A).B(x):A \to U}$$ #### Univalence axiom ... $$\frac{\Gamma \vdash A:U \quad \Gamma \vdash B:U}{\Gamma \vdash \mathrm{ua}(A, B):(A =_U B) \cong (A \cong B)}$$ category: redirected to nlab