Definition left_biadj_preserves_bincoprod_nat_trans_data : nat_trans_data (left_biadj_preserves_binprods_1cell x p) (universal_coprod_functor (psfunctor_bincoprod_cocone L p) x). Proof. intro f. simple refine (_ ,, _) ; cbn ; cbn in f. - refine (((psfunctor_comp L _ _)^-1 ▹ _) • rassociator _ _ _ • (_ ◃ (((psfunctor_comp L _ _)^-1 ▹ _) • rassociator _ _ _ • (_ ◃ psnaturality_of (biadj_counit R) f^-1) • lassociator _ _ _ • ((linvunitor _ • _) ▹ _) • lunitor _))). exact ((_ ◃ (_ ◃ (linvunitor _ • (_ ◃ rinvunitor _)))) • invertible_modcomponent_of (biadj_triangle_l R) p). - refine (((psfunctor_comp L _ _)^-1 ▹ _) • rassociator _ _ _ • (_ ◃ (((psfunctor_comp L _ _)^-1 ▹ _) • rassociator _ _ _ • (_ ◃ psnaturality_of (biadj_counit R) f^-1) • lassociator _ _ _ • ((linvunitor _ • _) ▹ _) • lunitor _))). exact ((_ ◃ (_ ◃ (linvunitor _ • (_ ◃ rinvunitor _)))) • invertible_modcomponent_of (biadj_triangle_l R) p). Defined.
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.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.Properties. Require Import UniMath.Bicategories.Morphisms.Properties.ClosedUnderInvertibles. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Biadjunction. Require Import UniMath.Bicategories.PseudoFunctors.Preservation.Preservation. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.Modifications.Modification. Require Import UniMath.Bicategories.Colimits.Coproducts.