proposition: Lemma mor_eqz_dotted : forall a u v y, has_equalizer a u v -> equalizer_hypothesis a u v y -> mor a (eqz_dotted a u v y).
proof: Proof. ir. cp (cone_composable_eqz_dotted H H0). uh H1; ee. rwi cone_target_equalizer_cone H2. am. Qed.
imports: Arith colimits little_cat fc_limits cardinal