I want to prove that weak descent of a $1$-category implies the classical Giraud axioms.


More precisely, let $\mathsf{C}$ be a cocomplete, finitely complete $1$-category. We say that $\mathsf{C}$ satisfies weak descent if the following conditions are satisfied:


* $(\mathbf{D1}a)$-(Universal coproducts): Given a collection of objects $\{ Y\_i \}\_{i \in I}$, let $Y = \coprod\_i Y\_i$. Let $f: X \to Y$ be a morphism, and let $X\_i = Y\_i \times\_Y X$. Then the induced map $\coprod\_i X\_i \to X$ is an isomorphism,
* $(\mathbf{D1}b)$-(Universal pushouts): Given a span $Y\_0 \leftarrow Y\_1 \to Y\_2$, let $Y = Y\_0 \coprod\_{Y\_1} Y\_2$. Let $f: X \to Y$ be a morphism and let $X\_i = Y\_i \times\_{Y} X$. Then the induced map $X\_0 \coprod\_{X\_1} X\_2 \to X$ is an isomorphism.
* $(\mathbf{D2}a)$-(Effective coproducts): Given a collection of maps $\{ f\_i: X\_i \to Y\_i \}$, let $X = \coprod\_i X\_i$, and $Y = \coprod\_i Y\_i$, and let $f: X \to Y$ be the coproduct $\coprod\_i f\_i$. Then the natural maps $X\_i \to Y\_i \times\_Y X$ are isomorphisms for each $i$.
* $(\mathbf{D2}b)$-(Weak effective pushouts): Given a map of spans:
$\require{AMScd}$
\begin{CD}
X\_0 @<<< X\_1 @>>> X\_2\\
@Vf\_0VV @Vf\_1VV @Vf\_2VV\\
Y\_0 @<<< Y\_1 @>>> Y\_2
\end{CD}
such that each square is a pullback square, let $X = X\_0 \coprod\_{X\_1} X\_2$ and $Y = Y\_0 \coprod\_{Y\_1} Y\_2$, and let $f:X \to Y$ denote the induced map of pushouts. Then the natural maps $X\_i \to Y\_i \times\_Y X$ are regular epimorphisms.


Condition $(\mathbf{D2}b)$ is the real difference between $1$-topoi and $\infty$-topoi, and I am trying to better understand this comparison. Now recall the classical Giraud Axioms:


* $(\mathbf{G1})$ Coproducts are disjoint, namely $A \times\_{A \coprod B} B \cong \varnothing$,
* $(\mathbf{G2})$ For any morphism $f: X \to Y$, the base change functor $f^\*: \mathsf{C}\_{/Y} \to \mathsf{C}\_{/X}$ preserves colimits,
* $(\mathbf{G3})$ Equivalence relations are effective.


Rezk [sketches](https://faculty.math.illinois.edu/%7Erezk/leeds-lectures-2019.pdf) how to prove that $(\mathbf{D1}) = (\mathbf{D1}a) \wedge (\mathbf{D1}b)$ is equivalent to $(\mathbf{G2})$, and that $(\mathbf{D2}a) \implies (\mathbf{G1})$.


My suspicion is that $(\mathbf{D2}b) \implies (\mathbf{G3})$ or is possibly equivalent to it, but I can't quite see how to prove it. I also suspect that the way one can prove it by is proving that $(\mathbf{D2}b)$ is equivalent to the coequalizer defining equivalence relations being effective. Namely if $R \xrightarrow{(s,t)} X \times X$ is an equivalence relation, then $R \rightrightarrows X \to X/R$ is a coequalizer iff $X/R \cong R \coprod\_{R \coprod R} X$, and my idea is to show that having condition $(\mathbf{D2}b)$ hold, but this time up to isomorphism rather than regular epi but only for pushouts of equivalence relations as above, and this would be equivalent to $(\mathbf{D2}b)$ and from this somehow it would be easier to see that it implies $(\mathbf{G3})$, but I've had no luck with this either.


Any ideas or insight would be appreciated.



Weak descent and effective equivalence relations
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.


