Timeline for In the category of sets epimorphisms are surjective - Constructive Proof?
Current License: CC BY-SA 3.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 18, 2014 at 19:47 | comment | added | Michal R. Przybylek | @ZhenLin, aws: yes, you're, of course, right --- it seems that I'm getting old and seeing things which are not :-) So, to conclude the series of comments: "surjection iff epi" holds in every pretopos. | |
| Aug 18, 2014 at 19:25 | comment | added | Zhen Lin | @MichalR.Przybylek Pretoposes are balanced. Do you mean quasitoposes? | |
| Aug 18, 2014 at 18:02 | comment | added | aws | By bounded separation, for every $b \in B$, the set $\{x \in \{0\}\;|\; \exists a \in A \;|\; h(a) = b\}$ exists. Hence by strong collection the set $\{ \{x \in \{0\} \;|\; \exists a \in A \; h(a) = b\} \;|\; b \in B \}$ exists. So by union, the second half of the definition of $C$ is a set. I think the problematic step for general $\Pi \Sigma$-pretoposes is strong collection. I'm not even sure how to state strong collection categorically (but it is included in CZF). | |
| Aug 18, 2014 at 17:48 | comment | added | Michal R. Przybylek | (...) but I don't see any reason why every $\Pi \Sigma$-pretopos, or any other notion of a predicative universe should be balanced (of course, CZF is balanced, so technically your claim is correct, but I'd like to see the exact reason behind this fact). | |
| Aug 18, 2014 at 17:47 | comment | added | Michal R. Przybylek | Sorry, then I still don't understand your construction --- could you write it down in a bit more formal way? I don't claim that you're wrong, I just want to understand what exactly you are doing. I think your proof cannot be carried to a general predicative universe --- I claim that in any regular category the statement "epi iff surjection" is equivalent to "bimorphism iff iso" (i.e. to the statement that the category is balanced). Clearly, every topos is balanced (because $\Omega$ classifies morphism), (cont...) | |
| Aug 18, 2014 at 14:48 | comment | added | aws | I claim that the first definition of C requires only bounded separation, strong collection and union (and pairing), so it's provably a set in CZF, for instance. I maybe should have been clearer that the first definition of C gives a different, in general strictly smaller set than the second. | |
| Aug 18, 2014 at 13:55 | comment | added | Michal R. Przybylek | Then, $f, g : B \rightarrow \Omega$ become predicates on $B$, where $f$ expresses the statement that $h$ is internally surjective, and $g := \top_B$. Therefore, $f = g$ says that "$h$ is internally injective" is true. | |
| Aug 18, 2014 at 13:49 | comment | added | Michal R. Przybylek | Actually, you need the power-set axiom to write your first definition. The second one, just says that $C := \mathcal{P}(\{0\}) = \Omega$, where $\Omega$ is the set of internal truth-values. | |
| Aug 18, 2014 at 13:09 | history | answered | aws | CC BY-SA 3.0 |