Definition Pcomp_strong_preserving : ∏ (C D E : UMONCAT) (F : UMONCAT⟦C,D⟧) (G : UMONCAT⟦D,E⟧), P_strong_preserving _ _ F → P_strong_preserving _ _ G -> P_strong_preserving _ _ (F·G). Proof. intros C D E F G sF sG. use tpair. - apply is_z_isomorphism_comp. + apply sG. + apply functor_on_is_z_isomorphism. apply sF. - intro ; intro. apply is_z_isomorphism_comp. + apply sG. + simpl. apply functor_on_is_z_isomorphism. apply sF. Defined.
Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.TensorLayer. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.UnitLayer. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.TensorUnitLayer. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.AssociatorUnitorsLayer. Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. 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.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod. Require Import UniMath.Bicategories.DisplayedBicats.Examples.FullSub. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sigma. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell. Require Import UniMath.Bicategories.Core.Univalence. Import Bicat.Notations. Import AssociatorUnitorsNotations. Import UMONCAT_Notations. Import Bicat.Notations.