[[!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 function types \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{ret}_{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 (g:A' \to B').\lambda x:A.e_B^{-1}(g(e_A(x)))$$ \end{proof} category: redirected to nlab