proposition: Lemma mor_codotted : forall a, is_cocone a -> has_colimit (cosocle a) -> mor (cocone_target a) (codotted a).
proof: Proof. ir. uf codotted. app mor_colimit_to_cocone. app is_colimit_colimit. rww cosocle_colimit. uf cocone_target. rww cosocle_colimit. Qed.
imports: Arith limits