Lemma inv_monad_mor_natural_pointwise {C₁ C₂ : univalent_category} {F : C₁ ⟶ C₂} {M₁ : monad bicat_of_univ_cats C₁} {M₂ : monad bicat_of_univ_cats C₂} (FF : M₁ -->[F] M₂) (X : C₁) : inv_from_z_iso (monad_mor_natural_pointwise FF X) = CompositesAndInverses.nat_z_iso_to_pointwise_z_iso (monad_mor_nat_z_iso FF) X. Proof. refine (!_). apply inv_z_iso_unique'. unfold precomp_with. cbn. apply (nat_trans_eq_pointwise (vcomp_linv (monad_mor_natural FF)) X). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Projection. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.Transformations.Examples.AlgebraMap. Require Import UniMath.Bicategories.Modifications.Modification. Require Import UniMath.Bicategories.PseudoFunctors.Biequivalence. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.DisplayedBicats.DispPseudofunctor. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Algebras. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Add2Cell. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod. Require Import UniMath.Bicategories.DisplayedBicats.Examples.FullSub. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Monads. Require Import UniMath.Bicategories.DisplayedBicats.Examples.KleisliTriple. Require Import UniMath.Bicategories.DisplayedBicats.DispBuilders. Require Import UniMath.Bicategories.DisplayedBicats.DispTransformation. Require Import UniMath.Bicategories.DisplayedBicats.DispModification. Require Import UniMath.Bicategories.DisplayedBicats.DispBiequivalence. Require Import UniMath.Bicategories.Transformations.Examples.Unitality. Require Import UniMath.Bicategories.DisplayedBicats.Examples.KleisliTriple. Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses.