proposition: Lemma cone_composable_equalizer_cone : forall a u v y z, equalizer_hypothesis a u v y -> mor a z -> source y = target z -> cone_composable (equalizer_cone a u v y) z.
proof: Proof. ir. uhg; ee. app is_cone_equalizer_cone. rww cone_target_equalizer_cone. rww vertex_equalizer_cone. sy; am. Qed.
imports: Arith colimits little_cat fc_limits cardinal