Library UniMath.CategoryTheory.DisplayedCats.Examples.AlgebraStructures

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Adjunctions.Reflections.
Require Import UniMath.CategoryTheory.Categories.HSET.All.
Require Import UniMath.CategoryTheory.Limits.BinProducts.
Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
Require Import UniMath.CategoryTheory.Limits.Equalizers.
Require Import UniMath.CategoryTheory.Limits.Coequalizers.
Require Import UniMath.CategoryTheory.Limits.Products.
Require Import UniMath.CategoryTheory.Limits.Preservation.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure.
Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits.
Require Import UniMath.CategoryTheory.Monads.Monads.

Local Open Scope cat.

Section MonadToStruct.
  Context (M : Monad SET).

1. Algebra structures
  Definition monad_algebra_laws
             {X : SET}
             (f : M X --> X)
    : UU
    := (η M X · f = identity X)
       ×
       (μ M X · f = #M f · f).

  Definition monad_algebra
             (X : SET)
    : UU
    := ∑ (f : M X --> X), monad_algebra_laws f.

  Definition make_monad_algebra
             {X : SET}
             (f : M X --> X)
             (p : monad_algebra_laws f)
    : monad_algebra X
    := f ,, p.

  Coercion monad_algebra_struct_to_mor
           {X : hSet}
           (f : monad_algebra X)
    : M X --> X
    := pr1 f.

  Proposition monad_algebra_unit
              {X : hSet}
              (f : monad_algebra X)
    : η M X · f = identity _.
  Show proof.
    exact (pr12 f).

  Proposition monad_algebra_mu
              {X : hSet}
              (f : monad_algebra X)
    : μ M X · f = #M f · f.
  Show proof.
    exact (pr22 f).

  Definition monad_to_hset_struct_data
    : hset_struct_data.
  Show proof.
    simple refine (_ ,, _).
    - exact monad_algebra.
    - exact (λ X Y f g h, f · h = #M h · g).

  Proposition monad_to_hset_struct_laws
    : hset_struct_laws monad_to_hset_struct_data.
  Show proof.
    repeat split.
    - intro X.
      use isaset_total2.
      + apply homset_property.
      + intro f.
        apply isasetaprop.
        apply isapropdirprod ; apply homset_property.
    - intros X Y f g h.
      apply homset_property.
    - intros X f ; cbn.
      rewrite (functor_id M).
      apply idpath.
    - intros X Y Z fX fY fZ h₁ h₂ Mh₁ Mh₂ ; cbn -[Monad] in *.
      use funextsec.
      intro x.
      rewrite (eqtohomot Mh₁).
      rewrite (eqtohomot Mh₂).
      rewrite (eqtohomot (functor_comp M h₁ h₂)).
      apply idpath.
    - intros X fX fX' p q.
      use subtypePath.
      {
        intro.
        apply isapropdirprod ; apply homset_property.
      }
      cbn -[Monad] in *.
      use funextsec.
      intro x.
      refine (eqtohomot p x @ _).
      apply maponpaths.
      exact (eqtohomot (functor_id M X) x).

  Definition monad_to_hset_struct
    : hset_struct
    := monad_to_hset_struct_data ,, monad_to_hset_struct_laws.

  Definition category_of_monad_algebra
    : category
    := category_of_hset_struct monad_to_hset_struct.

2. The cartesian structure of algebras
  Proposition unit_monad_algebra_laws
    : @monad_algebra_laws unitHSET (λ _, tt).
  Show proof.
    split.
    - cbn.
      use funextsec.
      intro x.
      apply isapropunit.
    - apply idpath.

  Definition unit_monad_algebra
    : monad_algebra unitHSET.
  Show proof.
    use make_monad_algebra.
    - exact (λ _, tt).
    - exact unit_monad_algebra_laws.

  Section ProdAlgebra.
    Context {X Y : SET}
            (f : monad_algebra X)
            (g : monad_algebra Y).

    Let XY : SET := (X × Y)%set.
    Let p₁ : XY --> X := dirprod_pr1.
    Let p₂ : XY --> Y := dirprod_pr2.

    Definition prod_monad_algebra_map
      : M XY --> XY
      := BinProductArrow _ (BinProductsHSET X Y) (#M p₁ · f) (#M p₂ · g).

    Proposition prod_monad_algebra_laws
      : monad_algebra_laws prod_monad_algebra_map.
    Show proof.
      split.
      - use (BinProductArrowsEq _ _ _ (BinProductsHSET X Y)).
        + rewrite !assoc'.
          etrans.
          {
            apply maponpaths.
            apply (BinProductPr1Commutes _ _ _ (BinProductsHSET X Y)).
          }
          rewrite !assoc.
          rewrite id_left.
          rewrite <- (nat_trans_ax (η M) _ _ p₁).
          rewrite !assoc'.
          rewrite (monad_algebra_unit f).
          apply idpath.
        + rewrite !assoc'.
          etrans.
          {
            apply maponpaths.
            apply (BinProductPr2Commutes _ _ _ (BinProductsHSET X Y)).
          }
          rewrite !assoc.
          rewrite id_left.
          rewrite <- (nat_trans_ax (η M) _ _ p₂).
          rewrite !assoc'.
          rewrite (monad_algebra_unit g).
          apply idpath.
      - use (BinProductArrowsEq _ _ _ (BinProductsHSET X Y)).
        + rewrite !assoc'.
          etrans.
          {
            apply maponpaths.
            apply (BinProductPr1Commutes _ _ _ (BinProductsHSET X Y)).
          }
          refine (!_).
          etrans.
          {
            apply maponpaths.
            apply (BinProductPr1Commutes _ _ _ (BinProductsHSET X Y)).
          }
          rewrite !assoc.
          rewrite <- functor_comp.
          etrans.
          {
            apply maponpaths_2.
            apply maponpaths.
            apply (BinProductPr1Commutes _ _ _ (BinProductsHSET X Y)).
          }
          rewrite <- (nat_trans_ax (μ M) _ _ p₁).
          rewrite functor_comp.
          rewrite !assoc'.
          rewrite (monad_algebra_mu f).
          apply idpath.
        + rewrite !assoc'.
          etrans.
          {
            apply maponpaths.
            apply (BinProductPr2Commutes _ _ _ (BinProductsHSET X Y)).
          }
          refine (!_).
          etrans.
          {
            apply maponpaths.
            apply (BinProductPr2Commutes _ _ _ (BinProductsHSET X Y)).
          }
          rewrite !assoc.
          rewrite <- functor_comp.
          etrans.
          {
            apply maponpaths_2.
            apply maponpaths.
            apply (BinProductPr2Commutes _ _ _ (BinProductsHSET X Y)).
          }
          rewrite <- (nat_trans_ax (μ M) _ _ p₂).
          rewrite functor_comp.
          rewrite !assoc'.
          rewrite (monad_algebra_mu g).
          apply idpath.

    Definition prod_monad_algebra
      : monad_algebra XY.
    Show proof.
      use make_monad_algebra.
      - exact prod_monad_algebra_map.
      - exact prod_monad_algebra_laws.
  End ProdAlgebra.

  Definition monad_to_hset_cartesian_struct_data
    : hset_cartesian_struct_data
    := monad_to_hset_struct
       ,, unit_monad_algebra
       ,, λ X Y f g, prod_monad_algebra f g.

  Proposition monad_to_hset_cartesian_struct_laws
    : hset_cartesian_struct_laws monad_to_hset_cartesian_struct_data.
  Show proof.
    split4.
    - intros X f ; cbn.
      apply idpath.
    - intros X Y f g ; cbn.
      apply idpath.
    - intros X Y f g ; cbn.
      apply idpath.
    - intros W X Y fW fX fY g₁ g₂ Mg₁ Mg₂ ; cbn -[Monad] in *.
      use funextsec.
      intro x.
      use pathsdirprod ; cbn.
      + refine (eqtohomot Mg₁ _ @ _).
        apply maponpaths.
        refine (!_).
        etrans.
        {
          refine (!_).
          apply (eqtohomot (functor_comp M _ _)).
        }
        apply idpath.
      + refine (eqtohomot Mg₂ _ @ _).
        apply maponpaths.
        refine (!_).
        etrans.
        {
          refine (!_).
          apply (eqtohomot (functor_comp M _ _)).
        }
        apply idpath.

  Definition monad_to_hset_cartesian_struct
    : hset_cartesian_struct
    := monad_to_hset_cartesian_struct_data
       ,,
       monad_to_hset_cartesian_struct_laws.

3. Equalizers of algebras
  Section EqualizerAlgebra.
    Context {X Y : SET}
            {f g : X --> Y}
            (hX : monad_algebra X)
            (hY : monad_algebra Y)
            (Mf : hX · f = #M f · hY)
            (Mg : hX · g = #M g · hY).

    Let E : SET := (∑ x, hProp_to_hSet (eqset (f x) (g x)))%set.
    Let π : E --> X := λ z, pr1 z.

    Definition equalizer_algebra_map
      : M E --> E.
    Show proof.
      use (EqualizerIn (Equalizers_in_HSET X Y f g)).
      - exact (#M π · hX).
      - abstract
          (rewrite !assoc' ;
           rewrite Mf, Mg ;
           rewrite !assoc ;
           apply maponpaths_2 ;
           rewrite <- !functor_comp ;
           apply maponpaths ;
           apply (EqualizerEqAr (Equalizers_in_HSET X Y f g))).

    Proposition equalizer_algebra_laws
      : monad_algebra_laws equalizer_algebra_map.
    Show proof.
      split.
      - use (EqualizerInsEq (Equalizers_in_HSET X Y f g)).
        rewrite !assoc'.
        etrans.
        {
          apply maponpaths.
          apply (EqualizerCommutes (Equalizers_in_HSET X Y f g)).
        }
        rewrite !id_left.
        rewrite !assoc.
        rewrite <- (nat_trans_ax (η M) _ _ π).
        rewrite !assoc'.
        rewrite monad_algebra_unit.
        rewrite id_right.
        apply idpath.
      - use (EqualizerInsEq (Equalizers_in_HSET X Y f g)).
        rewrite !assoc'.
        etrans.
        {
          apply maponpaths.
          apply (EqualizerCommutes (Equalizers_in_HSET X Y f g)).
        }
        refine (!_).
        etrans.
        {
          apply maponpaths.
          apply (EqualizerCommutes (Equalizers_in_HSET X Y f g)).
        }
        rewrite !assoc.
        rewrite <- functor_comp.
        etrans.
        {
          apply maponpaths_2.
          apply maponpaths.
          apply (EqualizerCommutes (Equalizers_in_HSET X Y f g)).
        }
        rewrite <- (nat_trans_ax (μ M) _ _ π).
        rewrite functor_comp.
        rewrite !assoc'.
        rewrite (monad_algebra_mu hX).
        apply idpath.

    Definition equalizer_algebra
      : monad_algebra E.
    Show proof.
      use make_monad_algebra.
      - exact equalizer_algebra_map.
      - exact equalizer_algebra_laws.
  End EqualizerAlgebra.

  Definition monad_to_hset_equalizer_struct_data
    : hset_equalizer_struct_data monad_to_hset_struct
    := λ X Y f g hX hY Mf Mg, equalizer_algebra hX hY Mf Mg.

  Proposition monad_to_hset_equalizer_struct_laws
    : hset_equalizer_struct_laws monad_to_hset_equalizer_struct_data.
  Show proof.
    split.
    - intros X Y f g hX hY Mf Mg.
      apply idpath.
    - intros X Y f g hX hY Mf Mg W hW k Mk q.
      use funextsec.
      intro x.
      use subtypePath.
      {
        intro.
        apply setproperty.
      }
      cbn -[Monad] in *.
      refine (eqtohomot Mk x @ _).
      apply maponpaths.
      refine (!_).
      exact (!(eqtohomot (functor_comp M _ _) _)).

  Definition monad_to_hset_equalizer_struct
    : hset_equalizer_struct monad_to_hset_struct
    := monad_to_hset_equalizer_struct_data
       ,,
       monad_to_hset_equalizer_struct_laws.

4. Type indexed products of algebras
  Section TypeProdAlgebra.
    Context {J : UU}
            {D : J → hSet}
            (p : ∏ (i : J), monad_algebra (D i)).

    Let prod : Product J SET D := ProductsHSET J D.

    Definition monad_type_prod_map
      : M prod --> prod
      := ProductArrow _ _ prod (λ i, #M (ProductPr _ _ _ i) · p i).

    Proposition monad_type_prod_laws
      : monad_algebra_laws monad_type_prod_map.
    Show proof.
      split.
      - use (ProductArrow_eq _ _ _ prod).
        intro i.
        rewrite id_left.
        rewrite !assoc'.
        etrans.
        {
          apply maponpaths.
          apply ProductPrCommutes.
        }
        rewrite !assoc.
        rewrite <- (nat_trans_ax (η M)).
        rewrite !assoc'.
        rewrite (monad_algebra_unit (p i)).
        rewrite id_right.
        apply idpath.
      - use (ProductArrow_eq _ _ _ prod).
        intro i.
        rewrite !assoc'.
        etrans.
        {
          apply maponpaths.
          apply ProductPrCommutes.
        }
        refine (!_).
        etrans.
        {
          apply maponpaths.
          apply ProductPrCommutes.
        }
        rewrite !assoc.
        rewrite <- functor_comp.
        etrans.
        {
          apply maponpaths_2.
          apply maponpaths.
          apply ProductPrCommutes.
        }
        rewrite <- (nat_trans_ax (μ M)).
        rewrite functor_comp.
        rewrite !assoc'.
        rewrite (monad_algebra_mu (p i)).
        apply idpath.
  End TypeProdAlgebra.

  Definition monad_to_hset_struct_type_prod_data
             (J : UU)
    : hset_struct_type_prod_data monad_to_hset_struct J.
  Show proof.
    intros D p.
    use make_monad_algebra.
    - exact (monad_type_prod_map p).
    - exact (monad_type_prod_laws p).

  Proposition monad_to_hset_struct_type_prod_laws
              (J : UU)
    : hset_struct_type_prod_laws (monad_to_hset_struct_type_prod_data J).
  Show proof.
    split.
    - intros D PD i.
      apply idpath.
    - intros D PD W hW ps Mps.
      cbn -[Monad] in *.
      use funextsec ; intro x.
      use funextsec ; intro i.
      refine (eqtohomot (Mps i) x @ _).
      apply maponpaths.
      refine (!_).
      exact (!(eqtohomot (functor_comp M _ _) _)).

  Definition monad_to_hset_struct_type_prod
             (J : UU)
    : hset_struct_type_prod monad_to_hset_struct J
    := monad_to_hset_struct_type_prod_data J
       ,,
       monad_to_hset_struct_type_prod_laws J.

5. The free algebra adjunction
  Proposition monad_free_alg_laws
              (X : hSet)
    : monad_algebra_laws (μ M X).
  Show proof.
    split.
    - apply Monad_law1.
    - exact (!(@Monad_law3 _ M X)).

  Definition monad_free_alg_struct
             (X : hSet)
    : monad_algebra (M X).
  Show proof.
    use make_monad_algebra.
    - exact (μ M X).
    - exact (monad_free_alg_laws X).

  Definition monad_free_alg
             (X : hSet)
    : category_of_monad_algebra
    := M X ,, monad_free_alg_struct X.

  Section FreeAlgAdjunction.
    Context {X : hSet}
            {Y : hSet}
            (hY : monad_algebra Y)
            (f : X → Y).

    Let YY : category_of_monad_algebra
      := Y ,, hY.

    Definition monad_to_hset_struct_adj_lift
      : monad_free_alg X --> YY.
    Show proof.
      refine (#M f · hY ,, _).
      cbn.
      use funextsec.
      intro x.
      etrans.
      {
        apply maponpaths.
        exact (!(eqtohomot (nat_trans_ax (μ M) _ _ f) x)).
      }
      cbn.
      refine (eqtohomot (monad_algebra_mu hY) (# M (# M f) x) @ _).
      cbn.
      apply maponpaths.
      exact (!(eqtohomot (functor_comp M _ _) _)).

    Proposition monad_to_hset_struct_adj_lift_eq
      : f = η M X · #M f · hY.
    Show proof.
      rewrite <- (nat_trans_ax (η M) _ _ f).
      rewrite !assoc'.
      refine (!id_right (f : SET⟦_, _⟧) @ _).
      apply maponpaths.
      exact (!monad_algebra_unit hY).

    Proposition monad_to_hset_struct_adj_lift_unique
      (g : monad_free_alg X --> YY)
      (Hg : f = η M X · # (underlying_of_hset_struct monad_to_hset_struct) g)
      : g = monad_to_hset_struct_adj_lift.
    Show proof.
      use eq_mor_hset_struct.
      cbn ; intro x.
      refine (!maponpaths (pr1 g) (eqtohomot (@Monad_law2 _ M X) x) @ _).
      cbn.
      pose (eqtohomot (pr2 g) (# M (η M X) x)) as p.
      cbn in p.
      rewrite p ; clear p.
      apply maponpaths.
      refine (!eqtohomot (functor_comp M (η M X) (pr1 g)) x @ _).
      apply (maponpaths_2 _ (!Hg)).

  End FreeAlgAdjunction.

  Definition monad_underlying_is_right_adjoint
    : is_right_adjoint (underlying_of_hset_struct monad_to_hset_struct).
  Show proof.
    apply reflections_to_is_right_adjoint.
    intro X.
    use make_reflection'.
    - exact (monad_free_alg X).
    - exact (η M X).
    - intro f.
      use make_reflection_arrow.
      + exact (monad_to_hset_struct_adj_lift _ (f : _ --> _)).
      + exact (monad_to_hset_struct_adj_lift_eq _ (f : _ --> _)).
      + exact (monad_to_hset_struct_adj_lift_unique _ _).

  Definition monad_free_alg_functor
    : SET ⟶ category_of_monad_algebra
    := left_adjoint
         monad_underlying_is_right_adjoint.

  Definition monad_free_alg_unit
    : functor_identity _
      ⟹
      monad_free_alg_functor ∙ underlying_of_hset_struct monad_to_hset_struct
    := unit_from_right_adjoint monad_underlying_is_right_adjoint.

  Definition monad_free_alg_counit
    : underlying_of_hset_struct monad_to_hset_struct ∙ monad_free_alg_functor
      ⟹
      functor_identity _
    := counit_from_right_adjoint monad_underlying_is_right_adjoint.

  Definition free_alg_coproduct
             (X Y : hSet)
    : BinCoproduct (monad_free_alg X) (monad_free_alg Y)
    := (monad_free_alg (setcoprod X Y) ,, _ ,, _)
       ,,
       left_adjoint_preserves_bincoproduct
         (left_adjoint
            monad_underlying_is_right_adjoint)
         (is_left_adjoint_left_adjoint _)
         _ _ _ _ _
         (pr2 (BinCoproductsHSET X Y)).

  Proposition mor_from_free_alg_eq
              {X : hSet}
              {Y : category_of_monad_algebra}
              {f g : monad_free_alg_functor X --> Y}
              (p : η M X · pr1 f = η M X · pr1 g)
    : f = g.
  Show proof.
    refine (!(id_left _) @ _ @ id_left _).
    etrans.
    {
      apply maponpaths_2.
      refine (!_).
      exact (triangle_id_left_ad
               (pr2 monad_underlying_is_right_adjoint)
               X).
    }
    refine (!_).
    etrans.
    {
      apply maponpaths_2.
      refine (!_).
      exact (triangle_id_left_ad
               (pr2 monad_underlying_is_right_adjoint)
               X).
    }
    refine (!_).
    rewrite !assoc'.
    use subtypePath.
    {
      intro ; apply homset_property.
    }
    enough (# M (η M X · η M (M X)) · μ M (M X) · (# M (identity _) · μ M X · pr1 f)
            =
            # M (η M X · η M (M X)) · μ M (M X) · (# M (identity _) · μ M X · pr1 g))
      as q.
    {
      exact q.
    }
    rewrite !functor_id.
    rewrite id_left.
    etrans.
    {
      apply maponpaths.
      exact (pr2 f).
    }
    refine (!_).
    etrans.
    {
      apply maponpaths.
      exact (pr2 g).
    }
    refine (!_).
    rewrite !assoc.
    apply maponpaths_2.
    rewrite !functor_comp.
    rewrite !assoc'.
    rewrite !(maponpaths (λ z, _ · z) (assoc _ _ _)).
    etrans.
    {
      apply maponpaths.
      apply maponpaths_2.
      exact (@Monad_law2 _ M (M X)).
    }
    refine (!_).
    etrans.
    {
      apply maponpaths.
      apply maponpaths_2.
      exact (@Monad_law2 _ M (M X)).
    }
    refine (!_).
    rewrite !id_left.
    rewrite <- !functor_comp.
    apply maponpaths.
    exact p.

6. Every algebra is a coequalizer of a free algebra
  Section AlgebraAsCoequalizer.
    Context {X : hSet}
            (hX : monad_algebra X).

    Let F : SET ⟶ category_of_monad_algebra := monad_free_alg_functor.
    Let AX : category_of_monad_algebra := X ,, hX.

    Let FX : category_of_monad_algebra := monad_free_alg X.
    Let FUFX : category_of_monad_algebra := monad_free_alg (pr1 FX).

    Definition algebra_as_coequalizer_left_map
      : FUFX --> FX
      := monad_free_alg_counit FX.

    Let ℓ : FUFX --> FX := algebra_as_coequalizer_left_map.

    Definition algebra_as_coequalizer_right_map
      : FUFX --> FX
      := #F hX.

    Let ρ : FUFX --> FX := algebra_as_coequalizer_right_map.

    Definition algebra_as_coequalizer_arr
      : FX --> AX.
    Show proof.
      simple refine (_ ,, _).
      - exact hX.
      - exact (monad_algebra_mu hX).

    Proposition algebra_as_coequalizer_arr_eq
      : ℓ · algebra_as_coequalizer_arr
        =
        ρ · algebra_as_coequalizer_arr.
    Show proof.
      unfold ℓ, ρ.
      unfold algebra_as_coequalizer_left_map.
      unfold algebra_as_coequalizer_right_map.
      use subtypePath.
      {
        intro.
        apply homset_property.
      }
      simpl.
      rewrite (functor_id M).
      etrans.
      {
        apply maponpaths_2.
        exact (id_left (μ M X)).
      }
      refine (monad_algebra_mu hX @ _).
      apply maponpaths_2.
      rewrite (functor_comp M).
      refine (_ @ assoc _ _ _).
      refine (!(id_right _) @ _).
      apply maponpaths.
      refine (!_).
      apply Monad_law2.

    Section UMP.
      Context {Y : category_of_monad_algebra}
              (g : FX --> Y)
              (p : ℓ · g = ρ · g).

      Proposition algebra_as_coequalizer_ump_unique
        : isaprop (∑ φ, algebra_as_coequalizer_arr · φ = g).
      Show proof.
        use invproofirrelevance.
        intros φ₁ φ₂.
        use subtypePath.
        {
          intro.
          apply homset_property.
        }
        use subtypePath.
        {
          intro.
          apply homset_property.
        }
        refine (!(id_left _) @ _ @ id_left _).
        etrans.
        {
          apply maponpaths_2.
          exact (!(monad_algebra_unit hX)).
        }
        refine (!_).
        etrans.
        {
          apply maponpaths_2.
          exact (!(monad_algebra_unit hX)).
        }
        rewrite !assoc'.
        apply maponpaths.
        refine (!_).
        exact (maponpaths pr1 (pr2 φ₁ @ !(pr2 φ₂))).

      Lemma algebra_as_coequalizer_ump_eq_lem_1
        : # M hX · pr1 g = μ M X · pr1 g.
      Show proof.
        refine (_ @ maponpaths pr1 (!p) @ _).
        - refine (maponpaths (λ z, z · _) _).
          simpl.
          rewrite (functor_comp M).
          refine (_ @ assoc (#M hX) _ _).
          refine (!(id_right _) @ _).
          apply maponpaths.
          refine (!_).
          apply Monad_law2.
        - refine (maponpaths (λ z, z · _) _).
          refine (_ @ id_left _).
          refine (maponpaths (λ z, z · _) _).
          apply functor_id.

      Lemma algebra_as_coequalizer_ump_eq_lem_2
        : hX · η M X · pr1 g = pr1 g.
      Show proof.
        etrans.
        {
          apply maponpaths_2.
          exact (nat_trans_ax (η M) _ _ hX).
        }
        rewrite !assoc'.
        rewrite algebra_as_coequalizer_ump_eq_lem_1.
        rewrite !assoc.
        refine (_ @ id_left _).
        apply maponpaths_2.
        apply Monad_law1.

      Lemma algebra_as_coequalizer_ump_eq
        : hX · (η M X · pr1 g) = # M (η M X · pr1 g) · pr12 Y.
      Show proof.
        rewrite functor_comp.
        rewrite !assoc'.
        refine (!_).
        etrans.
        {
          apply maponpaths.
          exact (!(pr2 g)).
        }
        rewrite !assoc.
        rewrite (@Monad_law2 _ M).
        rewrite id_left.
        refine (!_).
        apply algebra_as_coequalizer_ump_eq_lem_2.

      Definition algebra_as_coequalizer_ump
        : AX --> Y.
      Show proof.
        simple refine (_ ,, _).
        - exact (η M X · pr1 g).
        - exact algebra_as_coequalizer_ump_eq.

      Proposition algebra_as_coequalizer_ump_comm
        : algebra_as_coequalizer_arr · algebra_as_coequalizer_ump = g.
      Show proof.
        use subtypePath.
        {
          intro.
          apply homset_property.
        }
        simpl.
        apply algebra_as_coequalizer_ump_eq_lem_2.
    End UMP.

    Definition algebra_as_coequalizer
      : Coequalizer ℓ ρ.
    Show proof.
      use make_Coequalizer.
      - exact AX.
      - exact algebra_as_coequalizer_arr.
      - exact algebra_as_coequalizer_arr_eq.
      - intros Y g p.
        use iscontraprop1.
        + exact (algebra_as_coequalizer_ump_unique g).
        + simple refine (_ ,, _).
          * exact (algebra_as_coequalizer_ump g p).
          * exact (algebra_as_coequalizer_ump_comm g p).
  End AlgebraAsCoequalizer.
End MonadToStruct.