proposition: Lemma target_codotted : forall a, is_cocone a -> has_colimit (cosocle a) -> target (codotted a) = vertex a.
proof: Proof. ir. uf codotted. rww target_colimit_to_cocone. app is_colimit_colimit. rww cosocle_colimit. Qed.
imports: Arith limits