Definition Monad_bequiv_Ktriple_counit : disp_pstrans (disp_pseudo_comp (id_psfunctor bicat_of_univ_cats) (id_psfunctor bicat_of_univ_cats) kleisli_triple_disp_bicat (monad bicat_of_univ_cats) kleisli_triple_disp_bicat Ktriple_to_Monad Monad_to_Ktriple) (disp_pseudo_id kleisli_triple_disp_bicat) (lunitor_pstrans (id_psfunctor bicat_of_univ_cats)). Proof. use make_disp_pstrans. - exact disp_2cells_isaprop_kleisli. - exact disp_locally_groupoid_kleisli. - refine (λ (x : univalent_category) (kx : kleisli_triple x), _). use make_kleisli_triple_on_functor. + exact (λ X, identity_z_iso (kx X)). + abstract ( refine (λ A : x, _); apply pathsinv0; apply id_right). + abstract ( refine (λ (A B : pr1 x) (f : pr1 x ⟦ A, pr1 kx B ⟧), _); simpl; rewrite id_right; etrans; [ apply bind_kt_monad_to_kleisli | idtac ]; etrans; [ pose (kleisli_triple_on_functor_bind_kt (kleisli_triple_on_identity_functor kx) _ _ f ) as H; simpl in H; exact H | idtac ]; apply id_right ). - abstract ( refine (λ (x y : univalent_category) (f : pr1 x ⟶ pr1 y) (kx : kleisli_triple x) (ky : kleisli_triple y) (kf : kleisli_triple_on_functor kx ky f) (X : x), _); simpl; apply pathsinv0; etrans; [ apply maponpaths_2; do 2 rewrite id_left; apply (bind_unit ky) | idtac ]; etrans; [ apply id_left | idtac]; etrans; [ apply id_left | idtac]; apply pathsinv0; simpl; etrans; [ rewrite assoc'; apply maponpaths; rewrite functor_id; etrans; [ apply id_left | idtac]; apply id_left | idtac ]; etrans; [ apply id_right | idtac]; apply idpath ). 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.