proposition: Proposition make_smash_struct_enrichment_laws : smash_struct_enrichment_laws make_smash_struct_enrichment_data.
proof: Proof. repeat split. - intros x y z. use (transportf_struct_mor_prod_via_eq P). + exact (λ fg, pr1 (enriched_comp E x y z) (setquotpr _ fg)). + abstract (refine (hset_struct_comp P _ (pr2 (enriched_comp E x y z))) ; apply hset_struct_with_smash_setquotpr). + intros fg ; cbn. unfold enriched_smash_hom_to_mor. rewrite (enriched_to_arr_comp E). apply maponpaths. use eq_mor_hset_struct. intro b ; induction b ; cbn. * apply idpath. * pose (pointed_hset_struct_preserve_point P (pr2 (enriched_comp E x y z))) as p. refine (_ @ p). apply maponpaths. refine (_ @ !(hset_struct_with_smash_point_smash _ _ _)). use iscompsetquotpr. apply hinhpr. use inr. split ; unfold product_point_coordinate. ** use inr. cbn. rewrite <- (pointed_hset_struct_preserve_point _ (pr2 (enriched_from_arr E (pr2 fg)))). apply maponpaths. refine (!_). apply hset_struct_with_smash_point_unit. ** use inl. apply idpath. - intros x y z f. unfold smash_struct_enrichment_point. refine (!(enriched_to_from_arr E _) @ _ @ enriched_to_from_arr E _). apply maponpaths. rewrite enriched_from_arr_comp. use subtypePath. { intro ; cbn -[isaprop]. apply isaprop_hset_struct_on_mor. } use funextsec ; intro a. cbn. induction a ; cbn. + rewrite !enriched_from_arr_smash_lemma. pose (pointed_hset_struct_preserve_point P (pr2 (enriched_comp E x y z))) as p. refine (_ @ p). apply maponpaths. refine (_ @ !(hset_struct_with_smash_point_smash _ _ _)). use iscompsetquotpr. apply hinhpr. use inr. split ; unfold product_point_coordinate. * use inl. apply idpath. * use inl. apply idpath. + refine (!_). etrans. { apply maponpaths. exact (!(hset_struct_with_smash_point_unit (pr122 P))). } refine (pointed_hset_struct_preserve_point _ (pr2 (enriched_from_arr E _)) @ _). refine (!_). pose (pointed_hset_struct_preserve_point P (pr2 (enriched_comp E x y z))) as p. refine (_ @ p). apply maponpaths. refine (_ @ !(hset_struct_with_smash_point_smash _ _ _)). use iscompsetquotpr. apply hinhpr. use inr. split ; unfold product_point_coordinate. * use inr. cbn. rewrite <- (pointed_hset_struct_preserve_point _ (pr2 (enriched_from_arr E f))). apply maponpaths. refine (!_). apply hset_struct_with_smash_point_unit. * use inl. apply idpath. - intros x y z f. unfold smash_struct_enrichment_point. refine (!(enriched_to_from_arr E _) @ _ @ enriched_to_from_arr E _). apply maponpaths. rewrite enriched_from_arr_comp. use subtypePath. { intro ; cbn -[isaprop]. apply isaprop_hset_struct_on_mor. } use funextsec ; intro a. cbn. induction a ; cbn. + rewrite !enriched_from_arr_smash_lemma. pose (pointed_hset_struct_preserve_point P (pr2 (enriched_comp E x y z))) as p. refine (_ @ p). apply maponpaths. refine (_ @ !(hset_struct_with_smash_point_smash _ _ _)). use iscompsetquotpr. apply hinhpr. use inr. split ; unfold product_point_coordinate. * use inr. apply idpath. * use inl. apply idpath. + refine (!_). etrans. { apply maponpaths. exact (!(hset_struct_with_smash_point_unit (pr122 P))). } refine (pointed_hset_struct_preserve_point _ (pr2 (enriched_from_arr E _)) @ _). refine (!_). pose (pointed_hset_struct_preserve_point P (pr2 (enriched_comp E x y z))) as p. refine (_ @ p). apply maponpaths. refine (_ @ !(hset_struct_with_smash_point_smash _ _ _)). use iscompsetquotpr. apply hinhpr. use inr. split ; unfold product_point_coordinate. * use inr. cbn. etrans. { apply maponpaths. refine (!_). apply (hset_struct_with_smash_point_unit (pr122 P)). } exact (pointed_hset_struct_preserve_point _ (pr2 (enriched_from_arr E _))). * use inl. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits UniMath.CategoryTheory.DisplayedCats.Structures.StructuresSmashProduct UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Cartesian UniMath.CategoryTheory.Monoidal.Examples.SmashProductMonoidal UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor