Definition total_Equalizer : @Equalizer (total_category D) t_x t_y t_f t_g. Proof. use make_Equalizer. - exact t_e. - exact t_i. - exact total_Equalizer_path. - intros w h q. use iscontraprop1. + apply total_Equalizer_unique. exact q. + simple refine (_ ,, _). * exact (total_EqualizerIn (pr2 h) q). * exact (total_EqualizerIn_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.