I was thinking about the theorem that an elementary topos is co-Malcev, and how I would prove it -- and the proof I came up with seems to only require the hypotheses of being regular, epi-regular, and distributive. The idea is: given a reflexive corelation $X \sqcup X \to R \to X$, use the hypotheses to express the first map as the coequalizer of its kernel pair. By distributivity, that kernel pair is equivalent to a subobject of $(X \times X)^{\sqcup 4}$, which can be described semi-pictorially as: in the lower left and upper right quadrants, $\Delta_X$, and in the lower right and upper left quadrants, $\Delta_E$ where $E$ is the equalizer of the two maps $X \to R$. Using that, and the expression of $R$ as a coequalizer of $X \sqcup X$, it should then be straightforward to construct the required symmetry morphism $R \to R$ and the required transitivity morphism from $R$ to the pushout.
And a very rough sketch of the picture I have in my mind of the situation:
-----------
----------- <- X u X
|
V
---\ /--- <- X_1 <- R
---- <- E <- X_1 <- X_2 <- R
---/ \--- <- X_2 <- R
|
V
----------- <- X
(And the pushout would be the middle diagram but with each branching part repeated three times instead of twice. Then the symmetry morphism looks like "flipping R upside down" and the transitivity morphism looks like "sending R to the first and third branches".)
Anyway, I also did a quick search through the database and found no counterexamples to dissuade me of the validity of the argument.
I was thinking about the theorem that an elementary topos is co-Malcev, and how I would prove it -- and the proof I came up with seems to only require the hypotheses of being regular, epi-regular, and distributive. The idea is: given a reflexive corelation$X \sqcup X \to R \to X$ , use the hypotheses to express the first map as the coequalizer of its kernel pair. By distributivity, that kernel pair is equivalent to a subobject of $(X \times X)^{\sqcup 4}$ , which can be described semi-pictorially as: in the lower left and upper right quadrants, $\Delta_X$ , and in the lower right and upper left quadrants, $\Delta_E$ where $E$ is the equalizer of the two maps $X \to R$ . Using that, and the expression of $R$ as a coequalizer of $X \sqcup X$ , it should then be straightforward to construct the required symmetry morphism $R \to R$ and the required transitivity morphism from $R$ to the pushout.
And a very rough sketch of the picture I have in my mind of the situation:
(And the pushout would be the middle diagram but with each branching part repeated three times instead of twice. Then the symmetry morphism looks like "flipping R upside down" and the transitivity morphism looks like "sending R to the first and third branches".)
Anyway, I also did a quick search through the database and found no counterexamples to dissuade me of the validity of the argument.