Proposition hset_equalizer_arrow_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) {W : hSet} (PW : P W) (h : W → X) (Ph : mor_hset_struct P PW PX h) (q : (λ w, f(h w)) = (λ w, g(h w))) : mor_hset_struct P PW (hset_struct_equalizer EP Pf Pg) (λ w, h w ,, eqtohomot q w). Proof. exact (pr22 EP X Y f g PX PY Pf Pg W PW 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.