proposition: Lemma is_colimit_invertible_codotted : forall a, is_colimit a -> invertible (cocone_target a) (codotted a).
proof: Proof. ir. uf codotted. assert (has_colimit (cosocle a)). uhg. sh a. uhg; ee. am. tv. ap invertible_colimit_to_cocone. ap is_colimit_colimit. am. am. rww cosocle_colimit. rw cocone_target_colimit. rww target_cosocle. am. Qed.
imports: Arith limits