Definition smf_from_param_distr: parameterized_distributivity Mon_V A A' FA FA' G -> strong_monoidal_functor Mon_V montrafotarget_moncat. Proof. intro δs. induction δs as [δ [δtr_eq δpe_eq]]. use smf_from_param_distr_bicat_parts. - exact (parameterized_distributivity_nat_as_instance δ). - apply param_distr_triangle_eq_variant0_follows in δtr_eq. red in δtr_eq |- *. unfold param_distr_triangle_eq_variant0_RHS in δtr_eq. unfold param_distr_bicat_triangle_eq_variant0_RHS. cbn in δtr_eq |- *. unfold pre_whisker_in_funcat, post_whisker_in_funcat in δtr_eq. etrans. { exact δtr_eq. } apply maponpaths. rewrite (nat_trans_comp_id_right A' (functor_composite G (functor_identity A')) G). show_id_type. apply (nat_trans_eq A'). intro a. cbn. apply pathsinv0, id_left. - intros v w. set (δpe_eq_inst := δpe_eq v w). apply param_distr_pentagon_eq_body_variant_follows in δpe_eq_inst. unfold param_distr_bicat_pentagon_eq_body_variant_RHS, param_distr_bicat_pentagon_eq_body_RHS. unfold param_distr_pentagon_eq_body_variant, param_distr_pentagon_eq_body_variant_RHS in δpe_eq_inst. cbn in δpe_eq_inst |- *. etrans. { exact δpe_eq_inst. } clear δpe_eq_inst. apply maponpaths. apply (nat_trans_eq A'). intro a. cbn. do 3 rewrite id_left. apply idpath. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.DisplayedMonoidalTensored. Require Import UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal. Require Import UniMath.Bicategories.MonoidalCategories.Actions. Require Import UniMath.Bicategories.MonoidalCategories.ActionBasedStrength. Require Import UniMath.Bicategories.MonoidalCategories.MonoidalFromBicategory. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.BicatOfCats. Import Bicat.Notations.