Definition composition_preserves_reflexive_coequalizer {C₁ C₂ C₃ : category} {F : C₁ ⟶ C₂} {G : C₂ ⟶ C₃} (HF : preserves_reflexive_coequalizer F) (HG : preserves_reflexive_coequalizer G) : preserves_reflexive_coequalizer (F ∙ G). Proof. intros x y c f g s pf pg h p Fp Hx. use (HG (F x) (F y) (F c) (#F f) (#F g) (#F s) _ _ (#F h)). - abstract (rewrite <- functor_comp ; rewrite pf ; apply functor_id). - abstract (rewrite <- functor_comp ; rewrite pg ; apply functor_id). - abstract (rewrite <- !functor_comp ; rewrite p ; apply idpath). - use (HF x y c f g s _ _ h). + exact pf. + exact pg. + exact p. + exact Hx. 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.