Proposition pointed_struct_pointed_hset_with_smash_laws : hset_struct_with_smash_laws pointed_struct_pointed_hset_with_smash_data. 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.
Require Import UniMath.MoreFoundations.All. 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.