proposition: Lemma RelMonadMor_composed_radj_axioms : RelMonadMor_axioms RelMonadMor_composed_radj_data.
proof: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Monads.RelativeMonads