Definition equalizers_struct_pointed_poset_strict : hset_equalizer_struct struct_pointed_poset_strict. Proof. simple refine (_ ,, _). - intros X Y f g PX PY Pf Pg. exact (Equalizer_pointed_PartialOrder Pf Pg). - split. + abstract (intros X Y f g PX PY Pf Pg ; cbn in * ; exact (Equalizer_pr1_strict_and_monotone Pf Pg)). + abstract (intros X Y f g PX PY Pf Pg W PW h Ph q ; exact (Equalizer_map_strict_and_monotone Pf Pg 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. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructuresSmashProduct.