We deduce that \(\mathsf {isSurjective}\,\left \lvert f\right \rvert _{0}\) is equivalent to \(\mathsf {isSurjective}\,f\) as follows:
| \(\mathsf {isSurjective}\,\left \lvert f\right \rvert _{0}\) |
|
| \(
\equiv \mathchoice {\textstyle \prod _{{\mathopen {}\left (b:\left \lVert B\right \rVert _{0}\right )\mathclose {}}}}{\textstyle \prod _{{\mathopen {}\left (b:\left \lVert B\right \rVert _{0}\right )\mathclose {}}}}{\scriptstyle \prod _{{\mathopen {}\left (b:\left \lVert B\right \rVert _{0}\right )\mathclose {}}}}{\scriptscriptstyle \prod _{{\mathopen {}\left (b:\left \lVert B\right \rVert _{0}\right )\mathclose {}}}}\left \lVert \mathchoice {\textstyle \sum _{{\mathopen {}\left (a:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}{\textstyle \sum _{{\mathopen {}\left (a:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}{\scriptstyle \sum _{{\mathopen {}\left (a:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}{\scriptscriptstyle \sum _{{\mathopen {}\left (a:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}\left \lVert f\right \rVert _{0}a=b\right \rVert _{-1}
\) |
by definition |
| \(
\simeq
\mathchoice {\textstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\textstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\scriptstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\scriptscriptstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}
\left \lVert \mathchoice {\textstyle \sum _{{\mathopen {}\left (a:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}{\textstyle \sum _{{\mathopen {}\left (a:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}{\scriptstyle \sum _{{\mathopen {}\left (a:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}{\scriptscriptstyle \sum _{{\mathopen {}\left (a:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}\left \lVert f\right \rVert _{0}a=\left \lvert b\right \rvert _{0}\right \rVert _{-1}
\) |
by induction |
| \(
\simeq
\mathchoice {\textstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\textstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\scriptstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\scriptscriptstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}
\left \lVert \mathchoice {\textstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}{\textstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}{\scriptstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}{\scriptscriptstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}\left \lvert fa\right \rvert _{0}=\left \lvert b\right \rvert _{0}\right \rVert _{-1}
\) |
by Lemma |
| \(
\simeq
\mathchoice {\textstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\textstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\scriptstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\scriptscriptstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}
\left \lVert \mathchoice {\textstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}{\textstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}{\scriptstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}{\scriptscriptstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}\left \lVert fa=b\right \rVert _{-1}\right \rVert _{-1}
\) |
by HoTT Book, Theorem 7.3.12
|
| \(
\simeq
\mathchoice {\textstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\textstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\scriptstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\scriptscriptstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}
\left \lVert \mathchoice {\textstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}{\textstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}{\scriptstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}{\scriptscriptstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}fa=b\right \rVert _{-1}
\) |
by HoTT Book, Theorem 7.3.9 |
| \(
\equiv
\mathsf {isSurjective}\,f
\) |
by definition |