proposition: Lemma Epic_Equalizer_id : Epic_law (E_mor f) -> Equalizer_eq (Id a).
proof: Proof. unfold Equalizer_eq in |- *. intros ep i1 i2. apply Trans with (k i1). apply Idl. apply Trans with (k i2). apply ep. apply (Prf_E_law1 f i1 i2). apply Sym; apply Idl. Qed.
imports: CatProperty