Proposition make_smash_struct_enrichment_laws : smash_struct_enrichment_laws make_smash_struct_enrichment_data. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructuresSmashProduct. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Cartesian. Require Import UniMath.CategoryTheory.Monoidal.Examples.SmashProductMonoidal. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Section FromStructSmashEnrichment. End FromStructSmashEnrichment.