[[!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 We have a dependent type theory with 1. Judgmental equality 2. A separate type judgment 3. Function types 4. A Russell universe 6. Small dependent product types 7. Small identity types for each type in the type theory 8. Small dependent sum types 5. 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. 9. Univalence axiom, which could be expressed internally in the universe. #### Function types Formation rules for function types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \to B \; \mathrm{type}}$$ 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} \quad \Gamma \vdash f:A \to B}{\Gamma, x:A \vdash f(x):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 (\lambda(x:A).b(x))(a) \equiv b(a):B}$$ Uniqueness rules for function types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, f:A \to B \vdash f \equiv \lambda(x:A).f(x):A \to B}$$ #### Bijection types Formation rules for bijection types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \cong B \; \mathrm{type}}$$ Introduction rules for bijection types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B \quad \Gamma \vdash g:B \to A \quad \Gamma, x:A \vdash g(f(x)) \equiv x:A \quad \Gamma, y:B \vdash f(g(y)) \equiv y:B}{\Gamma \vdash \mathrm{toBij}(f, g):A \cong B}$$ Elimination rules for bijection types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \cong B}{\Gamma \vdash f:A \to B}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \cong B}{\Gamma \vdash f^{-1}:B \to A}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \cong B}{\Gamma, x:A \vdash f^{-1}(f(x)) \equiv x:A}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \cong B}{\Gamma, y:B \vdash f(f^{-1}(y)) \equiv y:B}$$ Computation rules for bijection types $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B \quad \Gamma \vdash g:B \to A \quad \Gamma, x:A \vdash g(f(x)) \equiv x:A \quad \Gamma, y:B \vdash f(g(y)) \equiv y:B}{\Gamma \vdash \mathrm{toBij}(f, g) \equiv f:A \to B}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash f:A \to B \quad \Gamma \vdash g:B \to A \quad \Gamma, x:A \vdash g(f(x)) \equiv x:A \quad \Gamma, y:B \vdash f(g(y)) \equiv y:B}{\Gamma \vdash \mathrm{toBij}(f, g)^{-1} \equiv g:A \to B}$$ Uniqueness rules for bijection types: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, f:A \cong B \vdash f \equiv \mathrm{toBij}(f, f^{-1}):A \cong B}$$ #### Russell universe $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash U \; \mathrm{type}} \qquad \frac{\Gamma \vdash A:U}{\Gamma \vdash A \; \mathrm{type}}$$ #### Identity types of universe $$\frac{\Gamma \vdash A:U \quad \Gamma \vdash B:U}{\Gamma \vdash A =_U B:U}$$ $$\frac{\Gamma \vdash A:U}{\Gamma \vdash \mathrm{refl}_U(A):A =_U A}$$ $$\frac{\Gamma \vdash C:\Pi(U, \Pi(U, \Pi(\lambda A:U.\lambda B:U.A =_U B, 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, \Pi(U, \Pi(\lambda A:U.\lambda B:U.A =_U B,\lambda p:A =_U B.C(A, B, p))))}$$ $$\frac{\Gamma \vdash C:\Pi(U, \Pi(U, \Pi(\lambda A:U.\lambda B:U.A =_U B, U))) \quad \Gamma \vdash D:\Pi(U, \lambda A:U.C(A)(A)(\mathrm{refl}_U(A)))}{\Gamma, A:U \vdash \mathrm{ind}_{=_U}(C, D, A, A, \mathrm{refl}_U(A)) \equiv D(A):C(A, A, \mathrm{refl}_U(A))}$$ #### 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)}$$ ... #### Identity types $$\frac{\Gamma \vdash A:U \quad \Gamma \vdash x:A \quad \Gamma \vdash y:A}{\Gamma \vdash x =_A y:U}$$ #### Dependent product types $$\frac{\Gamma \vdash A:U \quad \Gamma \vdash B:A \to U}{\Gamma \vdash \Pi(A, B):U}$$ $$\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, revisited $$\frac{\Gamma \vdash A:U \quad \Gamma \vdash x:A \quad \Gamma \vdash y:A}{\Gamma \vdash x =_A y:U}$$ $$\frac{\Gamma \vdash A:U \quad \Gamma \vdash x:A}{\Gamma \vdash \mathrm{refl}(A, x):x =_A x}$$ #### Dependent sum types ... category: redirected to nlab