Return to Answer

I find it a bit surprising, but I think you are correct. The proof I have is maybe a little too long for MO, so I'm only sketching it, but I'll be happy to provide more details if needed.

First one observe a form of "weak descent" for coequalizer diagram:

Lemma: Assume that the category $C$ satistifes all four condition of the op, then for any pair of coequalizer diagram $Y_0 \rightrightarrows Y_1 \to \text{coeq }Y_i$ and $X_0 \rightrightarrows X_1 \to \text{coeq }X_i$ and a cartesian natural transformation $X_0 \to Y_0$ , $X_1 \to Y_1$; the natural map $X_1 \to Y_1 \times_{\text{coeq } Y_i} (\text{coeq } X_i)$ is a regular epimorphism.

Proof: We use that a coequalizer $Y_0 \rightrightarrows Y_1$ can be written as a pushout $Y_1 \coprod_{Y_0 \coprod Y_1} Y_1$. Using that coproduct are disjoint and universal, one obtains that if $X_i \to Y_i$ is cartesian the map of spans from $X_1 \leftarrow X_0 \coprod X_1 \rightarrow X_1$ to $Y_1 \leftarrow Y_0 \coprod Y_1 \rightarrow Y_1$ is also cartesian and one can apply condition $(D2b)$ to this pushout.

With a bit more work, one can actually prove this also for $X_0 \to..$ and not just for coequalizer but for all colimits.

Now, we apply this to coequalizer of equivalence relation in a way inspired from the usual proof that descent for all colimits (in $\infty$-topos) implies that equivalence realtion are effective.

All the claim below are proved in the same way: they are clear for sets and we prove them for a general category with finite limits by interpreting everything in terms of "generalized" elements (or if you prefer by doing everything in terms of presheaves).

Consider now the case of an equivalence relation $R \rightrightarrows X$. Let $R^{(2)}$ be the subobject of $X^3$ corresponding to $\{ x_1,x_2,x_3 \in X^3 | x_1 R x_2 \text{ and } x_2 R x_3 \}$

$R^{(2)}$ has two maps to $R$ that sends $(x_1,x_2,x_3)$ to $(x_1,x_2)$ and $(x_1,x_3)$ and this makes $R^{(2)}$ into an equivalence relation on $R$. The coequalizer $R/R^{(2)}$ is $X$ because there is a split coequalizer diagram $R^{(2)} \rightrightarrows R \rightarrow X$ (with $X \to R$ and $R \to R^{(2)}$ defined in the obvious way).

Finally, we have a cartesian transformation of equalizer: $(R^{(2)} \rightrightarrows R) \to ( R \rightrightarrows X)$ where $R^{(2)} \to R$ is $(x_1,x_2,x_3) \mapsto (x_2,x_3)$ and $R \to X$ is $(x_1,x_2) \mapsto x_2$.

It then follows from the version of $(D2b)$ for coequalizer proved above that $R \to X \times_{E} X$ is a regular epimorphism (where $E =X/R$ is the coeqalizer).

But given that both $R$ and $X \times_E X$ are subobject of $X \times X$, this map is both a regular epimorphism and a monomorphism, hence it is an isomorphisms.

I find it a bit surprising, but I think you are correct. The proof I have is maybe a little too long for MO, so I'm only sketching it, but I'll be happy to provide more details if needed.

First one observe a form of "weak descent" for coequalizer diagram:

Lemma: Assume that the category $C$ satistifes all four condition of the op, then for any pair of coequalizer diagram $Y_0 \rightrightarrows Y_1 \to \text{coeq }Y_i$ and $X_0 \rightrightarrows X_1 \to \text{coeq }X_i$ and a cartesian natural transformation $X_0 \to Y_0$ , $X_1 \to Y_1$; the natural map $X_1 \to Y_1 \times_{\text{coeq } Y_i} (\text{coeq } X_i)$ is a regular epimorphism.

Proof: We use that a coequalizer $Y_0 \rightrightarrows Y_1$ can be written as a pushout $Y_1 \coprod_{Y_0 \coprod Y_1} Y_1$. Using that coproduct are disjoint and universal, one obtains that if $X_i \to Y_i$ is cartesian the map of spans from $X_1 \leftarrow X_0 \coprod X_1 \rightarrow X_1$ to $Y_1 \leftarrow Y_0 \coprod Y_1 \rightarrow Y_1$ is also cartesian, indeed, $(Y_0 \coprod Y_1) \times_{Y_1} X_1 = (Y_0 \times_{Y_1} X_1) \coprod (Y_1 \times_{Y_1} X_1) = X_0 \coprod X_1$.

and one can apply condition $(D2b)$ to this pushout.

With a bit more work, one can actually prove this also for $X_0 \to..$ and not just for coequalizer but for all colimits.

Now, we apply this to coequalizer of equivalence relation in a way inspired from the usual proof that descent for all colimits (in $\infty$-topos) implies that equivalence realtion are effective.

All the claim below are proved in the same way: they are clear for sets and we prove them for a general category with finite limits by interpreting everything in terms of "generalized" elements (or if you prefer by doing everything in terms of presheaves).

Consider now the case of an equivalence relation $R \rightrightarrows X$. Let $R^{(2)}$ be the subobject of $X^3$ corresponding to $\{ x_1,x_2,x_3 \in X^3 | x_1 R x_2 \text{ and } x_2 R x_3 \}$

$R^{(2)}$ has two maps to $R$ that sends $(x_1,x_2,x_3)$ to $(x_1,x_2)$ and $(x_1,x_3)$ and this makes $R^{(2)}$ into an equivalence relation on $R$. The coequalizer $R/R^{(2)}$ is $X$ because there is a split coequalizer diagram $R^{(2)} \rightrightarrows R \rightarrow X$ (with $X \to R$ and $R \to R^{(2)}$ defined in the obvious way).

Finally, we have a cartesian transformation of equalizer: $(R^{(2)} \rightrightarrows R) \to ( R \rightrightarrows X)$ where $R^{(2)} \to R$ is $(x_1,x_2,x_3) \mapsto (x_2,x_3)$ and $R \to X$ is $(x_1,x_2) \mapsto x_2$.

It then follows from the version of $(D2b)$ for coequalizer proved above that $R \to X \times_{E} X$ is a regular epimorphism (where $E =X/R$ is the coeqalizer).

But given that both $R$ and $X \times_E X$ are subobject of $X \times X$, this map is both a regular epimorphism and a monomorphism, hence it is an isomorphisms.

I find it a bit surprising, but I think you are correct. The proof I have is maybe a little too long for MO, so I'm only sketching it, but I'll be happy to provide more details if needed.

First one observe a form of "weak descent" for coequalizer diagram:

Lemme: Assume that the category $C$ satistifes all four condition of the op, then for any pair of coequalizer diagram $Y_0 \rightrightarrows Y_1 \to \text{coeq }Y_i$ and $X_0 \rightrightarrows X_1 \to \text{coeq }X_i$ and a cartesian natural transformation X_0 \to Y_0$ , $X_1 \to Y_1$; the natural map $X_1 \to Y_1 \times_{\text{coeq } Y_i} (\text{coeq } X_i)$ is a regular epimorphism.

Proof: We use that a coequalizer $Y_0 \rightrightarrows Y_1$ can be written as a pushout $Y_1 \coprod_{Y_0 \coprod Y_1} Y_1$. Using that coproduct are disjoint and universal, one obtains that if $X_i \to Y_i$ is cartesian the map of spans from $X_1 \leftarrow X_0 \coprod X_1 \rightarrow X_1$ to $Y_1 \leftarrow Y_0 \coprod Y_1 \rightarrow Y_1$ is also cartesian and one can apply condition $(D2b)$ to this pushout.

With a bit more work, one can actually prove this also for $X_0 \to..$ and not just for coequalizer but for all colimits.

Now, we apply this to coequalizer of equivalence relation in a way inspired from the usual proof that descent for all colimits (in $\infty$-topos) implies that equivalence realtion are effective.

All the claim below are proved in the same way: they are clear for sets and we prove them for a general category with finite limits by interpreting everything in terms of "generalized" elements (or if you prefer by doing everything in terms of presheaves).

Consider now the case of an equivalence relation $R \rightrightarrows X$. Let $R^{(2)}$ be the subobject of $X^3$ corresponding to $\{ x_1,x_2,x_3 \in X^3 | x_1 R x_2 \text{ and } x_2 R x_3 \}$

$R^{(2)}$ has two maps to $R$ that sends $(x_1,x_2,x_3)$ to $(x_1,x_2)$ and $(x_1,x_3)$ and this makes $R^{(2)}$ into an equivalence relation on $R$. The coequalizer $R/R^{(2)}$ is $X$ because there is a split coequalizer diagram $R^{(2)} \rightrightarrows R \rightarrow X$ (with $X \to R$ and $R \to R^{(2)}$ defined in the obvious way).

Finally, we have a cartesian transformation of equalizer: $(R^{(2)} \rightrightarrows R) \to ( R \rightrightarrows X)$ where $R^{(2)} \to R$ is $(x_1,x_2,x_3) \mapsto (x_2,x_3)$ and $R \to X$ is $(x_1,x_2) \mapsto x_2$.

It then follows from the version of $(D2b)$ for coequalizer proved above that $R \to X \times_{E} X$ is a regular epimorphism (where $E =X/R$ is the coeqalizer).

But given that both $R$ and $X \times_E X$ are subobject of $X \times X$, this map is both a regular epimorphism and a monomorphism, hence it is an isomorphisms.

I find it a bit surprising, but I think you are correct. The proof I have is maybe a little too long for MO, so I'm only sketching it, but I'll be happy to provide more details if needed.

First one observe a form of "weak descent" for coequalizer diagram:

Lemma: Assume that the category $C$ satistifes all four condition of the op, then for any pair of coequalizer diagram $Y_0 \rightrightarrows Y_1 \to \text{coeq }Y_i$ and $X_0 \rightrightarrows X_1 \to \text{coeq }X_i$ and a cartesian natural transformation $X_0 \to Y_0$ , $X_1 \to Y_1$; the natural map $X_1 \to Y_1 \times_{\text{coeq } Y_i} (\text{coeq } X_i)$ is a regular epimorphism.

Proof: We use that a coequalizer $Y_0 \rightrightarrows Y_1$ can be written as a pushout $Y_1 \coprod_{Y_0 \coprod Y_1} Y_1$. Using that coproduct are disjoint and universal, one obtains that if $X_i \to Y_i$ is cartesian the map of spans from $X_1 \leftarrow X_0 \coprod X_1 \rightarrow X_1$ to $Y_1 \leftarrow Y_0 \coprod Y_1 \rightarrow Y_1$ is also cartesian and one can apply condition $(D2b)$ to this pushout.

With a bit more work, one can actually prove this also for $X_0 \to..$ and not just for coequalizer but for all colimits.

Now, we apply this to coequalizer of equivalence relation in a way inspired from the usual proof that descent for all colimits (in $\infty$-topos) implies that equivalence realtion are effective.

All the claim below are proved in the same way: they are clear for sets and we prove them for a general category with finite limits by interpreting everything in terms of "generalized" elements (or if you prefer by doing everything in terms of presheaves).

Consider now the case of an equivalence relation $R \rightrightarrows X$. Let $R^{(2)}$ be the subobject of $X^3$ corresponding to $\{ x_1,x_2,x_3 \in X^3 | x_1 R x_2 \text{ and } x_2 R x_3 \}$

$R^{(2)}$ has two maps to $R$ that sends $(x_1,x_2,x_3)$ to $(x_1,x_2)$ and $(x_1,x_3)$ and this makes $R^{(2)}$ into an equivalence relation on $R$. The coequalizer $R/R^{(2)}$ is $X$ because there is a split coequalizer diagram $R^{(2)} \rightrightarrows R \rightarrow X$ (with $X \to R$ and $R \to R^{(2)}$ defined in the obvious way).

Finally, we have a cartesian transformation of equalizer: $(R^{(2)} \rightrightarrows R) \to ( R \rightrightarrows X)$ where $R^{(2)} \to R$ is $(x_1,x_2,x_3) \mapsto (x_2,x_3)$ and $R \to X$ is $(x_1,x_2) \mapsto x_2$.

It then follows from the version of $(D2b)$ for coequalizer proved above that $R \to X \times_{E} X$ is a regular epimorphism (where $E =X/R$ is the coeqalizer).

But given that both $R$ and $X \times_E X$ are subobject of $X \times X$, this map is both a regular epimorphism and a monomorphism, hence it is an isomorphisms.

I find it a bit surprising, but I think you are correct. The proof I have is maybe a little too long for MO, so I'm only sketching it, but I'll be happy to provide more details if needed.

First one observe that your four condition implies "weak descent" for all colimits. That is:

Lemme: Assume that the category $C$ satistifes all four condition of the op, then for any small category $I$, for any cartesian natural transformation $X_i \to Y_i$ of $I$-diagram in $C$, the natural map $X_i \to Y_i \times_{\text{colim } Y_i} (\text{colim } X_i)$ is a regular epimorphism.

Proof: On first show it when $I$ is a coequalizer diagram, using that a coequalizer $Y_0 \rightrightarrows Y_1$ can be written as a pushout $Y_1 \coprod_{Y_0 \coprod Y_1} Y_1$. Using that coproduct are disjoint and universal, one obtains that if $X_i \to Y_i$ is cartesian the map of spans from $X_1 \leftarrow X_0 \coprod X_1 \rightarrow X_1$ to $Y_1 \leftarrow Y_0 \coprod Y_1 \rightarrow Y_1$ is also cartesian and one can apply condition $(D2b)$ to this pushout.

The case of a general colimits is deduced in a similar way by writting a general colimit as an equalizer of coproducts in the usual way. Though in what follows we will only use coequalizer anyway.

All the claim below are proved in the same way: they are clear for sets and we prove them for a general category with finite limits by interpreting everything in terms of "generalized" elements (or if you prefer by doing everything in terms of presheaves).

Consider now the case of an equivalence relation $R \rightrightarrows X$. Let $R^{(2)}$ be the subobject of $X^3$ corresponding to $\{ x_1,x_2,x_3 \in X^3 | x_1 R x_2 \text{ and } x_2 R x_3 \}$

$R^{(2)}$ has two maps to $R$ that sends $(x_1,x_2,x_3)$ to $(x_1,x_2)$ and $(x_1,x_3)$ and this makes $R^{(2)}$ into an equivalence relation on $R$. The coequalizer $R/R^{(2)}$ is $X$ because there is a split coequalizer diagram $R^{(2)} \rightrightarrows R \rightarrow X$ (with $X \to R$ and $R \to R^{(2)}$ defined in the obvious way).

Finally, we have a cartesian transformation of equalizer: $(R^{(2)} \rightrightarrows R) \to ( R \rightrightarrows X)$ where $R^{(2)} \to R$ is $(x_1,x_2,x_3) \mapsto (x_2,x_3)$ and $R \to X$ is $(x_1,x_2) \mapsto x_2$.

It then follows from the version of $(D2b)$ for coequalizer proved above that $R \to X \times_{E} X$ is a regular epimorphism (where $E =X/R$ is the coeqalizer).

But given that both $R$ and $X \times_E X$ are subobject of $X \times X$, this map is both a regular epimorphism and a monomorphism, hence it is an isomorphisms.

I find it a bit surprising, but I think you are correct. The proof I have is maybe a little too long for MO, so I'm only sketching it, but I'll be happy to provide more details if needed.

First one observe a form of "weak descent" for coequalizer diagram:

Lemme: Assume that the category $C$ satistifes all four condition of the op, then for any pair of coequalizer diagram $Y_0 \rightrightarrows Y_1 \to \text{coeq }Y_i$ and $X_0 \rightrightarrows X_1 \to \text{coeq }X_i$ and a cartesian natural transformation X_0 \to Y_0$ , $X_1 \to Y_1$; the natural map $X_1 \to Y_1 \times_{\text{coeq } Y_i} (\text{coeq } X_i)$ is a regular epimorphism.

Proof: We use that a coequalizer $Y_0 \rightrightarrows Y_1$ can be written as a pushout $Y_1 \coprod_{Y_0 \coprod Y_1} Y_1$. Using that coproduct are disjoint and universal, one obtains that if $X_i \to Y_i$ is cartesian the map of spans from $X_1 \leftarrow X_0 \coprod X_1 \rightarrow X_1$ to $Y_1 \leftarrow Y_0 \coprod Y_1 \rightarrow Y_1$ is also cartesian and one can apply condition $(D2b)$ to this pushout.

With a bit more work, one can actually prove this also for $X_0 \to..$ and not just for coequalizer but for all colimits.

Now, we apply this to coequalizer of equivalence relation in a way inspired from the usual proof that descent for all colimits (in $\infty$-topos) implies that equivalence realtion are effective.

All the claim below are proved in the same way: they are clear for sets and we prove them for a general category with finite limits by interpreting everything in terms of "generalized" elements (or if you prefer by doing everything in terms of presheaves).

Consider now the case of an equivalence relation $R \rightrightarrows X$. Let $R^{(2)}$ be the subobject of $X^3$ corresponding to $\{ x_1,x_2,x_3 \in X^3 | x_1 R x_2 \text{ and } x_2 R x_3 \}$

$R^{(2)}$ has two maps to $R$ that sends $(x_1,x_2,x_3)$ to $(x_1,x_2)$ and $(x_1,x_3)$ and this makes $R^{(2)}$ into an equivalence relation on $R$. The coequalizer $R/R^{(2)}$ is $X$ because there is a split coequalizer diagram $R^{(2)} \rightrightarrows R \rightarrow X$ (with $X \to R$ and $R \to R^{(2)}$ defined in the obvious way).

Finally, we have a cartesian transformation of equalizer: $(R^{(2)} \rightrightarrows R) \to ( R \rightrightarrows X)$ where $R^{(2)} \to R$ is $(x_1,x_2,x_3) \mapsto (x_2,x_3)$ and $R \to X$ is $(x_1,x_2) \mapsto x_2$.

It then follows from the version of $(D2b)$ for coequalizer proved above that $R \to X \times_{E} X$ is a regular epimorphism (where $E =X/R$ is the coeqalizer).

But given that both $R$ and $X \times_E X$ are subobject of $X \times X$, this map is both a regular epimorphism and a monomorphism, hence it is an isomorphisms.