proposition: Lemma has_limits_over_opp : forall b c, Category.axioms b -> Category.axioms c -> has_colimits_over c b -> has_limits_over (opp c) (opp b).
proof: Proof. ir. uhg. ir. assert (f = oppf (oppf f)). rww oppf_oppf. rw H5. ap has_limit_oppf. uh H1. ap H1. app oppf_axioms. rw source_oppf. rw H3. rww opp_opp. am. rw target_oppf. rw H4. rww opp_opp. am. Qed.
imports: Arith limits