proposition: Lemma cone_composable_eqz_dotted : forall a u v y, has_equalizer a u v -> equalizer_hypothesis a u v y -> cone_composable (equalizer_cone a u v (equalizer a u v)) (eqz_dotted a u v y).
proof: Proof. ir. uf eqz_dotted. rw equalizer_cone_equalizer. assert (twoarrow_functor a u v = socle (equalizer_cone a u v y)). rww socle_equalizer_cone. rw H1. ap cone_composable_dotted. app is_cone_equalizer_cone. rw socle_equalizer_cone. uh H; ee; am. am. Qed.
imports: Arith colimits little_cat fc_limits cardinal