Lemma RelMonadMor_composed_radj_axioms : RelMonadMor_axioms RelMonadMor_composed_radj_data. Proof. repeat split; cbn; intros. - unfold RelMonadMor_composed_radj_data. cbn. etrans. apply pathsinv0, φ_adj_natural_postcomp . apply maponpaths. apply (r_eta_α f). - unfold RelMonadMor_composed_radj_data. cbn. etrans. apply (!functor_comp _ _ _ ). etrans. 2: { apply functor_comp. } apply maponpaths. etrans. apply maponpaths. apply maponpaths. apply (φ_adj_inv_natural_postcomp R). apply (α_r_bind f). 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.