Definition preserves_chosen_reflexive_coequalizer {C₁ C₂ : category} (HC₁ : reflexive_coequalizers C₁) (F : C₁ ⟶ C₂) : UU := ∏ (x y : C₁) (f g : x --> y) (s : y --> x) (pf : s · f = identity _) (pg : s · g = identity _) (p : # F f · # F (CoequalizerArrow (HC₁ x y f g s pf pg)) = # F g · # F (CoequalizerArrow (HC₁ x y f g s pf pg))), isCoequalizer (#F f) (#F g) (#F (CoequalizerArrow (HC₁ x y f g s pf pg))) p.
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.