[[!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(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]]. \end{proof} category: redirected to nlab