[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] \begin{theorem} The function $\mathrm{apb}_{A, B}(a, b, c, d):(a =_A c) \times (b =_B d) \to (a, b) =_{A \times B} (c, d)$ is an equivalence of types. \end{theorem} \begin{proof} ... \end{proof} category: redirected to nlab