Lemma RelMonadMor_composed_axioms : RelMonadMor_axioms RelMonadMor_composed_data. Proof. repeat split; cbn; intros. - unfold RelMonadMor_composed_data. cbn. etrans. apply (!functor_comp _ _ _ ). apply maponpaths. apply r_eta_α. apply f. - unfold RelMonadMor_composed_data. cbn. etrans. apply pathsinv0. apply (inv_natural_precomp NHW). cbn. rewrite assoc. etrans. apply (inv_natural_precomp NHW). cbn. etrans. apply maponpaths. apply φ_adj_inv_unit. rewrite id_right. rewrite functor_comp. apply pathsinv0. etrans. apply maponpaths_2. apply (inv_natural_precomp NHW). cbn. etrans. apply maponpaths_2. apply maponpaths. apply φ_adj_inv_unit. rewrite id_right. etrans. apply (!functor_comp _ _ _ ). etrans. apply maponpaths. apply (!(α_r_bind f) _ _ _ ). cbn. apply pathsinv0. etrans. apply (!functor_comp _ _ _ ). apply maponpaths. apply maponpaths. apply maponpaths. etrans. apply maponpaths_2. apply φ_adj_natural_postcomp. etrans. apply (!assoc _ _ _ ). etrans. apply maponpaths. apply ηinv_is_natural. apply assoc. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Monads.RelativeMonads.