proposition: 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: 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.
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