Definition preserves_reflexive_coequalizers_if_chosen {C₁ C₂ : category} (HC₁ : reflexive_coequalizers C₁) (F : C₁ ⟶ C₂) (HF : preserves_chosen_reflexive_coequalizer HC₁ F) : preserves_reflexive_coequalizer F. Proof. intros x y c f g s pf pg h p Fp Hz. use (Coequalizer_eq_ar _ _ _ (pr22 (z_iso_to_Coequalizer (make_Coequalizer _ _ _ _ (HF x y f g s pf pg _)) (z_iso_inv (functor_on_z_iso F (z_iso_between_Coequalizer (make_Coequalizer _ _ _ _ Hz) (HC₁ x y f g s pf pg))))))) ; 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.