Definition disp_Coequalizers_hset_disp_struct {P : hset_struct} (EP : hset_coequalizer_struct P) : disp_Coequalizers (hset_struct_disp_cat P) Coequalizers_HSET. Proof. intros X Y f g PX PY Pf Pg. simple refine (_ ,, _ ,, _ ,, _). - exact (hset_struct_coequalizer EP Pf Pg). - exact (hset_coequalizer_map_struct EP Pf Pg). - apply isaprop_hset_struct_on_mor. - intros W PW h Ph q qq. use iscontraprop1. + abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply isasetaprop ; apply isaprop_hset_struct_on_mor | ] ; apply isaprop_hset_struct_on_mor). + simple refine (_ ,, _). * exact (hset_equalizer_out_struct EP Pf Pg PW h Ph q). * apply isaprop_hset_struct_on_mor. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Binproducts. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Monads.MonadAlgebras. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure.