Definition total_Equalizers (EC : Equalizers C) (DC : disp_Equalizers EC) : Equalizers (total_category D). Proof. intros x y f g. exact (total_Equalizer (pr2 f) (pr2 g) (EC _ _ (pr1 f) (pr1 g)) (DC _ _ _ _ _ _ (pr2 f) (pr2 g))). Defined.
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.