Theorem. Set-truncation preserves and reflects surjections [007V]
- August 18, 2023
- Jon Sterling
Theorem. Set-truncation preserves and reflects surjections [007V]
- August 18, 2023
- Jon Sterling
A function \(f:A\to B\) is surjective (i.e. an effective epimorphism) if and only if its set-truncation \(\left \lVert f\right \rVert _{0}:\left \lVert A\right \rVert _{0}\to \left \lVert B\right \rVert _{0}\) is surjective.
Proof.
- August 18, 2023
- Jon Sterling
Proof.
- August 18, 2023
- Jon Sterling
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 |
Incidentally, the appeal to Theorem 7.3.12 of the HoTT Book can be replaced by the more general Proposition 2.26 of Christensen et al., which applies to an arbitrary reflective subuniverse and the corresponding subuniverse of separated types.