Proposition struct_pointed_poset_strict_with_smash_laws : hset_struct_with_smash_laws struct_pointed_poset_strict_with_smash_data. 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.
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.