Definition total_Coequalizer : @Coequalizer (total_category D) t_x t_y t_f t_g. Proof. use make_Coequalizer. - exact t_e. - exact t_i. - exact total_Coequalizer_path. - intros w h q. use iscontraprop1. + apply total_Coequalizer_unique. exact q. + simple refine (_ ,, _). * exact (total_CoequalizerOut (pr2 h) q). * exact (total_CoequalizerOut_commutes (pr2 h) q). 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.