Library UniMath.CategoryTheory.Monads.Monads

**********************************************************
Contents:
Written by: Benedikt Ahrens (started March 2015) Extended by: Anders Mörtberg, 2016 Extended by: Ralph Matthes, 2017 (Section MonadsUsingCoproducts) Rewrite by: Ralph Matthes, 2023, defining the category of monads through a displayed category over the endofunctors, this gives the previously missing univalence result nearly for free

Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.

Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.MoreFoundations.Notations.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Limits.Terminal.
Require Import UniMath.CategoryTheory.Limits.BinCoproducts.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
Require Import UniMath.CategoryTheory.DisplayedCats.SIP.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.Core.Univalence.

Local Open Scope cat.

Section Monad_disp_def.

  Context {C : category}.

  Definition disp_Monad_data (F : functor C C) : UU :=
    (F F F) × (functor_identity C F).

  Definition disp_μ {F : functor C C} (T : disp_Monad_data F) : F F F := pr1 T.
  Definition disp_η {F : functor C C} (T : disp_Monad_data F) : functor_identity C F := pr2 T.

  Definition disp_Monad_laws {F : functor C C} (T : disp_Monad_data F) : UU :=
    (
      ( c : C, disp_η T (F c) · disp_μ T c = identity (F c))
      ×
      ( c : C, #F (disp_η T c) · disp_μ T c = identity (F c)) )
      ×
      ( c : C, #F (disp_μ T c) · disp_μ T c = disp_μ T (F c) · disp_μ T c).

  Lemma isaprop_disp_Monad_laws {F : functor C C} (T : disp_Monad_data F) : isaprop (disp_Monad_laws T).
  Show proof.
    repeat apply isapropdirprod;
      apply impred; intro c; apply C.

  Definition disp_Monad_Mor_laws {F F' : functor C C} (T : disp_Monad_data F) (T' : disp_Monad_data F') (α : F F') : UU :=
    ( a : C, disp_μ T a · α a = α (F a) · #F' (α a) · disp_μ T' a) ×
    ( a : C, disp_η T a · α a = disp_η T' a).

  Lemma isaprop_disp_Monad_Mor_laws {F F' : functor C C} (T : disp_Monad_data F) (T' : disp_Monad_data F') (α : F F')
    : isaprop (disp_Monad_Mor_laws T T' α).
  Show proof.
    apply isapropdirprod;
      apply impred; intro c; apply C.


  Lemma monads_category_id_subproof {F : functor C C} (T : disp_Monad_data F) (Tlaws : disp_Monad_laws T) :
    disp_Monad_Mor_laws T T (nat_trans_id F).
  Show proof.
    split; intros a; simpl.
    - now rewrite id_left, id_right, functor_id, id_left.
    - now apply id_right.

  Lemma monads_category_comp_subproof {F F' F'' : functor C C}
    (T : disp_Monad_data F) (Tlaws : disp_Monad_laws T)
    (T' : disp_Monad_data F') (T'laws : disp_Monad_laws T')
    (T'' : disp_Monad_data F'') (T''laws : disp_Monad_laws T'')
    (α : F F') (α' : F' F'') :
    disp_Monad_Mor_laws T T' α disp_Monad_Mor_laws T' T'' α' disp_Monad_Mor_laws T T'' (nat_trans_comp _ _ _ α α').
  Show proof.
    intros Hα'.
    split; intros; simpl.
    - rewrite assoc.
      set (H:=pr1 a); simpl in H.
      rewrite H; clear H; rewrite <- !assoc.
      set (H:=pr1 Hα' a); simpl in H.
      rewrite H; clear H.
      rewrite functor_comp.
      apply maponpaths.
      now rewrite !assoc, nat_trans_ax.
    - rewrite assoc.
      eapply pathscomp0; [apply cancel_postcomposition, (pr2 )|].
      apply (pr2 Hα').

  Definition monads_category_disp : disp_cat [C,C].
  Show proof.
    use disp_cat_from_SIP_data.
    - intro F. exact ( T : disp_Monad_data F, disp_Monad_laws T).
    - intros F F' [T Tlaws] [T' T'laws] α. exact (disp_Monad_Mor_laws T T' α).
    - intros F F' [T Tlaws] [T' T'laws] α. apply isaprop_disp_Monad_Mor_laws.
    - intros F [T Tlaws]. apply (monads_category_id_subproof _ Tlaws).
    - intros F F' F'' [T Tlaws] [T' T'laws] [T'' T''laws] α α'.
      apply (monads_category_comp_subproof _ Tlaws _ T'laws _ T''laws).

  Definition category_Monad : category := total_category monads_category_disp.

  Definition Monad : UU := ob category_Monad.

  #[reversible] Coercion functor_from_Monad (T : Monad) : functor C C := pr1 T.

  Definition μ (T : Monad) : T T T := pr112 T.
  Definition η (T : Monad) : functor_identity C T := pr212 T.

  Lemma Monad_law1 {T : Monad} : c : C, η T (T c) · μ T c = identity (T c).
  Show proof.
    exact (pr1 (pr122 T)).

  Lemma Monad_law2 {T : Monad} : c : C, #T (η T c) · μ T c = identity (T c).
  Show proof.
    exact (pr2 (pr122 T)).

  Lemma Monad_law3 {T : Monad} : c : C, #T (μ T c) · μ T c = μ T (T c) · μ T c.
  Show proof.
    exact (pr222 T).

  Lemma monads_category_disp_eq (F : functor C C) (T T' : monads_category_disp F) : pr1 T = pr1 T' -> T = T'.
  Show proof.
    intro H.
    induction T as [T Tlaws].
    induction T' as [T' T'laws].
    use total2_paths_f; [apply H |].
    apply isaprop_disp_Monad_laws.

  Lemma monads_category_Pisset (F : functor C C) : isaset ( T : disp_Monad_data F, disp_Monad_laws T).
  Show proof.
    change isaset with (isofhlevel 2).
    apply isofhleveltotal2.
    { apply isasetdirprod; apply [C,C]. }
    intro T.
    apply isasetaprop.
    apply isaprop_disp_Monad_laws.

  Lemma monads_category_Hstandard {F : functor C C}
    (T : disp_Monad_data F) (Tlaws : disp_Monad_laws T)
    (T' : disp_Monad_data F) (T'laws : disp_Monad_laws T') :
    disp_Monad_Mor_laws T T' (nat_trans_id F) disp_Monad_Mor_laws T' T (nat_trans_id F) T,, Tlaws = T',, T'laws.
  Show proof.
    intros H H'.
    apply subtypeInjectivity.
    { intro T0. apply isaprop_disp_Monad_laws. }
    cbn.
    induction T as [μ η].
    induction T' as [μ' η'].
    apply dirprodeq; cbn.
    - apply nat_trans_eq; [apply C|]. intro a.
      assert (Hinst := pr1 H a).
      cbn in Hinst.
      rewrite id_right in Hinst.
      rewrite id_left in Hinst.
      rewrite functor_id in Hinst.
      rewrite id_left in Hinst.
      exact Hinst.
    - apply nat_trans_eq; [apply C|]. intro a.
      assert (Hinst := pr2 H a).
      cbn in Hinst.
      rewrite id_right in Hinst.
      exact Hinst.

  Definition is_univalent_monads_category_disp : is_univalent_disp monads_category_disp.
  Show proof.
    use is_univalent_disp_from_SIP_data.
    - exact monads_category_Pisset.
    - intros F [T Tlaws] [T' T'laws]. apply monads_category_Hstandard.

End Monad_disp_def.

Arguments category_Monad _ : clear implicits.
Arguments Monad _ : clear implicits.

Definition is_univalent_category_Monad (C : univalent_category) :
  is_univalent (category_Monad C).
Show proof.
  apply SIP.
  - apply is_univalent_functor_category. apply C.
  - apply monads_category_Pisset.
  - intros F [T Tlaws] [T' T'laws]. apply monads_category_Hstandard.

Section pointfree.

  Context (C : category) (T0: functor C C) (T : disp_Monad_data T0).

  Let EndC := [C, C].

  Let η := disp_η T.
  Let μ := disp_μ T.

  Definition Monad_laws_pointfree : UU :=
    (
      (nat_trans_comp _ _ _ (pre_whisker T0 η) μ = identity(C:=EndC) T0)
        ×
      (nat_trans_comp _ _ _ (post_whisker η T0) μ = identity(C:=EndC) T0) )
        ×
      (nat_trans_comp _ _ _ (post_whisker μ T0) μ = nat_trans_comp _ _ _ (pre_whisker T0 μ) μ).

  Lemma pointfree_is_equiv: Monad_laws_pointfree <-> disp_Monad_laws T.
  Show proof.
    split.
    - intro H. induction H as [[H1 H2] H3].
      split.
      + split.
        * intro c. apply (maponpaths pr1) in H1. apply toforallpaths in H1. apply H1.
        * intro c. apply (maponpaths pr1) in H2. apply toforallpaths in H2. apply H2.
      + intro c. apply (maponpaths pr1) in H3. apply toforallpaths in H3. apply H3.
    - intro H. induction H as [[H1 H2] H3].
      split.
      + split.
        * apply nat_trans_eq_alt. exact H1.
        * apply nat_trans_eq_alt. exact H2.
      + apply nat_trans_eq; try apply homset_property. exact H3.

  Let T0' := T0 : EndC.
  Let η' := η: EndCfunctor_identity C, T0'.
  Let μ' := μ: EndCfunctor_compose T0' T0', T0'.

  Definition Monad_laws_pointfree_in_functor_category : UU :=
    (
      (#(pre_composition_functor _ _ _ T0') η' · μ' = identity(C:=EndC) T0')
        ×
      (#(post_composition_functor _ _ _ T0') η' · μ' = identity(C:=EndC) T0') )
        ×
      (#(post_composition_functor _ _ _ T0') μ' · μ' = (#(pre_composition_functor _ _ _ T0') μ') · μ').

the last variant of the laws is convertible with the one before
  Goal
    Monad_laws_pointfree = Monad_laws_pointfree_in_functor_category.
  Show proof.
    apply idpath.

End pointfree.

Definition Monad_Mor {C : category} (T T' : Monad C) : UU
  := category_Monad C T, T'.

#[reversible] Coercion nat_trans_from_monad_mor {C : category} (T T' : Monad C) (s : Monad_Mor T T')
  : T T' := pr1 s.

Definition Monad_Mor_laws {C : category} {T T' : Monad C} (α : T T')
  : UU :=
  ( a : C, μ T a · α a = α (T a) · #T' (α a) · μ T' a) ×
    ( a : C, η T a · α a = η T' a).

Definition Monad_Mor_η {C : category} {T T' : Monad C} (α : Monad_Mor T T')
  : a : C, η T a · α a = η T' a.
Show proof.
  exact (pr22 α).

Definition Monad_Mor_μ {C : category} {T T' : Monad C} (α : Monad_Mor T T')
  : a : C, μ T a · α a = α (T a) · #T' (α a) · μ T' a.
Show proof.
  exact (pr12 α).

Definition Monad_Mor_equiv {C : category}
  {T T' : Monad C} (α β : Monad_Mor T T')
  : α = β (pr1 α = pr1 β).
Show proof.
  apply subtypeInjectivity; intro a.
  apply isaprop_disp_Monad_Mor_laws.

Lemma isaset_Monad_Mor {C : category} (T T' : Monad C) : isaset (Monad_Mor T T').
Show proof.
  apply homset_property.

Definition Monad_composition {C : category} {T T' T'' : Monad C}
  (α : Monad_Mor T T') (α' : Monad_Mor T' T'')
  : Monad_Mor T T'' := α · α'.

Definition forgetfunctor_Monad (C : category) : functor (category_Monad C) [C,C]
  := pr1_category monads_category_disp.

Lemma forgetMonad_faithful (C : category) : faithful (forgetfunctor_Monad C).
Show proof.
  apply faithful_pr1_category.
  intros T T' α.
  apply isaprop_disp_Monad_Mor_laws.

Definition and lemmas for bind

Section bind.

Definition of bind

  Context {C : category} {T : Monad C}.

  Definition bind {a b : C} (f : Ca,T b) : CT a,T b := # T f · μ T b.

  Lemma η_bind {a b : C} (f : Ca,T b) : η T a · bind f = f.
  Show proof.
    unfold bind.
    rewrite assoc.
    eapply pathscomp0;
      [apply cancel_postcomposition, (! (nat_trans_ax (η T) _ _ f))|]; simpl.
    rewrite <- assoc.
    eapply pathscomp0; [apply maponpaths, Monad_law1|].
    apply id_right.

  Lemma bind_η {a : C} : bind (η T a) = identity (T a).
  Show proof.
    apply Monad_law2.

  Lemma bind_bind {a b c : C} (f : Ca,T b) (g : Cb,T c) :
    bind f · bind g = bind (f · bind g).
  Show proof.
    unfold bind; rewrite <- assoc.
    eapply pathscomp0; [apply maponpaths; rewrite assoc;
                        apply cancel_postcomposition, (!nat_trans_ax (μ T) _ _ g)|].
    rewrite !functor_comp, <- !assoc.
    now apply maponpaths, maponpaths, (!Monad_law3 c).

End bind.

Operations for monads based on binary coproducts

Section MonadsUsingCoproducts.

  Context {C : category} (T : Monad C) (BC : BinCoproducts C).

  Local Notation "a ⊕ b" := (BinCoproductObject (BC a b)).

operation of weakening in a monad
  Definition mweak (a b : C): CT b, T (a b) := bind (BinCoproductIn2 (BC _ _) · (η T _)).

operation of exchange in a monad
  Definition mexch (a b c : C): CT (a (b c)), T (b (a c)).
  Show proof.
    set (a1 := BinCoproductIn1 (BC _ _) · BinCoproductIn2 (BC _ _): Ca, b (a c)).
    set (a21 := BinCoproductIn1 (BC _ _): Cb, b (a c)).
    set (a22 := BinCoproductIn2 (BC _ _) · BinCoproductIn2 (BC _ _): Cc, b (a c)).
    exact (bind ((BinCoproductArrow _ a1 (BinCoproductArrow _ a21 a22)) · (η T _))).

Substitution operation for monads

  Section MonadSubst.

    Definition monadSubstGen {b:C} (a : C) (e : Cb,T a) : CT (b a), T a :=
      bind (BinCoproductArrow _ e (η T a)).

    Lemma subst_interchange_law_gen (c b a : C) (e : Cc,T (b a)) (f : Cb,T a):
      (monadSubstGen _ e) · (monadSubstGen _ f) =
        (mexch c b a) · (monadSubstGen _ (f · (mweak c a)))
          · (monadSubstGen _ (e · (monadSubstGen _ f))).
    Show proof.
      unfold monadSubstGen, mexch.
      do 3 rewrite bind_bind.
      apply maponpaths.
      apply BinCoproductArrowsEq.
      + do 4 rewrite assoc.
        do 2 rewrite BinCoproductIn1Commutes.
        rewrite <- assoc.
        rewrite bind_bind.
        rewrite <- assoc.
        rewrite (η_bind(a:=let (pr1, _) := pr1 (BC b (c a)) in pr1)).
        rewrite <- assoc.
        apply pathsinv0.
        eapply pathscomp0.
        * apply cancel_precomposition.
          rewrite assoc.
          rewrite BinCoproductIn2Commutes.
          rewrite (η_bind(a:=(c a))).
          apply idpath.
        * now rewrite BinCoproductIn1Commutes.
      + rewrite assoc.
        rewrite BinCoproductIn2Commutes.
        rewrite (η_bind(a:=b a)).
        do 3 rewrite assoc.
        rewrite BinCoproductIn2Commutes.
        apply BinCoproductArrowsEq.
        * rewrite BinCoproductIn1Commutes.
          rewrite <- assoc.
          rewrite bind_bind.
          do 2 rewrite assoc.
          rewrite BinCoproductIn1Commutes.
          rewrite <- assoc.
          rewrite (η_bind(a:=let (pr1, _) := pr1 (BC b (c a)) in pr1)).
          rewrite assoc.
          rewrite BinCoproductIn1Commutes.
          unfold mweak.
          rewrite <- assoc.
          rewrite bind_bind.
          apply pathsinv0.
          apply remove_id_right; try now idtac.
          rewrite <- bind_η.
          apply maponpaths.
          rewrite <- assoc.
          rewrite (η_bind(a:=let (pr1, _) := pr1 (BC c a) in pr1)).
          now rewrite BinCoproductIn2Commutes.
        * rewrite BinCoproductIn2Commutes.
          rewrite <- assoc.
          rewrite bind_bind.
          do 2 rewrite assoc.
          rewrite BinCoproductIn2Commutes.
          do 2 rewrite <- assoc.
          rewrite (η_bind(a:=let (pr1, _) := pr1 (BC b (c a)) in pr1)).
          apply pathsinv0.
          eapply pathscomp0.
      - apply cancel_precomposition.
        rewrite assoc.
        rewrite BinCoproductIn2Commutes.
        rewrite (η_bind(a:=(c a))).
        apply idpath.
      - now rewrite BinCoproductIn2Commutes.

    Context (TC : Terminal C).

    Local Notation "1" := TC.

    Definition monadSubst (a : C) (e : C1,T a) : CT (1 a), T a :=
      monadSubstGen a e.

    Lemma subst_interchange_law (a : C) (e : C1,T (1 a)) (f : C1,T a):
      (monadSubst _ e) · (monadSubst _ f) =
        (mexch 1 1 a) · (monadSubst _ (f · (mweak 1 a)))
          · (monadSubst _ (e · (monadSubst _ f))).
    Show proof.
      apply subst_interchange_law_gen.

  End MonadSubst.

End MonadsUsingCoproducts.

Helper lemma for showing two monads are equal

Section Monad_eq_helper.

Alternate (equivalent) definition of Monad

  Section Monad'_def.

    Definition raw_Monad_data (C : category) : UU :=
       F : C -> C, ((( a b : ob C, a --> b -> F a --> F b) ×
                      ( a : ob C, F (F a) --> F a)) ×
                     ( a : ob C, a --> F a)).

    #[reversible] Coercion functor_data_from_raw_Monad_data {C : category} (T : raw_Monad_data C) :
      functor_data C C := make_functor_data (pr1 T) (pr1 (pr1 (pr2 T))).

    Definition Monad'_data_laws {C : category} (T : raw_Monad_data C) :=
      ((is_functor T) ×
       (is_nat_trans (functor_composite_data T T) T (pr2 (pr1 (pr2 T))))) ×
      (is_nat_trans (functor_identity C) T (pr2 (pr2 T))).

    Definition Monad'_data (C : category) := (T : raw_Monad_data C), Monad'_data_laws T.

    Definition Monad'_data_to_Monad_data {C : category} (T : Monad'_data C) : disp_Monad_data (_,, pr1 (pr1 (pr2 T))) :=
      ((pr2 (pr1 (pr2 (pr1 T))),, (pr2 (pr1 (pr2 T))))),,
       (pr2 (pr2 (pr1 T)),, (pr2 (pr2 T))).

    Definition Monad' (C : category) := (T : Monad'_data C),
                                             (disp_Monad_laws (Monad'_data_to_Monad_data T)).
  End Monad'_def.

Equivalence of Monad and Monad'

  Section Monad_Monad'_equiv.
    Definition Monad'_to_Monad {C : category} (T : Monad' C) : Monad C :=
      (_,,(Monad'_data_to_Monad_data (pr1 T),, pr2 T)).

    Definition Monad_to_raw_data {C : category} (T : Monad C) : raw_Monad_data C.
    Show proof.
      use tpair.
      - exact (functor_on_objects T).
      - use tpair.
        + use tpair.
          * exact (@functor_on_morphisms C C T).
          * exact (μ T).
        + exact (η T).

    Definition Monad_to_Monad'_data {C : category} (T : Monad C) : Monad'_data C :=
      (Monad_to_raw_data T,, ((pr2 (T : functor C C),, (pr2 (μ T))),, pr2 (η T))).

    Definition Monad_to_Monad' {C : category} (T : Monad C) : Monad' C :=
      (Monad_to_Monad'_data T,, pr22 T).

    Definition Monad'_to_Monad_to_Monad' {C : category} (T : Monad' C) :
      Monad_to_Monad' (Monad'_to_Monad T) = T := (idpath T).

    Definition Monad_to_Monad'_to_Monad {C : category} (T : Monad C) :
      Monad'_to_Monad (Monad_to_Monad' T) = T := (idpath T).

  End Monad_Monad'_equiv.

  Lemma Monad'_eq_raw_data (C : category) (T T' : Monad' C) :
    pr1 (pr1 T) = pr1 (pr1 T') -> T = T'.
  Show proof.
    intro e.
    apply subtypePath.
    - intro. now apply isaprop_disp_Monad_laws.
    - apply subtypePath.
      + intro. apply isapropdirprod.
        * apply isapropdirprod.
          -- apply (isaprop_is_functor C C), homset_property.
          -- apply (isaprop_is_nat_trans C C), homset_property.
        * apply (isaprop_is_nat_trans C C), homset_property.
      + apply e.

  Lemma Monad_eq_raw_data (C : category) (T T' : Monad C) :
    Monad_to_raw_data T = Monad_to_raw_data T' -> T = T'.
  Show proof.
    intro e.
    apply (invmaponpathsweq (_,, (isweq_iso _ _ (@Monad_to_Monad'_to_Monad C)
                                             (@Monad'_to_Monad_to_Monad' C)))).
    now apply (Monad'_eq_raw_data C).

End Monad_eq_helper.

Section Monads_from_adjunctions.

  Definition functor_from_adjunction {C D : category}
    {L : functor C D} {R : functor D C} (H : are_adjoints L R) : functor C C := LR.

  Definition Monad_data_from_adjunction {C D : category} {L : functor C D}
    {R : functor D C} (H : are_adjoints L R) : disp_Monad_data (functor_from_adjunction H).
  Show proof.
    use tpair.
    - exact (pre_whisker L (post_whisker (adjcounit H) R)).
    - exact (adjunit H).

  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).
  Show 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))).

  Definition Monad_from_adjunction {C D : category} {L : functor C D}
    {R : functor D C} (H : are_adjoints L R) : Monad C.
  Show proof.

End Monads_from_adjunctions.