proposition: Lemma codotted_colimit : forall f, Functor.axioms f -> has_colimit f -> codotted (colimit f) = id (target f) (vertex (colimit f)).
proof: Proof. ir. uf codotted. rww cosocle_colimit. rw colimit_to_cocone_refl. rw cocone_target_colimit. tv. am. app is_colimit_colimit. Qed.
imports: Arith limits