proposition: Lemma RelMonadMor_composed_axioms : RelMonadMor_axioms RelMonadMor_composed_data.
proof: 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.
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