Definition is_coequalizer_cod_fib : isCoequalizer ρ₁ ρ₂ i p. Proof. intros wφ k q. use iscontraprop1. - apply is_coequalizer_cod_fib_unique. - simple refine (_ ,, _). + exact (is_coequalizer_cod_fib_mor k q). + apply is_coequalizer_cod_fib_eq. 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.