Definition r_lift_r_bind {C: precategory_data} {D: precategory} {J : functor C D}(R : RelMonad)(a b c : C) (f : b --> c) (g : J a --> R b) : r_bind R g · r_lift R f = r_bind R (g · r_lift R f). Proof. unfold r_lift. rewrite <- (r_bind_r_bind R). apply idpath. 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.