Definition total_Coequalizers (EC : Coequalizers C) (DC : disp_Coequalizers EC) : Coequalizers (total_category D). Proof. intros x y f g. exact (total_Coequalizer (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.