Proposition struct_pointed_poset_strict_with_smash_adj_laws : hset_struct_with_smash_closed_adj_laws struct_pointed_poset_strict_with_smash_closed_pointed. Proof. split. - intros PX PY PZ f. induction PX as [ X RX ]. induction PY as [ Y RY ]. induction PZ as [ Z RZ ]. induction f as [ f Hf ]. split. + use setquotunivprop'. { intro. repeat (use impred ; intro). apply propproperty. } intros xy₁. use setquotunivprop'. { intro. repeat (use impred ; intro). apply propproperty. } intros xy₂. use factor_through_squash. { apply propproperty. } cbn in *. induction xy₁ as [ x₁ y₁ ], xy₂ as [ x₂ y₂ ]. intro p. induction p as [ p | p ]. * revert p. use factor_through_squash. { apply propproperty. } cbn. intro p. induction p as [ p | p ]. ** assert (pr1 (f x₁) y₁ = ⊥_{RZ}) as r. { rewrite p. exact (eqtohomot (maponpaths pr1 (pr2 Hf)) y₁). } rewrite r. apply (pr2 RZ). ** assert (pr1 (f x₁) y₁ = ⊥_{RZ}) as r. { rewrite p. apply (pr2 (f x₁)). } rewrite r. apply (pr2 RZ). * cbn ; cbn in p. refine (trans_PartialOrder RZ _ _). ** exact (pr12 (f x₁) _ _ (pr2 p)). ** exact (pr1 Hf _ _ (pr1 p) y₂). + cbn. etrans. { apply maponpaths_2. exact (pr2 Hf). } apply idpath. - intros PX PY PZ f. induction PX as [ X RX ]. induction PY as [ Y RY ]. induction PZ as [ Z RZ ]. induction f as [ f Hf ]. split. + intros x₁ x₂ p y. apply (pr1 Hf). cbn in *. apply hinhpr. use inr. refine (p ,, _). apply refl_PartialOrder. + use eq_strict_and_monotone_function. intro y. cbn. refine (_ @ pr2 Hf). apply maponpaths. use iscompsetquotpr. apply hinhpr. use inr. unfold product_point_coordinate ; cbn. unfold pointed_struct_pointed_poset_strict_data. split. * exact (inl (idpath _)). * exact (inl (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.