Proposition hset_equalizer_out_struct {X Y : hSet} {f g : X → Y} {PX : P X} {PY : P Y} (Pf : mor_hset_struct P PX PY f) (Pg : mor_hset_struct P PX PY g) {Z : hSet} (PZ : P Z) (h : Y → Z) (Ph : mor_hset_struct P PY PZ h) (q : (λ w, h(f w)) = (λ w, h(g w))) : mor_hset_struct P (hset_struct_coequalizer EP Pf Pg) PZ (coequalizer_out_hSet f g h (eqtohomot q)). Proof. exact (pr22 EP X Y f g PX PY Pf Pg Z PZ h Ph q). Qed.
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.