Definition disp_Equalizer {x y : C} {f g : x --> y} {xx : D x} {yy : D y} (ff : xx -->[ f ] yy) (gg : xx -->[ g ] yy) (e : Equalizer f g) : UU := ∑ (ee : D e) (ar_e : ee -->[ EqualizerArrow e ] xx) (pp : transportf (λ z, _ -->[ z ] _) (EqualizerEqAr e) (ar_e ;; ff) = ar_e ;; gg), is_disp_Equalizer e ee ar_e pp.
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.