Definition functor_ass_ntrans1 (αC : associator TC) (αD : associator TD) {F : functor C D} {FF : functor_tensorunit_disp_cat TC TD IC ID F} (FF_iso : is_nat_z_iso (pr11 FF)) : nat_trans (functor_composite (pair_functor (pair_functor F F) F) (functor_composite (pair_functor TD (functor_identity _)) TD) ) (functor_composite (assoc_right TC) F). Proof. set (pF := pair_functor F F). set (pFF := pair_functor pF F). use nat_trans_comp. 2: { exact (pre_whisker pFF αD). } use assoc_right_commutes_with_triple_pairing. - exact (pr1 FF). - exact FF_iso. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored.