proposition: Lemma Monad_laws_from_adjunction {C D : category} {L : functor C D} {R : functor D C} (H : are_adjoints L R) : disp_Monad_laws (Monad_data_from_adjunction H).
proof: Proof. cbn. use make_dirprod. + use make_dirprod. * intro c; cbn. apply triangle_id_right_ad. * intro c; cbn. rewrite <- functor_id. rewrite <- functor_comp. apply maponpaths. apply triangle_id_left_ad. + intro c; cbn. do 2 (rewrite <- functor_comp). apply maponpaths. apply (nat_trans_ax ((counit_from_are_adjoints H))). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.SIP UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.Core.Univalence