Proposition struct_pointed_poset_strict_with_smash_laws_enrich : hset_struct_with_smash_closed_laws_enrich struct_pointed_poset_strict_with_smash_adj. 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.
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.