Definition functor_from_univalent_kleisli_cat_nat_trans_is_z_iso : is_nat_z_iso functor_from_univalent_kleisli_cat_nat_trans. Proof. unfold functor_from_univalent_kleisli_cat_nat_trans. use (@is_nat_z_iso_comp _ _ _ _ _ _ (functor_from_kleisli_cat_monad_nat_trans m F γ p₁ p₂)). - use (@is_nat_z_iso_comp _ _ _ (Left_Kleisli_functor m ∙ functor_to_kleisli_cat m ∙ functor_from_univalent_kleisli_cat)). + use post_whisker_z_iso_is_z_iso. apply (functor_to_kleisli_cat_incl_nat_z_iso m). + use (pre_whisker_on_nat_z_iso (Left_Kleisli_functor m) (lift_functor_along_comm C₂ (functor_to_kleisli_cat m) (essentially_surjective_functor_to_kleisli_cat m) (fully_faithful_functor_to_kleisli_cat m) (functor_from_kleisli_cat_monad m F γ p₁ p₂))). apply (lift_functor_along_comm C₂ (functor_to_kleisli_cat m) (essentially_surjective_functor_to_kleisli_cat m) (fully_faithful_functor_to_kleisli_cat m) (functor_from_kleisli_cat_monad m F γ p₁ p₂)). - apply functor_from_kleisli_cat_monad_nat_trans_is_z_iso. Defined.
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.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.EilenbergMoore. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.Subcategory.Full. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Monads.KleisliCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.PrecompEquivalence.