Lean4
/-- Composition of morphisms in the diagram indexing reflexive (co)equalizers -/
def comp : ∀ {X Y Z : WalkingReflexivePair} (_ : Hom X Y) (_ : Hom Y Z), Hom X Z
| _, _, _, id _, h => h
| _, _, _, h, id _ => h
| _, _, _, reflexion, left => id zero
| _, _, _, reflexion, right => id zero
| _, _, _, reflexion, rightCompReflexion => reflexion
| _, _, _, reflexion, leftCompReflexion => reflexion
| _, _, _, left, reflexion => leftCompReflexion
| _, _, _, right, reflexion => rightCompReflexion
| _, _, _, rightCompReflexion, rightCompReflexion => rightCompReflexion
| _, _, _, rightCompReflexion, leftCompReflexion => rightCompReflexion
| _, _, _, rightCompReflexion, right => right
| _, _, _, rightCompReflexion, left => right
| _, _, _, leftCompReflexion, left => left
| _, _, _, leftCompReflexion, right => left
| _, _, _, leftCompReflexion, rightCompReflexion => leftCompReflexion
| _, _, _, leftCompReflexion, leftCompReflexion => leftCompReflexion
