proposition: Lemma if_has_colimit : forall f, has_colimit f -> is_colimit_of f (colimit f).
proof: Proof. ir. uhg. ee. uf colimit. ap is_colimit_oppc. ap is_limit_limit. ap has_limit_oppf. am. uf colimit. rw cosocle_oppc. rw socle_limit. rw oppf_oppf. tv. app has_limit_oppf. app is_limit_is_cone. app is_limit_limit. app has_limit_oppf. Qed.
imports: Arith limits