Definition equalizers_struct_poset : hset_equalizer_struct struct_poset. Proof. simple refine (_ ,, _). - intros X Y f g PX PY Pf Pg. exact (Equalizer_order PX _ f g). - repeat split. + abstract (intros X Y f g PX PY Pf Pg ; cbn in * ; exact (Equalizer_pr1_monotone PX Y f g)). + abstract (intros X Y f g PX PY Pf Pg W PW h Ph q ; exact (Equalizer_map_monotone PX Y f g PW Ph (eqtohomot q))). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits.