Definition coequalizers_cod_fib {C : category} (y : C) (H : Coequalizers C) : Coequalizers (C/y). Proof. intros f g ρ₁ ρ₂. use make_Coequalizer. - exact (coequalizers_cod_fib_coeq H ρ₁ ρ₂). - apply coequalizers_cod_fib_map. - apply coequalizers_cod_fib_eq. - use is_coequalizer_cod_fib. + abstract (apply CoequalizerEqAr). + apply isCoequalizer_Coequalizer. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod.