proposition: Lemma limit_oppf : forall f, has_colimit f -> limit (oppf f) = oppc (colimit f).
proof: Proof. ir. uf colimit. rw oppc_oppc_cone. tv. ap is_limit_is_cone. ap is_limit_limit. app has_limit_oppf. Qed.
imports: Arith limits