Definition Monad_to_Ktriple_functor {x y : univalent_category} {f : bicat_of_univ_cats ⟦ x, y ⟧} {mx : (monad bicat_of_univ_cats) x} {my : (monad bicat_of_univ_cats) y} (mf : mx -->[ f] my) : Monad_to_Ktriple_data mx -->[ f ] Monad_to_Ktriple_data my. Proof. use make_kleisli_triple_on_functor. - exact (monad_mor_natural_pointwise mf). - abstract ( refine (λ (X : x), _); simpl; pose (nat_trans_eq_pointwise (monad_mor_unit mf) X) as mf_unit; cbn in mf_unit; do 2 rewrite id_left in mf_unit; etrans; [ apply pathsinv0 | apply maponpaths_2; exact mf_unit ]; etrans; [ rewrite assoc' | apply id_right ]; apply maponpaths; exact (z_iso_inv_after_z_iso (nat_z_iso_pointwise_z_iso (invertible_2cell_to_nat_z_iso _ _ (monad_mor_natural mf)) X)) ). - abstract ( refine (λ (X Y : x) (p : x ⟦ X, pr1 (Monad_to_Ktriple_data mx) Y ⟧), _); unfold Monad_to_Ktriple_data, bind_kt; simpl; etrans; [ apply (monad_mor_bind_alt mf) | idtac ]; do 2 rewrite (inv_monad_mor_natural_pointwise mf); do 2 rewrite assoc'; 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.