proposition: Proposition copow_adjunction_laws : form_adjunction' copow_adjunction_data.
proof: Proof. split. - intro v ; cbn. use arr_to_copower_eq. { exact (pr2 (copowC _ r)). } rewrite enriched_from_arr_id. etrans. { apply maponpaths_2. apply maponpaths. apply arr_to_copower_precomp. } etrans. { apply arr_to_copower_commutes. } use internal_funext. intros a h. rewrite !tensor_comp_r_id_r. rewrite !assoc'. unfold is_copower_enriched_map, internal_postcomp. rewrite !internal_beta. rewrite tensor_split. refine (!_). rewrite tensor_split. rewrite !assoc'. apply maponpaths. clear a h. refine (!_). rewrite !assoc. rewrite internal_beta. rewrite <- tensor_split'. refine (!_). rewrite tensor_split. rewrite !assoc'. rewrite <- enrichment_id_left. rewrite tensor_lunitor. apply maponpaths. refine (!(id_right _) @ _). apply maponpaths. refine (!_). unfold postcomp_arr. rewrite !assoc. rewrite tensor_linvunitor. refine (_ @ mon_linvunitor_lunitor _). rewrite !assoc'. apply maponpaths. refine (_ @ copow_on_enriched_mor_commute copowC _ _). rewrite !tensor_comp_r_id_r. rewrite !assoc'. unfold is_copower_enriched_map. rewrite internal_beta. rewrite !assoc. apply maponpaths_2. rewrite <- tensor_split. rewrite <- tensor_split'. apply idpath. - intro x ; cbn. unfold postcomp_arr. rewrite !assoc. rewrite tensor_linvunitor. rewrite !assoc'. refine (_ @ mon_linvunitor_lunitor _). apply maponpaths. rewrite !assoc. rewrite <- tensor_split. refine (_ @ copow_on_enriched_mor_commute copowC r x). rewrite !tensor_comp_r_id_r. rewrite !assoc'. unfold is_copower_enriched_map. rewrite internal_beta. rewrite !assoc. rewrite <- tensor_split'. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.OppositeCategory.Core UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Structure.Cartesian UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.Structure.Closed UniMath.CategoryTheory.Monoidal.Examples.CartesianMonoidal UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation UniMath.CategoryTheory.EnrichedCats.EnrichmentAdjunction UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedTerminal UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedBinaryProducts UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedPowers UniMath.CategoryTheory.EnrichedCats.Limits.Examples.SelfEnrichedLimits UniMath.CategoryTheory.EnrichedCats.Limits.Examples.OppositeEnrichedLimits UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedInitial UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedBinaryCoproducts UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCopowers UniMath.CategoryTheory.EnrichedCats.Colimits.CopowerFunctor UniMath.CategoryTheory.EnrichedCats.Colimits.Examples.SelfEnrichedColimits UniMath.CategoryTheory.EnrichedCats.Colimits.Examples.OppositeEnrichedColimits UniMath.Semantics.EnrichedEffectCalculus.EECModel