proposition: Lemma has_colimits_functor_cat : forall a b z, Category.axioms a -> Category.axioms b -> Category.axioms z -> has_colimits_over z b -> has_colimits_over z (functor_cat a b).
proof: Proof. ir. assert (Category.axioms (opp a)). app opp_axioms. assert (Category.axioms (opp b)). app opp_axioms. assert (Category.axioms (opp z)). app opp_axioms. assert (has_limits_over (opp z) (opp (functor_cat a b))). apply has_limits_over_finverse_invariance with (functor_cat (opp a) (opp b)). app functor_cat_axioms. ap opp_axioms. app functor_cat_axioms. am. app has_limits_functor_cat. app has_limits_over_opp. sh (fc_opp a b). sh (opp_fc a b). ee. app are_finverse_symm. app are_finverse_opp_fc_fc_opp. rw source_fc_opp. reflexivity. rw target_fc_opp. reflexivity. assert (z = opp (opp z)). rww opp_opp. assert (functor_cat a b = opp (opp (functor_cat a b))). sy; rw opp_opp. reflexivity. rw H7; rw H8. ap has_colimits_over_opp. ap opp_axioms. app functor_cat_axioms. am. am. Qed.
imports: Arith colimits functor_cat