Definition enriched_functor_from_univalent_kleisli_cat_nat_trans_is_z_iso : is_nat_z_iso (pr11 enriched_functor_from_univalent_kleisli_cat_nat_trans). Proof. use is_nat_z_iso_comp. - use is_nat_z_iso_comp. + use is_nat_z_iso_comp. * use post_whisker_z_iso_is_z_iso. exact (pr2 (functor_to_kleisli_cat_incl_nat_z_iso M)). * apply is_nat_z_iso_nat_trans_id. + use pre_whisker_on_nat_z_iso. apply is_nat_z_iso_enriched_functor_category_z_iso. - 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.Prelude. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Categories.EilenbergMoore. Require Import UniMath.CategoryTheory.Categories.KleisliCategory. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentMonad. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.KleisliEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.UnivalentKleisliEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.FunctorCategory. Require Import UniMath.CategoryTheory.EnrichedCats.RezkCompletion.RezkUniversalProperty. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Monads.KleisliCategory. Require Import UniMath.CategoryTheory.Limits.Equalizers. Section FunctorFromUnivalentKleisli. End FunctorFromUnivalentKleisli. Section NatTransFromUnivalentKleisli. End NatTransFromUnivalentKleisli.