proposition: Proposition pointed_struct_pointed_hset_with_smash_laws : hset_struct_with_smash_laws pointed_struct_pointed_hset_with_smash_data.
proof: Proof. repeat split. - intros X Y x y f pf g pg. cbn in *. unfold pointed_hset_struct_unit_map. rewrite pf. apply idpath. - intro y. use iscompsetquotpr. apply hinhpr. use inr. unfold product_point_coordinate ; cbn. unfold pointed_struct_pointed_hset_data. split. + exact (inl (idpath _)). + exact (inl (idpath _)). - intro x. use iscompsetquotpr. apply hinhpr. use inr. unfold product_point_coordinate ; cbn. unfold pointed_struct_pointed_hset_data. split. + exact (inr (idpath _)). + exact (inr (idpath _)). - intros Z z h Ph hp₁ hp₂ hp₃ ; cbn in *. exact Ph. Qed.
imports: UniMath.MoreFoundations.All 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