fact: Structure Equalizer : Type := {E_ob : C; E_mor : E_ob --> a; Prf_E_law1 : Equalizer_law1 E_mor; E_diese : forall (r : C) (h : r --> a), Equalizer_eq h -> (r --> E_ob); Prf_E_law2 : Equalizer_law2 E_mor E_diese; Prf_E_law3 : Equalizer_law3 E_mor E_diese}.
imports: CatProperty