Definition nat_trans_from_kleisli_cat_monad_unique {β₁ β₂ : G₁ ⟹ G₂} (q₁ : pre_whisker _ β₁ = α) (q₂ : pre_whisker _ β₂ = α) : β₁ = β₂.
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.Adjunctions.Core. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.whiskering.