proposition: Proposition struct_pointed_poset_strict_with_smash_laws : hset_struct_with_smash_laws struct_pointed_poset_strict_with_smash_data.
proof: Proof. repeat split. - intros b₁ b₂ p ; cbn in p. induction b₁, b₂. + apply refl_PartialOrder. + induction p. + apply pointed_PartialOrder_min_point. + apply refl_PartialOrder. - intros x y p . unfold pointed_hset_struct_unit_map ; cbn. unfold pointed_struct_pointed_poset_strict_data. assert (q := pr1 Pf x y p) ; cbn in q. induction (f x), (f y). + apply Pg. exact p. + induction q. + apply (pr2 PY). + apply (pr2 PY). - unfold pointed_hset_struct_unit_map. cbn. unfold pointed_struct_pointed_poset_strict_data. induction (f ⊥_{PX}). + apply Pg. + apply idpath. - intros x₁ x₂ p ; cbn. apply hinhpr. use inr. refine (p ,, _). apply refl_PartialOrder. - use iscompsetquotpr ; cbn. apply hinhpr. use inr. unfold product_point_coordinate ; cbn. unfold pointed_struct_pointed_poset_strict_data. split. + exact (inl (idpath _)). + exact (inl (idpath _)). - intros y₁ y₂ p ; cbn. apply hinhpr. use inr. exact (refl_PartialOrder (pr1 PX) x ,, p). - use iscompsetquotpr ; cbn. apply hinhpr. use inr. unfold product_point_coordinate ; cbn. unfold pointed_struct_pointed_poset_strict_data. split. + exact (inr (idpath _)). + exact (inr (idpath _)). - intros xy₁ xy₂ p ; cbn. apply hinhpr. use inr. exact p. - use setquotunivprop'. { intro. repeat (use impred ; intro). apply propproperty. } intros xy₁. use setquotunivprop'. { intro. repeat (use impred ; intro). apply propproperty. } intros xy₂. induction xy₁ as [ x₁ y₁ ]. induction xy₂ as [ x₂ y₂ ] ; cbn. use factor_through_squash. { apply propproperty. } intro p. induction p as [ p | p]. + revert p. use factor_through_squash. { apply propproperty. } intro p. induction p as [ p | p ] ; rewrite p. * assert (h ⊥_{PX} y₁ = ⊥_{PZ}) as q. { refine (!(hp₂ (⊥_{PX}) y₁) @ _). apply (pr2 Ph). } rewrite q. apply (pr2 PZ). * assert (h x₁ ⊥_{PY} = ⊥_{PZ}) as q. { refine (hp₂ x₁ (⊥_{PY}) @ _). apply (pr2 Ph). } rewrite q. apply (pr2 PZ). + exact (pr1 Ph (x₁ ,, y₁) (x₂ ,, y₂) p). - apply (pr2 Ph). 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