proposition: Lemma cocone_composable_codotted : forall a, is_cocone a -> has_colimit (cosocle a) -> cocone_composable (codotted a) (colimit (cosocle a)).
proof: Proof. ir. uf cocone_composable. ee. ap is_colimit_is_cocone. app is_colimit_colimit. rww cocone_target_colimit. rw target_cosocle. app mor_codotted. rww source_codotted. Qed.
imports: Arith limits