proposition: Lemma equalizer_hypothesis_comp : forall a u v y z, equalizer_hypothesis a u v y -> mor a z -> source y = target z -> equalizer_hypothesis a u v (comp a y z).
proof: Proof. ir. uh H; uhg; ee. am. rww mor_comp. rww target_comp. wrr assoc. rw H4. rww assoc. uh H; ee. am. uh H; ee. wrr H6. uh H; ee; am. Qed.
imports: Arith colimits little_cat fc_limits cardinal