Lemma forgetRelMonad_faithful {C : precategory} (D : category) (J : functor C D) : faithful (forgetfunctor_RelMonad D J). Proof. intros R R'. simpl. apply isinclbetweensets. - apply isaset_total2. + apply impred_isaset. intros. apply D. + intros. apply isasetaprop. apply isaprop_RelMonadMor_axioms. apply D. - apply isaset_nat_trans. apply D. - intros α α' p. apply RelMonadMor_equiv. + apply D. + apply funextsec. intro c. change (nat_trans_RelMonadMor α c = nat_trans_RelMonadMor α' c). rewrite p. 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.