proposition: Lemma show_is_equalizer : forall a u v y , equalizer_hypothesis a u v y -> (forall z z', mor a z -> mor a z' -> source y = target z -> source y = target z' -> comp a y z = comp a y z' -> z = z') -> (forall z, equalizer_hypothesis a u v z -> (exists w, (mor a w & source y = target w & comp a y w = z))) -> is_equalizer a u v y.
proof: Proof. ir. uhg; ee. am. uhg. ee. rww is_uni_equalizer_cone. rww is_versal_equalizer_cone. Qed.
imports: Arith colimits little_cat fc_limits cardinal