Library UniMath.Bicategories.Morphisms.Monadic

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.categories.EilenbergMoore.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful.
Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses.
Require Import UniMath.CategoryTheory.Monads.Monads.
Require Import UniMath.Bicategories.Core.Bicat.
Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.BicategoryLaws.
Require Import UniMath.Bicategories.Core.Unitors.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.Core.AdjointUnique.
Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats.
Require Import UniMath.Bicategories.Morphisms.Adjunctions.
Require Import UniMath.Bicategories.Morphisms.Properties.AdjunctionsRepresentable.
Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat.
Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor.
Require Import UniMath.Bicategories.PseudoFunctors.Examples.MonadInclusion.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax.
Require Import UniMath.Bicategories.Monads.Examples.AdjunctionToMonad.
Require Import UniMath.Bicategories.Monads.Examples.ToMonadInCat.
Require Import UniMath.Bicategories.Monads.Examples.MonadsInBicatOfUnivCats.
Require Import UniMath.Bicategories.Limits.EilenbergMooreObjects.
Require Import UniMath.Bicategories.Limits.Examples.BicatOfUnivCatsLimits.

Local Open Scope cat.

Section Monadic.
  Context {B : bicat}
          (HB : bicat_has_em B)
          {x y : B}
          (l : adjunction x y).

  Let r : y --> x := left_adjoint_right_adjoint l.
  Let η : id₁ _ ==> l · r := left_adjoint_unit l.
  Let ε : r · l ==> id₁ _ := left_adjoint_counit l.

  Let m : mnd B := mnd_from_adjunction l.

  Let e : em_cone m := pr1 (HB m).
  Let He : has_em_ump _ e := pr2 (HB m).

1. Comparison cell
  Local Definition comparison_mor_cone_mult
    : lassociator r (l · r) (l · r)
      • (lassociator r l r ▹ l · r)
      • ((ε ▹ r) ▹ l · r)
      • (lunitor r ▹ l · r)
      • lassociator r l r
      • (ε ▹ r)
      =
      (r ◃ rassociator l r (l · r))
      • (r ◃ (l ◃ lassociator r l r))
      • (r ◃ (l ◃ (ε ▹ r)))
      • (r ◃ (l ◃ lunitor r))
      • lassociator r l r
      • (ε ▹ r).
  Show proof.
    refine (!_).
    etrans.
    {
      rewrite !vassocl.
      apply maponpaths.
      rewrite !vassocr.
      rewrite !lwhisker_vcomp.
      rewrite lwhisker_lwhisker.
      rewrite !vassocl.
      rewrite <- vcomp_whisker.
      apply idpath.
    }
    rewrite !vassocl.
    use vcomp_move_R_pM ; [ is_iso | ] ; cbn.
    rewrite !vassocr.
    rewrite lassociator_lassociator.
    rewrite !vassocl.
    apply maponpaths.
    rewrite !vassocr.
    rewrite rwhisker_rwhisker.
    rewrite !vassocl.
    apply maponpaths.
    rewrite !vassocr.
    rewrite lunitor_triangle.
    rewrite !vassocl.
    use vcomp_move_L_pM ; [ is_iso | ].
    cbn.
    rewrite !vassocr.
    rewrite lwhisker_hcomp.
    rewrite <- linvunitor_natural.
    rewrite !vassocl.
    rewrite lunitor_linvunitor.
    rewrite id2_right.
    apply idpath.

  Definition comparison_mor_cone
    : em_cone m.
  Show proof.
    use make_em_cone.
    - exact y.
    - exact r.
    - exact (lassociator _ _ _ • (ε ▹ r)).
    - abstract
        (refine (!(id2_left _) @ _) ;
         use vcomp_move_R_Mp ; [ is_iso | ] ;
         cbn ;
         rewrite !vassocr ;
         exact (!(internal_triangle2 l))).
    - abstract
        (cbn ;
         rewrite <- !rwhisker_vcomp, <- !lwhisker_vcomp ;
         rewrite !vassocr ;
         exact comparison_mor_cone_mult).

  Definition comparison_mor
    : y --> e
    := em_ump_1_mor _ He comparison_mor_cone.

  Definition comparison_mor_cell
    : em_ump_1_mor m He comparison_mor_cone · mor_of_mnd_mor (mor_of_em_cone m e)
      ==>
      r
    := cell_of_mnd_cell (em_ump_1_inv2cell _ He comparison_mor_cone).

  Definition comparison_mor_inv2cell
    : invertible_2cell
        (em_ump_1_mor m He comparison_mor_cone · mor_of_mnd_mor (mor_of_em_cone m e))
        r.
  Show proof.
    use make_invertible_2cell.
    - exact comparison_mor_cell.
    - exact (from_invertible_mnd_2cell
               (em_ump_1_inv2cell _ He comparison_mor_cone)).

  Definition comparison_mor_eq_help
    : rassociator _ _ _
      • (_ ◃ mnd_mor_endo (mor_of_em_cone m e))
      • lassociator _ _ _
      • (runitor _ • linvunitor _ ▹ _)
      • rassociator _ _ _
      • (_ ◃ comparison_mor_cell)
      =
      (comparison_mor_cell ▹ _)
      • lassociator r l r
      • (ε ▹ r).
  Show proof.
    pose (mnd_cell_endo (em_ump_1_inv2cell _ He comparison_mor_cone)).
    rewrite !vassocl.
    refine (_ @ p).
    do 4 refine (_ @ vassocr _ _ _).
    apply idpath.

  Definition comparison_mor_eq
    : (_ ◃ mnd_mor_endo (mor_of_em_cone m e))
      • (_ ◃ lunitor _)
      • comparison_mor_cell
      =
      lassociator _ _ _
      • lassociator _ _ _
      • ((comparison_mor_cell ▹ l) ▹ r)
      • (ε ▹ r)
      • lunitor r.
  Show proof.
    use vcomp_move_L_Mp ; [ is_iso | ].
    rewrite !vassocl.
    use vcomp_move_L_pM ; [ is_iso | ].
    cbn.
    rewrite !vassocr.
    rewrite rwhisker_rwhisker.
    refine (_ @ comparison_mor_eq_help).
    rewrite !vassocl.
    do 2 apply maponpaths.
    rewrite <- !rwhisker_vcomp.
    rewrite !vassocr.
    refine (!_).
    etrans.
    {
      do 3 apply maponpaths_2.
      apply runitor_rwhisker.
    }
    rewrite !vassocl.
    apply maponpaths.
    rewrite linvunitor_natural.
    rewrite <- lwhisker_hcomp.
    rewrite !vassocr.
    apply maponpaths_2.
    refine (!_).
    apply linvunitor_assoc.

2. Monadic adjunctions
  Definition is_monadic
    : UU
    := left_adjoint_equivalence comparison_mor.

  Definition isaprop_is_monadic
             (HB_2_1 : is_univalent_2_1 B)
    : isaprop is_monadic.
  Show proof.
    apply isaprop_left_adjoint_equivalence.
    exact HB_2_1.
End Monadic.

3. Representable definition of monadic 1-cells
Definition is_monadic_repr
           {B : bicat}
           (HB_2_1 : is_univalent_2_1 B)
           {x y : B}
           (l : adjunction x y)
  : UU
  := ∏ (w : B),
     is_monadic
       has_em_bicat_of_univ_cats
       (left_adjoint_to_adjunction_cat _ l w HB_2_1).

Definition isaprop_is_monadic_repr
           {B : bicat}
           (HB_2_1 : is_univalent_2_1 B)
           {x y : B}
           (l : adjunction x y)
  : isaprop (is_monadic_repr HB_2_1 l).
Show proof.
  use impred ; intro.
  apply isaprop_is_monadic.
  exact univalent_cat_is_univalent_2_1.

Section MonadicReprWeqMonadic.
  Context {B : bicat}
          (HB_2_1 : is_univalent_2_1 B)
          (HB : bicat_has_em B)
          {x y : B}
          (l : adjunction x y).

  Section DiagramOfMonadicRepr.
    Context (w : B).

    Let M : Monad (hom w x)
      := mnd_bicat_of_univ_cats_to_Monad
           (mnd_from_adjunction
              (left_adjoint_to_adjunction_cat l l w HB_2_1)).

    Let M' : Monad (hom w x)
      := mnd_to_cat_Monad (mnd_from_adjunction l) w.

    Let F : hom w y
            ⟶
            eilenberg_moore_cat _
      := comparison_mor
           has_em_bicat_of_univ_cats
           (left_adjoint_to_adjunction_cat l l w HB_2_1).

    Let G : hom w y ⟶ hom w (pr1 (HB (mnd_from_adjunction l)))
      := post_comp w (comparison_mor HB l).

    Let H : hom w (pr1 (HB (mnd_from_adjunction l)))
            ⟶
            eilenberg_moore_cat M'
      := is_em_universal_em_cone_functor _ (pr1 (HB (mnd_from_adjunction l))) w.

    Definition is_monadic_connecting_functor_ob
               (z : eilenberg_moore_cat M')
      : eilenberg_moore_cat M.
    Show proof.
      use make_ob_eilenberg_moore.
      - exact (ob_of_eilenberg_moore_ob z).
      - cbn.
        exact (rassociator _ _ _ • mor_of_eilenberg_moore_ob z).
      - abstract
          (refine (_ @ eilenberg_moore_ob_unit z) ; cbn ;
           rewrite !vassocl ;
           do 2 apply maponpaths ;
           rewrite !vassocr ;
           rewrite lassociator_rassociator ;
           apply id2_left).
      - abstract
          (cbn ;
           rewrite !id2_left, id2_right ;
           rewrite !vassocr ;
           rewrite rwhisker_rwhisker_alt ;
           rewrite <- !rwhisker_vcomp ;
           rewrite !vassocl ;
           pose (eilenberg_moore_ob_mult z) as p ;
           cbn in p ;
           rewrite <- p ; clear p ;
           rewrite !vassocr ;
           apply maponpaths_2 ;
           rewrite <- !lwhisker_vcomp ;
           rewrite !vassocl ;
           rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ;
           rewrite rassociator_rassociator ;
           rewrite !vassocl ;
           rewrite !lwhisker_vcomp ;
           rewrite lwhisker_lwhisker_rassociator ;
           rewrite !vassocr ;
           apply maponpaths_2 ;
           rewrite <- rassociator_rassociator ;
           rewrite !vassocl ;
           apply maponpaths ;
           rewrite !lwhisker_vcomp ;
           rewrite !vassocr ;
           rewrite rassociator_lassociator ;
           rewrite id2_left ;
           rewrite <- !lwhisker_vcomp ;
           rewrite !vassocr ;
           rewrite rwhisker_lwhisker_rassociator ;
           rewrite !vassocl ;
           apply maponpaths ;
           rewrite lunitor_lwhisker ;
           apply idpath).

    Definition is_monadic_connecting_functor_mor
               {z₁ z₂ : eilenberg_moore_cat M'}
               (f : z₁ --> z₂)
      : is_monadic_connecting_functor_ob z₁ --> is_monadic_connecting_functor_ob z₂.
    Show proof.
      use make_mor_eilenberg_moore.
      - exact (mor_of_eilenberg_moore_mor f).
      - abstract
          (cbn ;
           rewrite !vassocr ;
           rewrite rwhisker_rwhisker_alt ;
           rewrite !vassocl ;
           apply maponpaths ;
           exact (eq_of_eilenberg_moore_mor f)).

    Definition is_monadic_connecting_functor_data
      : functor_data (eilenberg_moore_cat M') (eilenberg_moore_cat M).
    Show proof.
      use make_functor_data.
      - exact is_monadic_connecting_functor_ob.
      - exact @is_monadic_connecting_functor_mor.

    Definition is_monadic_connecting_is_functor
      : is_functor is_monadic_connecting_functor_data.
    Show proof.
      split.
      - intro z.
        use eq_mor_eilenberg_moore ; cbn.
        apply idpath.
      - intros z₁ z₂ z₃ f g.
        use eq_mor_eilenberg_moore ; cbn.
        apply idpath.

    Definition is_monadic_connecting_functor
      : eilenberg_moore_cat M' ⟶ eilenberg_moore_cat M.
    Show proof.
      use make_functor.
      - exact is_monadic_connecting_functor_data.
      - exact is_monadic_connecting_is_functor.

    Section IsMonadicEso.
      Context (z : eilenberg_moore_cat M).

      Definition is_monadic_connecting_functor_fiber
        : eilenberg_moore_cat M'.
      Show proof.
        use make_ob_eilenberg_moore.
        - exact (ob_of_eilenberg_moore_ob z).
        - cbn.
          exact (lassociator _ _ _ • mor_of_eilenberg_moore_ob z).
        - abstract
            (refine (_ @ eilenberg_moore_ob_unit z) ; cbn ;
             rewrite !vassocl ;
             apply idpath).
        - abstract
            (cbn ;
             rewrite <- !rwhisker_vcomp ;
             rewrite !vassocl ;
             rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ;
             rewrite <- rwhisker_rwhisker ;
             rewrite !vassocl ;
             pose (eilenberg_moore_ob_mult z) as p ;
             cbn in p ;
             rewrite !id2_left, !id2_right in p ;
             rewrite <- p ;
             rewrite !vassocr ;
             apply maponpaths_2 ;
             rewrite !vassocl ;
             use vcomp_move_L_pM ; [ is_iso | ] ; cbn ;
             rewrite <- !lwhisker_vcomp ;
             rewrite !vassocr ;
             rewrite rassociator_rassociator ;
             rewrite !vassocl ;
             rewrite !(maponpaths (λ z, _ • (_ • z)) (vassocr _ _ _)) ;
             rewrite !lwhisker_vcomp ;
             rewrite !vassocl ;
             rewrite !(maponpaths (λ z, _ • z) (vassocr _ _ _)) ;
             rewrite lwhisker_lwhisker_rassociator ;
             rewrite !vassocl ;
             rewrite rassociator_lassociator ;
             rewrite id2_right ;
             use vcomp_move_L_pM ; [ is_iso | ] ; cbn ;
             rewrite !vassocr ;
             rewrite <- rassociator_rassociator ;
             rewrite !vassocl ;
             rewrite lwhisker_vcomp ;
             rewrite !vassocr ;
             rewrite rassociator_lassociator ;
             rewrite id2_left ;
             rewrite <- !rwhisker_vcomp ;
             rewrite !vassocl ;
             apply maponpaths ;
             rewrite <- !lwhisker_vcomp ;
             rewrite !vassocr ;
             rewrite rwhisker_lwhisker_rassociator ;
             rewrite !vassocl ;
             apply maponpaths ;
             rewrite lunitor_lwhisker ;
             apply idpath).

      Definition is_monadic_connecting_functor_fiber_mor
        : is_monadic_connecting_functor_ob is_monadic_connecting_functor_fiber
          -->
          z.
      Show proof.
        use make_mor_eilenberg_moore.
        - apply identity.
        - abstract
            (cbn ;
             rewrite !vassocr ;
             rewrite rassociator_lassociator ;
             rewrite !id2_rwhisker ;
             rewrite !id2_left, id2_right ;
             apply idpath).

      Definition is_monadic_connecting_functor_z_iso
        : z_iso
            (is_monadic_connecting_functor_ob is_monadic_connecting_functor_fiber)
            z.
      Show proof.
        refine (is_monadic_connecting_functor_fiber_mor ,, _).
        use is_z_iso_eilenberg_moore.
        apply is_z_isomorphism_identity.
    End IsMonadicEso.

    Definition is_monadic_connecting_functor_is_eso
      : Functors.essentially_surjective is_monadic_connecting_functor.
    Show proof.
      intros z.
      apply hinhpr.
      simple refine (_ ,, _).
      - exact (is_monadic_connecting_functor_fiber z).
      - exact (is_monadic_connecting_functor_z_iso z).

    Section IsMonadicFull.
      Context {z₁ z₂ : eilenberg_moore_cat M'}
              (f : is_monadic_connecting_functor z₁
                   -->
                   is_monadic_connecting_functor z₂).

      Definition is_monadic_connecting_functor_fiber_of_mor
        : z₁ --> z₂.
      Show proof.
        use make_mor_eilenberg_moore.
        - exact (mor_of_eilenberg_moore_mor f).
        - abstract
            (cbn ;
             use (vcomp_lcancel (rassociator _ _ _)) ; [ is_iso | ] ;
             rewrite !vassocr ;
             refine (eq_of_eilenberg_moore_mor f @ _) ;
             cbn ;
             rewrite <- rwhisker_rwhisker_alt ;
             rewrite !vassocl ;
             apply idpath).
    End IsMonadicFull.

    Definition is_monadic_connecting_functor_is_full
      : full is_monadic_connecting_functor.
    Show proof.
      intros z₁ z₂ f.
      apply hinhpr.
      refine (is_monadic_connecting_functor_fiber_of_mor f ,, _).
      use eq_mor_eilenberg_moore.
      apply idpath.

    Definition is_monadic_connecting_functor_is_faithful
      : faithful is_monadic_connecting_functor.
    Show proof.
      intros z₁ z₂ g.
      use invproofirrelevance.
      intros f₁ f₂.
      use subtypePath.
      {
        intro.
        apply homset_property.
      }
      use eq_mor_eilenberg_moore.
      exact (maponpaths (λ z, pr11 z) (pr2 f₁ @ !(pr2 f₂))).

    Definition is_monadic_connecting_functor_is_equiv
      : adj_equivalence_of_cats is_monadic_connecting_functor.
    Show proof.
      use rad_equivalence_of_cats.
      - use is_univalent_eilenberg_moore_cat.
        apply is_univ_hom.
        exact HB_2_1.
      - use full_and_faithful_implies_fully_faithful.
        split.
        + exact is_monadic_connecting_functor_is_full.
        + exact is_monadic_connecting_functor_is_faithful.
      - exact is_monadic_connecting_functor_is_eso.

    Section CommuteData.
      Context (f : w --> y).

      Definition is_monadic_commute_cell
        : f
          · comparison_mor HB l
          · mor_of_mnd_mor
              (mor_of_em_cone
                 (mnd_from_adjunction l)
                 (pr1 (HB (mnd_from_adjunction l))))
          ==>
          f · left_adjoint_right_adjoint l
        := rassociator _ _ _ • (f ◃ comparison_mor_inv2cell HB l).

      Definition is_monadic_commute_eq
        : (rassociator _ _ _
          • (rassociator _ _ _
          • (_ ◃ (mnd_mor_endo
                    (mor_of_em_cone
                       (mnd_from_adjunction l)
                       (pr1 (HB (mnd_from_adjunction l))))
                  • lunitor _))))
          • is_monadic_commute_cell
          =
          ((is_monadic_commute_cell ▹ l) ▹ left_adjoint_right_adjoint l)
          • (id₂ _
          • (((rassociator _ _ _
             • (f ◃ left_adjoint_counit l))
             • runitor f) ▹ left_adjoint_right_adjoint l)).
      Show proof.
        unfold is_monadic_commute_cell.
        rewrite id2_left.
        rewrite !vassocl.
        etrans.
        {
          do 2 apply maponpaths.
          rewrite !vassocr.
          rewrite <- lwhisker_lwhisker_rassociator.
          rewrite !vassocl.
          apply maponpaths.
          rewrite lwhisker_vcomp.
          apply maponpaths.
          rewrite <- !lwhisker_vcomp.
          exact (comparison_mor_eq HB l).
        }
        rewrite <- !lwhisker_vcomp.
        rewrite !vassocl.
        refine (!_).
        etrans.
        {
          apply maponpaths.
          rewrite <- !rwhisker_vcomp.
          rewrite <- lunitor_lwhisker.
          apply maponpaths.
          rewrite !vassocr.
          rewrite <- rwhisker_lwhisker_rassociator.
          apply idpath.
        }
        rewrite !vassocr.
        do 2 apply maponpaths_2.
        refine (!_).
        etrans.
        {
          rewrite !vassocl.
          do 4 apply maponpaths.
          rewrite lwhisker_vcomp.
          rewrite rwhisker_rwhisker.
          rewrite <- lwhisker_vcomp.
          apply idpath.
        }
        rewrite !vassocr.
        use vcomp_move_R_Mp ; [ is_iso | ].
        rewrite !vassocl.
        refine (!_).
        etrans.
        {
          apply maponpaths.
          rewrite !vassocr.
          apply rassociator_rassociator.
        }
        etrans.
        {
          rewrite <- !rwhisker_vcomp.
          rewrite !vassocl.
          apply maponpaths.
          rewrite !vassocr.
          rewrite rwhisker_rwhisker_alt.
          rewrite !vassocl.
          rewrite <- rwhisker_lwhisker_rassociator.
          apply idpath.
        }
        rewrite !vassocr.
        apply maponpaths_2.
        rewrite !vassocl.
        refine (!_).
        etrans.
        {
          apply maponpaths.
          rewrite !vassocr.
          rewrite <- rassociator_rassociator.
          rewrite !vassocl.
          rewrite lwhisker_vcomp.
          rewrite rassociator_lassociator.
          rewrite lwhisker_id2.
          rewrite id2_right.
          apply idpath.
        }
        rewrite !vassocr.
        rewrite rwhisker_rwhisker_alt.
        rewrite !vassocl.
        apply idpath.
    End CommuteData.

    Definition is_monadic_commute_data
      : nat_trans_data (G ∙ (H ∙ is_monadic_connecting_functor)) F.
    Show proof.
      intro f.
      use make_mor_eilenberg_moore.
      - exact (is_monadic_commute_cell f).
      - exact (is_monadic_commute_eq f).

    Definition is_monadic_commute_is_nat_trans
      : is_nat_trans _ _ is_monadic_commute_data.
    Show proof.
      intros f₁ f₂ τ.
      use eq_mor_eilenberg_moore.
      cbn ; unfold is_monadic_commute_cell.
      rewrite !vassocl.
      rewrite <- vcomp_whisker.
      rewrite !vassocr.
      apply maponpaths_2.
      rewrite rwhisker_rwhisker_alt.
      apply idpath.

    Definition is_monadic_commute
      : G ∙ (H ∙ is_monadic_connecting_functor) ⟹ F.
    Show proof.
      use make_nat_trans.
      - exact is_monadic_commute_data.
      - exact is_monadic_commute_is_nat_trans.

    Definition is_monadic_commute_nat_z_iso
      : nat_z_iso (G ∙ (H ∙ is_monadic_connecting_functor)) F.
    Show proof.
      use make_nat_z_iso.
      - exact is_monadic_commute.
      - intro f.
        use is_z_iso_eilenberg_moore.
        use is_inv2cell_to_is_z_iso.
        cbn ; unfold is_monadic_commute_cell.
        is_iso.
        exact (pr2 (comparison_mor_inv2cell HB l)).

    Definition comp_connecting_functor_equiv
      : adj_equivalence_of_cats (H ∙ is_monadic_connecting_functor).
    Show proof.
      use comp_adj_equivalence_of_cats.
      - apply is_universal_em_cone_weq_is_em_universal_em_cone.
        + exact HB_2_1.
        + apply has_em_ump_is_universal.
          exact (pr2 (HB (mnd_from_adjunction l))).
      - exact is_monadic_connecting_functor_is_equiv.

    Definition monadic_repr_triangle_1
               (HG : adj_equivalence_of_cats G)
      : adj_equivalence_of_cats F.
    Show proof.
      use (two_out_of_three_comp
             _ _ _
             is_monadic_commute_nat_z_iso).
      - exact HG.
      - exact comp_connecting_functor_equiv.

    Definition monadic_repr_triangle_2
               (HF : adj_equivalence_of_cats F)
      : adj_equivalence_of_cats G.
    Show proof.
      use (two_out_of_three_first
             _ _ _
             is_monadic_commute_nat_z_iso).
      - exact comp_connecting_functor_equiv.
      - exact HF.
  End DiagramOfMonadicRepr.

  Definition is_monadic_to_is_monadic_repr
             (Hl : is_monadic HB l)
    : is_monadic_repr HB_2_1 l.
  Show proof.
    intro w.
    apply equiv_cat_to_adj_equiv.
    apply monadic_repr_triangle_1.
    apply left_adjequiv_to_left_adjequiv_repr.
    exact Hl.

  Definition is_monadic_repr_to_is_monadic
             (Hl : is_monadic_repr HB_2_1 l)
    : is_monadic HB l.
  Show proof.
    use left_adjoint_repr_to_left_adjoint_equivalence.
    intro w.
    apply monadic_repr_triangle_2.
    exact (adj_equiv_to_equiv_cat _ (Hl w)).

  Definition is_monadic_repr_weq_is_monadic
    : is_monadic_repr HB_2_1 l ≃ is_monadic HB l.
  Show proof.
    use weqimplimpl.
    - exact is_monadic_repr_to_is_monadic.
    - exact is_monadic_to_is_monadic_repr.
    - apply isaprop_is_monadic_repr.
    - apply isaprop_is_monadic.
      exact HB_2_1.
End MonadicReprWeqMonadic.