Proposition pointed_poset_strict_smash_eqrel_equiv {X Y : hSet} (PX : pointed_PartialOrder X) (PY : pointed_PartialOrder Y) (xy₁ xy₂ : X × Y) : smash_eqrel cartesian_struct_pointed_poset_strict pointed_struct_pointed_poset_strict PX PY xy₁ xy₂ <-> @downward_closed_to_eqrel (X × Y)%set (smash_set PX PY) xy₁ xy₂. Proof. induction xy₁ as [ x₁ y₁ ]. induction xy₂ as [ x₂ y₂ ]. split. - use factor_through_squash. { apply propproperty. } intro p. unfold product_point_coordinate in p. cbn in p. unfold pointed_struct_pointed_poset_strict_data in p. apply hinhpr. induction p as [ p | p ]. + exact (inl p). + apply inr. split. * exact (hinhpr (pr1 p)). * exact (hinhpr (pr2 p)). - use factor_through_squash. { apply propproperty. } intro p. unfold smash_set in p ; cbn in p. induction p as [ p | p ]. + exact (hinhpr (inl p)). + assert (p₁ := pr1 p). revert p₁. use factor_through_squash. { apply propproperty. } intros p₁. assert (p₂ := pr2 p). revert p₂. use factor_through_squash. { apply propproperty. } intros p₂. apply hinhpr. apply inr. unfold product_point_coordinate ; cbn. unfold pointed_struct_pointed_poset_strict_data. split. * exact p₁. * exact p₂. 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.