proposition: Lemma codotted_unique : forall f u, Functor.axioms f -> has_colimit f -> cocone_composable u (colimit f) -> codotted (cocone_compose u (colimit f)) = u.
proof: Proof. ir. rw codotted_cocone_compose. rw codotted_colimit. rw cocone_target_colimit. rw right_id. tv. assert (target f = cocone_target (colimit f)). rww cocone_target_colimit. rw H2. app ob_vertex. ap is_colimit_is_cocone. app is_colimit_colimit. uh H1; ee. rwi cocone_target_colimit H2. am. am. uh H1; ee. am. tv. am. am. am. am. rww cosocle_colimit. Qed.
imports: Arith limits