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