proposition: Lemma eqzmap_equalizer_cone : forall a u v y, equalizer_hypothesis a u v y -> eqzmap (equalizer_cone a u v y) = y.
proof: Proof. ir. uf eqzmap. rw edge_equalizer_cone_R. tv. Qed.
imports: Arith colimits little_cat fc_limits cardinal