Lemma RelMonad_composition_laws {C : precategory_data} {D : precategory} {J : functor_data C D} {R R' R'' : RelMonad_data J} (α : RelMonadMor R R') (α' : RelMonadMor R' R''): RelMonadMor_axioms (λ a : C, (α : RelMonadMor_data R R') a · (α' : RelMonadMor_data R' R'') a). Proof. split; intros; simpl. - rewrite assoc. rewrite (r_eta_α α). apply (r_eta_α α'). - intermediate_path ((α:RelMonadMor_data R R') a · ((α':RelMonadMor_data R' R'') a · r_bind R'' ((f · (α:RelMonadMor_data R R') b) · (α':RelMonadMor_data R' R'') b))). * now repeat rewrite assoc. * rewrite (α_r_bind α'). rewrite assoc. rewrite (α_r_bind α). apply pathsinv0. apply assoc. 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.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core.