proposition: Lemma source_eqzmap : forall c, is_cone c -> cone_source c = twoarrow_cat -> source (eqzmap c) = vertex c.
proof: Proof. ir. uf eqzmap. rww source_edge. rw H0. app ob_twoarrow_cat. Qed.
imports: Arith colimits little_cat fc_limits cardinal