Definition preserves_coequalizer_if_preserves_chosen {C₁ C₂ : category} (HC₁ : Coequalizers C₁) (F : C₁ ⟶ C₂) (HF : preserves_chosen_coequalizer HC₁ F) : preserves_coequalizer F. Proof. intros x y c f g h p Fp Hz. use (Coequalizer_eq_ar _ _ _ (pr22 (z_iso_to_Coequalizer (make_Coequalizer _ _ _ _ (HF x y f g _)) (z_iso_inv (functor_on_z_iso F (z_iso_between_Coequalizer (make_Coequalizer _ _ _ _ Hz) (HC₁ x y f g))))))) ; cbn. - abstract (rewrite <- !functor_comp ; rewrite CoequalizerCommutes ; apply idpath). - abstract (rewrite <- !functor_comp ; rewrite CoequalizerEqAr ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Adjunctions.Core.