proposition: Lemma cocone_compose_codotted : forall a, is_cocone a -> has_colimit (cosocle a) -> cocone_compose (codotted a) (colimit (cosocle a)) = a.
proof: Proof. ir. uf codotted. rww cocone_compose_colimit_to_cocone. app is_colimit_colimit. rww cosocle_colimit. Qed.
imports: Arith limits