Definition is_disp_Coequalizer {x y : C} {f g : x --> y} (e : Coequalizer f g) {xx : D x} {yy : D y} {ff : xx -->[ f ] yy} {gg : xx -->[ g ] yy} (ee : D e) (ar_e : yy -->[ CoequalizerArrow e ] ee) (pp : transportf (λ z, _ -->[ z ] _) (CoequalizerEqAr e) (ff ;; ar_e) = gg ;; ar_e) : UU := ∏ (w : C) (ww : D w) (h : y --> w) (hh : yy -->[ h ] ww) (q : f · h = g · h) (qq : transportf (λ z, _ -->[ z ] _) q (ff ;; hh) = gg ;; hh), ∃! (ii : ee -->[ CoequalizerOut e w h q ] ww), transportf (λ z, _ -->[ z ] _) (CoequalizerCommutes e w h q) (ar_e ;; ii) = hh.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total.