Direct proof that pointed protomodularity implies the Mal'cev property

Question

It is a theorem that a finitely complete protomodular category is Mal'cev. The proof in the Bourn-Borceux monograph relies on classification via the fibration of points.

Is there perhaps a more direct proof in the pointed case? That is, how can one prove directly that pointed protomodularity implies every reflexive relation is an equivalence relation? I don't see how to use protomodularity to obtain symmetry and transitivity arrows for a given reflexive relation.

The obvious proof for groups relies on using inverses and I don't see how to generalize it to the pointed-protomodular case.

Answer 1

There is a direct proof valid in any category with finite limits. It is given as Theorem 5.9 (pages 16-17) in these notes, and as Theorem 3.18 in Chapter IV of the book Categorical Foundations.

Answer 2

Zurab Janelidze has done quite a bit of work on characterizing categories via the properties of their internal relations. In particular he characterizes pointed protomodular categories via their internal relations in the paper Closedness Properties of Internal Relations III: Pointed Protomodular Categories, which then trivially implies that pointed protomodular categories are Mal'cev when you use the characterization of Mal'cev categories via their relations (as he does in the paper). Whether you find this is more or less direct than Bourn's proof will I guess depend on whether you're willing to take Janelidze's relational approach as more basic than the fibrational approach of Bourn.