Definition is_disp_Equalizer {x y : C} {f g : x --> y} (e : Equalizer f g) {xx : D x} {yy : D y} {ff : xx -->[ f ] yy} {gg : xx -->[ g ] yy} (ee : D e) (ar_e : ee -->[ EqualizerArrow e ] xx) (pp : transportf (λ z, _ -->[ z ] _) (EqualizerEqAr e) (ar_e ;; ff) = ar_e ;; gg) : UU := ∏ (w : C) (ww : D w) (h : w --> x) (hh : ww -->[ h ] xx) (q : h · f = h · g) (qq : transportf (λ z, _ -->[ z ] _) q (hh ;; ff) = hh ;; gg), ∃! (ii : ww -->[ EqualizerIn e w h q ] ee), transportf (λ z, _ -->[ z ] _) (EqualizerCommutes e w h q) (ii ;; ar_e) = 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.