[[!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 #### Strict dependent product types Finally, we present the typal congruence rule for the formation rule of function types, which relies upon the previous two results. \begin{theorem} Given types $A$ and $A'$ and type families $x:A \vdash B(x)$, $x:A' \vdash B'(x)$ and equivalence $e_A:A \simeq A'$ and dependent function $e_B:\prod_{x:A} B(x) \simeq B'(e_A(x))$, there is an equivalence $$\mathrm{congform}(e_A, e_B):\left(\prod_{x:A} B(x)\right) \simeq \left(\prod_{x:A'} B'(x)\right)$$ \end{theorem} \begin{proof} We define the function $$\mathrm{congform}(e_A, e_B):\left(\prod_{x:A} B(x)\right) \to \left(\prod_{x:A'} B'(x)\right)$$ by $$\mathrm{congform}(e_A, e_B) \coloneqq \lambda (f:\prod_{x:A} B(x)).\lambda x:A'.\mathrm{transport}_{x:A'.B'(x)}(e_A(e_A^{-1}(x)), x, \mathrm{sec}_{e_A}(x), e_B(e_A^{-1}(x))(f(e_A^{-1}(x))))$$ and the inverse function by $$\mathrm{congform}(e_A, e_B)^{-1} \coloneqq \lambda (f:\prod_{x:A'} B'(x)).\lambda x:A.e_B(x)^{-1}(f(e_A(x)))$$ where the equivalence $e_A:A \simeq A'$ has families of identifications $$x':A \vdash \mathrm{sec}_{e_A}(x):e_A(e_A^{-1}(x)) =_{A'} x$$ $$x:A \vdash \mathrm{ret}_{e_A}:e_A^{-1}(e_A(x)) =_A x$$ witnessing that $e_A^{-1}$ is a [[section]] and [[retraction]] of $e_A$ respectively. Now it suffices to construct homotopies $$\prod_{f:\prod_{x:A} B(x)} \mathrm{congform}(e_A, e_B)^{-1}(\mathrm{congform}(e_A, e_B)(f)) =_{\prod_{x:A} B(x)} f$$ $$\prod_{g:\prod_{x:A'} B'(x)} \mathrm{congform}(e_A, e_B)(\mathrm{congform}(e_A, e_B)^{-1}(g)) =_{\prod_{x:A'} B'(x)} g$$ from where it implies that $\mathrm{congform}(e_A, e_B)$ has a coherent inverse and contractible fibers and is thus an [[equivalence of types]]. ---- Similarly, by definition, $$\mathrm{congform}(e_A, e_B)(\mathrm{congform}(e_A, e_B)^{-1}(f)) \equiv \lambda x:A'.\mathrm{transport}_{x:A'.B'(x)}(e_A(e_A^{-1}(x)), x, \mathrm{sec}_{e_A}(x), e_B(e_A^{-1}(x))(( \lambda x:A.e_B(x)^{-1}(f(e_A(x))) )(e_A^{-1}(x))))$$ By the computation rules of strict function types, there is a family of judgmental equalities $$x:A \vdash (\lambda x:A.e_B(x)^{-1}(f(e_A(x))))(e_A^{-1}(x)) \equiv e_B(e_A^{-1}(x))^{-1}(f(e_A(e_A^{-1}(x))))$$ and thus by the structural rules of [[judgmental equalities]] and the judgmental congruence rules for function types, a judgmental equality $$\lambda x:A'.\mathrm{transport}_{x:A'.B'(x)}(e_A(e_A^{-1}(x)), x, \mathrm{sec}_{e_A}(x), e_B(e_A^{-1}(x))((\lambda x:A.e_B(x)^{-1}(f(e_A(x))) )(e_A^{-1}(x)))) \equiv \lambda x:A'.\mathrm{transport}_{x:A'.B'(x)}(e_A(e_A^{-1}(x)), x, \mathrm{sec}_{e_A}(x), e_B(e_A^{-1}(x))(e_B(e_A^{-1}(x))^{-1}(f(e_A(e_A^{-1}(x))))))$$ ---- The equivalence $e_B:B \simeq B'$ has a family of identifications $$x:B \vdash \mathrm{ret}_{e_B}(x):e_B^{-1}(e_B(x)) =_{B} x$$ witnessing that $e_B^{-1}$ is a [[retraction]] of $e_B$. This means that by applying the canonical inductively defined function $\mathrm{idtohomotopy}$ which takes identifications between functions to homotopies between functions, one gets the family of identifications $$\mathrm{idtohomotopy}(\lambda x:A.e_B^{-1}(e_B(x)), \lambda x:A.x, f(e_A^{-1}(e_A(x))):e_B^{-1}(e_B(f(e_A^{-1}(e_A(x))))) =_{B} f(e_A^{-1}(e_A(x)))$$ Similarly, the equivalence $e_A:A \simeq A'$ has a family of identifications $$x:B \vdash \mathrm{ret}_{e_A}(x):e_A^{-1}(e_A(x)) =_{A} x$$ witnessing that $e_A^{-1}$ is a [[retraction]] of $e_A$. This means by applying $f$ to the above family of identifications, one gets the family of identifications $$x:A \vdash \mathrm{ap}(f, e_A^{-1}(e_A(x)), x, \mathrm{ret}_{e_A}(x)):f(e_A^{-1}(e_A(x))) =_{B} f(x)$$ By concatenation of identifications, one gets the family of identifications $$x:A \vdash \mathrm{idtohomotopy}(\lambda x:A.e_B^{-1}(e_B(x)), \lambda x:A.x, f(e_A^{-1}(e_A(x))) \bullet \mathrm{ap}(f, e_A^{-1}(e_A(x)), x, \mathrm{ret}_{e_A}(x)):e_B^{-1}(e_B(f(e_A^{-1}(e_A(x))))) =_{B} f(x)$$ By lambda abstraction, one gets the homotopy $$\lambda x:A.\mathrm{idtohomotopy}(\lambda x:A.e_B^{-1}(e_B(x)), \lambda x:A.x, f(e_A^{-1}(e_A(x))) \bullet \mathrm{ap}(f, e_A^{-1}(e_A(x)), x, \mathrm{ret}_{e_A}(x)):\prod_{x:A} e_B^{-1}(e_B(f(e_A^{-1}(e_A(x))))) =_{B} f(x)$$ and by function extensionality, this is the same as $$\mathrm{funext}^{-1}(\lambda x:A.\mathrm{idtohomotopy}(\lambda x:A.e_B^{-1}(e_B(x)), \lambda x:A.x, f(e_A^{-1}(e_A(x))) \bullet \mathrm{ap}(f, e_A^{-1}(e_A(x)), x, \mathrm{ret}_{e_A}(x))):\lambda (x:A).e_B^{-1}(e_B(f(e_A^{-1}(e_A(x))))) =_{A \to B} \lambda x:A.f(x)$$ By the computation rules of strict function types and the structural rules of judgmental equality, the type $$\lambda (x:A).e_B^{-1}(e_B(f(e_A^{-1}(e_A(x))))) =_{A \to B} \lambda x:A.f(x)$$ is judgmentally equal to $\mathrm{congform}(e_A, e_B)^{-1}(\mathrm{congform}(e_A, e_B)(f)) =_{A \to B} f$, so we have $$\mathrm{funext}^{-1}(\lambda x:A.\mathrm{idtohomotopy}(\lambda x:A.e_B^{-1}(e_B(x)), \lambda x:A.x, f(e_A^{-1}(e_A(x))) \bullet \mathrm{ap}(f, e_A^{-1}(e_A(x)), x, \mathrm{ret}_{e_A}(x))):\mathrm{congform}(e_A, e_B)^{-1}(\mathrm{congform}(e_A, e_B)(f)) =_{A \to B} f$$ $\lambda$-abstraction on functions $f:A \to B$ leads to the dependent function $$\lambda (f:A \to B).\mathrm{funext}^{-1}(\lambda x:A.\mathrm{idtohomotopy}(\lambda x:A.e_B^{-1}(e_B(x)), \lambda x:A.x, f(e_A^{-1}(e_A(x))) \bullet \mathrm{ap}(f, e_A^{-1}(e_A(x)), x, \mathrm{ret}_{e_A}(x))):\prod_{f:A \to B} \mathrm{congform}(e_A, e_B)^{-1}(\mathrm{congform}(e_A, e_B)(f)) =_{A \to B} f$$ \end{proof} category: redirected to nlab