proposition: Lemma eqz_dotted_uni : forall a u v y r, has_equalizer a u v -> equalizer_hypothesis a u v y -> cone_composable (equalizer_cone a u v (equalizer a u v)) r -> cone_compose (equalizer_cone a u v (equalizer a u v)) r = equalizer_cone a u v y -> eqz_dotted a u v y = r.
proof: Proof. ir. uf eqz_dotted. wr H2. rw equalizer_cone_equalizer. ap dotted_unique. ap twoarrow_functor_axioms. uh H0; ee; am. uh H; ee; am. wr equalizer_cone_equalizer. am. am. am. Qed.
imports: Arith colimits little_cat fc_limits cardinal