Definition Monad_biequiv_Ktriple_unit : disp_pstrans (disp_pseudo_comp (id_psfunctor bicat_of_univ_cats) (id_psfunctor bicat_of_univ_cats) (monad bicat_of_univ_cats) kleisli_triple_disp_bicat (monad bicat_of_univ_cats) Monad_to_Ktriple Ktriple_to_Monad) (disp_pseudo_id (monad bicat_of_univ_cats)) (lunitor_pstrans (id_psfunctor bicat_of_univ_cats)). Proof. use make_disp_pstrans. - exact (disp_2cells_isaprop_monad bicat_of_univ_cats univalent_cat_is_univalent_2). - exact (disp_locally_groupoid_monad bicat_of_univ_cats univalent_cat_is_univalent_2). - intros. use make_cat_monad_mor. + simpl. cbn. use make_nat_z_iso. * use make_nat_trans. ** intro z. apply identity. ** abstract (intros z t f ; cbn; rewrite id_left, id_right; unfold monad_bind; rewrite (functor_comp (monad_endo xx : _ ⟶ _)); rewrite assoc'; etrans; [ apply maponpaths; apply (cat_monad_ημ xx) | apply id_right ]). * intros z. apply identity_is_z_iso. + intros z. apply id_right. + abstract ( simpl; intros X; rewrite id_left; apply id_right). - abstract ( intros; use make_cat_monad_cell; simpl; intros X; rewrite !(functor_id ((monad_endo yy) : _ ⟶ _)); rewrite (functor_id f); rewrite !id_left; rewrite !(functor_id ((monad_endo yy) : _ ⟶ _)); rewrite !id_right; apply pathsinv0; apply inv_z_iso_unique'; unfold precomp_with; simpl; exact (z_iso_after_z_iso_inv (nat_z_iso_pointwise_z_iso (invertible_2cell_to_nat_z_iso _ _ (monad_mor_natural ff)) X)) ). Defined.
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.