Definition RelMonad_composed_radj_axioms : RelMonad_axioms RelMonad_composed_radj_data. Proof. repeat split; intros; cbn. - etrans. do 2 apply maponpaths. apply φ_adj_inv_after_φ_adj. etrans. apply maponpaths. apply r_bind_r_eta. apply TH. apply functor_id. - etrans. apply pathsinv0. apply φ_adj_natural_postcomp. etrans. apply maponpaths. apply (r_eta_r_bind TH). apply φ_adj_after_φ_adj_inv. - etrans. apply (!functor_comp _ _ _ ). apply maponpaths. etrans. apply (r_bind_r_bind TH). apply maponpaths. apply pathsinv0. apply (φ_adj_inv_natural_postcomp R). Defined.
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.