proposition: Proposition struct_pointed_poset_strict_with_smash_laws_enrich : hset_struct_with_smash_closed_laws_enrich struct_pointed_poset_strict_with_smash_adj.
proof: Proof. split. - intros PX PY PZ. induction PX as [ X RX ]. induction PY as [ Y RY ]. induction PZ as [ Z RZ ]. split. + intros f₁ f₂ p. use setquotunivprop'. { intro. apply propproperty. } intros xz. induction xz as [ x z ]. cbn in *. apply p. + use eq_strict_and_monotone_function. use setquotunivprop'. { intro. apply setproperty. } intro x ; cbn in *. apply idpath. - intros PX PY PZ. induction PX as [ X RX ]. induction PY as [ Y RY ]. induction PZ as [ Z RZ ]. split. + intros f₁ f₂ p x y. cbn in *. apply p. + use eq_strict_and_monotone_function. intro x. use eq_strict_and_monotone_function. intro z. cbn. apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Categories.HSET.All UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits UniMath.CategoryTheory.DisplayedCats.Structures.StructuresSmashProduct