Proposition strength_to_enrichment_laws : @is_functor_enrichment _ _ _ F self_enrichment self_enrichment (λ x y, internal_lam (tF (internal_hom x y) x · # F (internal_eval x y))). Proof. repeat split. - intros x ; cbn. use internal_funext. intros w h. refine (!_). etrans. { rewrite tensor_split. rewrite !assoc'. unfold internal_id. rewrite internal_beta. rewrite tensor_lunitor. apply idpath. } refine (!_). rewrite tensor_split. rewrite tensor_comp_id_r. rewrite !assoc'. rewrite internal_beta. etrans. { apply maponpaths. rewrite !assoc. rewrite <- functor_id. rewrite (left_strength_natural tF). rewrite !assoc'. rewrite <- functor_comp. unfold internal_id. rewrite internal_beta. rewrite left_strength_mon_lunitor. apply idpath. } rewrite tensor_lunitor. apply idpath. - intros x y z ; cbn. use internal_funext. intros w h. etrans. { rewrite tensor_comp_r_id_r. rewrite !assoc'. rewrite internal_beta. apply idpath. } etrans. { rewrite !assoc. etrans. { apply maponpaths_2. rewrite tensor_split. rewrite <- functor_id. rewrite !assoc'. rewrite left_strength_natural. apply idpath. } rewrite !assoc'. rewrite <- !functor_comp. unfold internal_comp. rewrite internal_beta. apply idpath. } refine (!_). etrans. { rewrite tensor_comp_r_id_r. rewrite !assoc'. unfold internal_comp. rewrite internal_beta. rewrite !assoc. rewrite tensor_lassociator. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_comp_mor. rewrite id_right. rewrite tensor_split. rewrite !assoc'. rewrite internal_beta. apply maponpaths_2. apply maponpaths. rewrite tensor_split. rewrite !assoc'. rewrite internal_beta. apply idpath. } rewrite !tensor_comp_id_l. rewrite !assoc. rewrite <- tensor_lassociator. rewrite tensor_id_id. rewrite !assoc'. etrans. { apply maponpaths. etrans. { do 2 apply maponpaths. rewrite !assoc. rewrite left_strength_natural. apply idpath. } rewrite !assoc. rewrite <- left_strength_mon_lassociator. apply idpath. } rewrite !assoc'. rewrite <- !functor_comp. apply idpath. - intros x y f ; cbn. use internal_funext. intros w h. rewrite tensor_comp_r_id_r. rewrite !assoc'. rewrite internal_beta. refine (!_). etrans. { rewrite tensor_split. rewrite <- functor_id. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite left_strength_natural. rewrite !assoc'. rewrite <- functor_comp. unfold internal_from_arr. rewrite internal_beta. rewrite functor_comp. rewrite !assoc. rewrite left_strength_mon_lunitor. apply idpath. } rewrite !assoc. rewrite tensor_lunitor. refine (!_). etrans. { rewrite tensor_split. rewrite !assoc'. unfold internal_from_arr. rewrite internal_beta. rewrite !assoc. rewrite tensor_lunitor. apply idpath. } 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.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentMonad. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.StrongMonad. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Import MonoidalNotations.