UniMath.Bicategories.DisplayedBicats.Examples.Monads

Definition make_monad {C : bicat}
           (X : C)
           (f : C ⟦X ,X ⟧)
           (η : id₁ X ==> f)
           (μ : f · f ==> f)
           (ημ : linvunitor f • (η ▹ f ) • μ
                 =
                 id₂ f)
           (μη : rinvunitor f • (f ◃ η ) • μ
                 =
                 id₂ f)
           (μμ : (f ◃ μ ) • μ
                 =
                 lassociator f f f • (μ ▹ f ) • μ)
  : monad C X.
Proof.
  use tpair.
  - use tpair.
    + exact f.
    + split.
      × exact η.
      × exact μ.
  - repeat split.
    + exact ημ.
    + exact μη.
    + exact μμ.
Defined.

Definition make_monad_mor
           {C : bicat}
           {x y : C} {mx : monad C x} {my : monad C y}
           {f : x --> y}
           (mf_nat : invertible_2cell (monad_endo mx · f) (f · monad_endo my))
           (mfη : (monad_unit mx ▹ f ) • mf_nat
                     =
                     (lunitor f • rinvunitor f ) • (f ◃ monad_unit my ))
           (mfμ : (monad_mu mx ▹ _) • mf_nat
                  =
                  ((((rassociator _ _ _ • (_ ◃ mf_nat ))
                       • lassociator _ _ _) • (mf_nat ▹ _))
                     • rassociator _ _ _) • (_ ◃ monad_mu my ))
  : mx -->[f ] my.
Proof.
  refine (_,, tt).
  use tpair.
  - exact mf_nat.
  - apply make_dirprod.
    + exact mfη.
    + exact mfμ.
Defined.

Definition make_monad_cell
           {C : bicat} {x y : C} {mx : monad C x} {my : monad C y}
           {f g : x --> y} {α : f ==> g}
           {mf : mx -->[f ] my}
           {mg : mx -->[g ] my}
           (α_nat : (monad_endo mx ◃ α ) • monad_mor_natural mg
                    =
                    monad_mor_natural mf • (α ▹ monad_endo my ))
  : mf ==>[ α ] mg
  := ((α_nat ,, (tt ,,tt )),, tt).

Definition bigmonad (C : bicat) := total_bicat (monad C).

Definition base {C : bicat} (m : bigmonad C) : C := pr1 m.

Definition bigmonad_to_monad (C : bicat) (m : bigmonad C) : monad C (base m)
  := pr2 m.

Definition make_bigmonad {C : bicat}
           (X : C)
           (f : C ⟦X ,X ⟧)
           (η : id₁ X ==> f)
           (μ : f · f ==> f)
           (ημ : linvunitor f • (η ▹ f ) • μ
                 =
                 id₂ f)
           (μη : rinvunitor f • (f ◃ η ) • μ
                 =
                 id₂ f)
           (μμ : (f ◃ μ ) • μ
                 =
                 lassociator f f f • (μ ▹ f ) • μ)
  : bigmonad C.
Proof.
  use tpair.
  - exact X.
  - use make_monad.
    + exact f.
    + exact η.
    + exact μ.
    + exact ημ.
    + exact μη.
    + exact μμ.
Defined.

Definition monad_is_univalent_2_1
           (C : bicat)
  : disp_univalent_2_1 (monad_data C).
Proof.
  use sigma_disp_univalent_2_1_with_props.
  - apply disp_2cells_isaprop_alg.
  - apply disp_2cells_isaprop_prod ; apply disp_2cells_isaprop_add_cell.
  - apply disp_alg_bicat_univalent_2_1.
  - apply is_univalent_2_1_dirprod_bicat ; apply add_cell_disp_cat_univalent_2_1.
Defined.

Definition monad_is_univalent_2_0
           (C : bicat)
           (HC : is_univalent_2 C)
  : disp_univalent_2_0 (monad_data C).
Proof.
  use sigma_disp_univalent_2_0_with_props.
  - exact HC.
  - apply disp_2cells_isaprop_alg.
  - apply disp_2cells_isaprop_prod ; apply disp_2cells_isaprop_add_cell.
  - apply disp_alg_bicat_univalent_2_1.
  - apply is_univalent_2_1_dirprod_bicat ; apply add_cell_disp_cat_univalent_2_1.
  - apply disp_locally_groupoid_alg.
  - apply disp_locally_groupoid_prod ; apply disp_locally_groupoid_add_cell.
  - apply disp_alg_bicat_univalent_2_0.
    exact (pr2 HC).
  - apply is_univalent_2_0_dirprod_bicat.
    + apply total_is_univalent_2_1.
      × exact (pr2 HC).
      × apply disp_alg_bicat_univalent_2_1.
    + apply add_cell_disp_cat_univalent_2.
      × exact (pr2 HC).
      × apply disp_alg_bicat_univalent_2_1.
    + apply add_cell_disp_cat_univalent_2.
      × exact (pr2 HC).
      × apply disp_alg_bicat_univalent_2_1.
Defined.

Definition bigmonad_is_univalent_2_1
           (C : bicat)
           (HC_1 : is_univalent_2_1 C)
  : is_univalent_2_1 (bigmonad C).
Proof.
  apply sigma_is_univalent_2_1.
  - exact HC_1.
  - apply monad_is_univalent_2_1.
  - apply disp_fullsubbicat_univalent_2_1.
Defined.

Definition bigmonad_is_univalent_2_0
           (C : bicat)
           (HC : is_univalent_2 C)
  : is_univalent_2_0 (bigmonad C).
Proof.
  apply sigma_is_univalent_2_0.
  - exact HC.
  - split.
    + apply monad_is_univalent_2_0.
      exact HC.
    + apply monad_is_univalent_2_1.
  - split.
    + apply disp_univalent_2_0_fullsubbicat.
      × exact (lawless_monad_is_univalent_2 C HC).
      × intro ; simpl.
        repeat (apply isapropdirprod) ; apply C.
    + apply disp_fullsubbicat_univalent_2_1.
Defined.

Definition bigmonad_is_univalent_2
           (C : bicat)
           (HC : is_univalent_2 C)
  : is_univalent_2 (bigmonad C).
Proof.
  split.
  - apply bigmonad_is_univalent_2_0; assumption.
  - apply bigmonad_is_univalent_2_1.
    exact (pr2 HC).
Defined.

Definition disp_2cells_isaprop_monad
           (C : bicat)
           (HC : is_univalent_2 C)
  : disp_2cells_isaprop (monad C).
Proof.
  apply disp_2cells_isaprop_sigma.
  - apply disp_2cells_isaprop_sigma.
    + apply disp_2cells_isaprop_alg.
    + apply disp_2cells_isaprop_prod.
      × apply disp_2cells_isaprop_add_cell.
      × apply disp_2cells_isaprop_add_cell.
  - apply disp_2cells_isaprop_fullsubbicat.
Qed.

Definition disp_locally_groupoid_monad
           (C : bicat)
           (HC : is_univalent_2 C)
  : disp_locally_groupoid (monad C).
Proof.
  apply disp_locally_groupoid_sigma.
  - exact HC.
  - apply disp_2cells_isaprop_sigma.
    + apply disp_2cells_isaprop_alg.
    + apply disp_2cells_isaprop_prod.
      × apply disp_2cells_isaprop_add_cell.
      × apply disp_2cells_isaprop_add_cell.
  - apply disp_2cells_isaprop_fullsubbicat.
  - apply disp_locally_groupoid_sigma.
    + exact HC.
    + apply disp_2cells_isaprop_alg.
    + apply disp_2cells_isaprop_prod.
      × apply disp_2cells_isaprop_add_cell.
      × apply disp_2cells_isaprop_add_cell.
    + apply disp_locally_groupoid_alg.
    + apply disp_locally_groupoid_prod.
      × apply disp_locally_groupoid_add_cell.
      × apply disp_locally_groupoid_add_cell.
  - apply disp_locally_groupoid_fullsubbicat.
Qed.

Definition make_cat_monad
           (C : univalent_category)
           (M : C ⟶ C)
           (η : functor_identity C ⟹ M)
           (μ : M ∙ M ⟹ M)
           (lid : ∏ (X : C ), #M (η X) · μ X = id₁ (M X ))
           (rid : ∏ (X : C ), η (M X) · μ X = id₁ (M X ))
           (massoc : ∏ (X : C ), μ (M X) · μ X = #M (μ X) · μ X)
  : monad bicat_of_cats C.
Proof.
  use make_monad.
  - exact M.
  - exact η.
  - exact μ.
  - abstract
      (use nat_trans_eq; try apply homset_property;
       intros X ; cbn;
       rewrite id_left;
       apply lid).
  - abstract
      (use nat_trans_eq; try apply homset_property;
       intros X ; cbn;
       rewrite id_left;
       apply rid).
  - abstract
      (use nat_trans_eq; try apply homset_property;
       intros X ; cbn;
       rewrite id_left;
       apply massoc).
Defined.

Definition cat_monad_ημ {C : univalent_category} (M : monad bicat_of_cats C)
  : ∏ (X : C ), #(pr1(monad_endo M)) (pr1(monad_unit M) X) · pr1(monad_mu M) X = id₁ _.
Proof.
  intros X.
  pose (nat_trans_eq_pointwise (monad_ημ M) X) as p.
  cbn in p.
  rewrite id_left in p.
  exact p.
Qed.

Definition cat_monad_μη {C : univalent_category} (M : monad bicat_of_cats C)
  : ∏ (X : C ), pr1(monad_unit M) (pr1(monad_endo M) X) · pr1(monad_mu M) X = id₁ _.
Proof.
  intros X.
  pose (nat_trans_eq_pointwise (monad_μη M) X) as p.
  cbn in p.
  rewrite id_left in p.
  exact p.
Qed.

Definition cat_monad_μμ {C : univalent_category} (M : monad bicat_of_cats C)
  : ∏ (X : C ),
    pr1(monad_mu M) (pr1(monad_endo M) X) · pr1(monad_mu M) X
    =
    #(pr1(monad_endo M)) (pr1(monad_mu M) X) · pr1(monad_mu M) X.
Proof.
  intros X.
  pose (nat_trans_eq_pointwise (monad_μμ M) X) as p.
  cbn in p.
  rewrite id_left in p.
  exact p.
Qed.

Section Bind.

Context {C : univalent_category}
        (M : monad bicat_of_cats C).

Definition monad_bind
           {A B : C}
           (f : C ⟦A , (monad_endo M : _ ⟶ _) B ⟧)
  : C ⟦(monad_endo M : _ ⟶ _) A , (monad_endo M : _ ⟶ _) B ⟧
  := #(monad_endo M : _ ⟶ _) f · pr1 (monad_mu M) B.

Definition cat_monad_map_as_bind
           {x y : pr1 C}
           (f : x --> y)
  : #(monad_endo M : _ ⟶ _) f = monad_bind (f · pr1 (monad_unit M) y).
Proof.
  unfold monad_bind.
  refine (!_).
  etrans.
  {
    apply maponpaths_2.
    apply functor_comp.
  }
  rewrite assoc'.
  etrans.
  {
    apply maponpaths.
    apply cat_monad_ημ.
  }
  apply id_right.
Qed.

Lemma cat_monad_bind_unit
      {A B : C}
      (f : C ⟦A , (monad_endo M : _ ⟶ _) B ⟧)
  : (monad_unit M : _ ⟹ _) A · monad_bind f = f.
Proof.
  unfold monad_bind.
  etrans.
  { rewrite assoc.
    apply maponpaths_2.
    apply (!(nat_trans_ax ((monad_unit M : _ ⟹ _)) A _ f)).
  }
  etrans.
  2: apply id_right.
  rewrite assoc'.
  apply maponpaths.
  apply (cat_monad_μη M).
Qed.

Lemma cat_monad_unit_bind
      {A : C}
  : monad_bind ((monad_unit M : _ ⟹ _) A) = id₁ _.
Proof.
  apply (cat_monad_ημ M).
Qed.

Lemma cat_monad_bind_bind
      {a b c : C}
      (f : C ⟦a , (monad_endo M : _ ⟶ _) b ⟧)
      (g : C ⟦b , (monad_endo M : _ ⟶ _) c ⟧)
  : monad_bind f · monad_bind g = monad_bind (f · monad_bind g).
Proof.
  unfold monad_bind.
  etrans.
  2: {
    rewrite (functor_comp (monad_endo M : _ ⟶ _)).
    rewrite assoc'.
    apply maponpaths.
    rewrite (functor_comp (monad_endo M : _ ⟶ _)).
    rewrite assoc'.
    apply maponpaths.
    apply (cat_monad_μμ M).
  }
  pose (nat_trans_ax ((monad_mu M : _ ⟹ _)) _ _ g) as Hμ.
  simpl in Hμ.
  rewrite assoc'.
  apply maponpaths.
  etrans.
  { rewrite assoc.
    apply maponpaths_2.
    apply (!Hμ).
  }
  rewrite assoc.
  apply idpath.
Qed.

End Bind.

Definition make_cat_monad_mor
           {C D : univalent_category}
           {mx : monad bicat_of_cats C} {my : monad bicat_of_cats D}
           {F : C ⟶ D}
           (mf_nat : nat_iso (monad_endo mx ∙ F) (F ∙ monad_endo my))
           (mfη : ∏ (X : C ), #F (pr1 (monad_unit mx) X) · mf_nat X
                             =
                             pr1 (monad_unit my) (F X))
           (mfμ : ∏ (X : C ),
                  # F (pr1 (monad_mu mx) X) · mf_nat X
                  =
                  mf_nat (pr1 (monad_endo mx) X)
                         · # (pr1 (monad_endo my)) (mf_nat X)
                         · pr1 (monad_mu my) (F X))
  : mx -->[F ] my.
Proof.
  use make_monad_mor.
  - apply nat_iso_to_invertible_2cell.
    exact mf_nat.
  - abstract
      (use nat_trans_eq; try apply homset_property;
       intros X ; cbn;
       do 2 rewrite id_left;
       apply mfη).
  - abstract
      (use nat_trans_eq; try apply homset_property;
       intros X ; cbn;
       rewrite id_left, !id_right;
       apply mfμ).
Defined.

Definition make_cat_monad_cell
           {C D : univalent_category}
           {mx : monad bicat_of_cats C}
           {my : monad bicat_of_cats D}
           {f g : C ⟶ D}
           {α : f ⟹ g}
           {mf : mx -->[f ] my}
           {mg : mx -->[g ] my}
           (H : ∏ (X : C ),
                α (pr1 (monad_endo mx) X) · (pr11 (monad_mor_natural mg )) X
                =
                (pr11 (monad_mor_natural mf )) X · # (pr1 (monad_endo my)) (pr1 α X))
  : mf ==>[α: prebicat_cells bicat_of_cats _ _] mg.
Proof.
  apply make_monad_cell.
  use nat_trans_eq; try apply homset_property.
  intros X; cbn.
  apply H.
Qed.

Definition monad_mor_nat_iso
           {C₁ C₂ : univalent_category}
           {F : C₁ ⟶ C₂}
           {M₁ : monad bicat_of_cats C₁}
           {M₂ : monad bicat_of_cats C₂}
           (FF : M₁ -->[F ] M₂)
  : nat_iso (monad_endo M₁ ∙ F) (F ∙ monad_endo M₂)
  := invertible_2cell_to_nat_iso _ _ (monad_mor_natural FF).

Definition monad_mor_natural_pointwise
           {C₁ C₂ : univalent_category}
           {F : C₁ ⟶ C₂}
           {M₁ : monad bicat_of_cats C₁}
           {M₂ : monad bicat_of_cats C₂}
           (FF : M₁ -->[F ] M₂)
           (X : C₁)
  : iso ((monad_endo M₂ : C₂ ⟶ C₂) (F X)) (F ((monad_endo M₁ : C₁ ⟶ C₁) X))
  := CompositesAndInverses.nat_iso_to_pointwise_iso
       (nat_iso_inv (monad_mor_nat_iso FF)) X.

Definition monad_mor_iso
           {C₁ C₂ : univalent_category}
           {F : C₁ ⟶ C₂}
           {M₁ : monad bicat_of_cats C₁}
           {M₂ : monad bicat_of_cats C₂}
           (FF : M₁ -->[F ] M₂)
  : ∏ X : C₁ , iso (F ((monad_endo M₁ : C₁ ⟶ C₁) X)) ((monad_endo M₂ : C₂ ⟶ C₂) (F X))
  := CompositesAndInverses.nat_iso_to_pointwise_iso (monad_mor_nat_iso FF).

Lemma monad_mor_bind
      {C₁ C₂ : univalent_category}
      {F : C₁ ⟶ C₂}
      {M₁ : monad bicat_of_cats C₁}
      {M₂ : monad bicat_of_cats C₂}
      (FF : M₁ -->[F ] M₂)
      {A B : C₁}
      (f : A --> (monad_endo M₁ : _ ⟶ _) B)
  : #F (monad_bind M₁ f) · monad_mor_iso FF B
    =
    monad_mor_iso FF A · monad_bind M₂ (# F f · pr1 (monad_mor_iso FF B)).
Proof.
  unfold monad_bind, monad_mor_iso.
  simpl.
  etrans.
  2: {
    rewrite assoc.
    apply maponpaths_2.
    rewrite (functor_comp (monad_endo M₂ : _ ⟶ _)).
    rewrite assoc.
    apply maponpaths_2.
    apply (nat_trans_ax (pr1 (monad_mor_natural FF)) _ _ f).
  }
  simpl.
  rewrite functor_comp.
  do 3 rewrite assoc'.
  apply maponpaths.
  etrans.
  { pose (nat_trans_eq_pointwise (monad_mor_mu FF) B) as H.
    simpl in H.
    rewrite id_left in H.
    do 2 rewrite id_right in H.
    apply H.
  }
  rewrite assoc'.
  apply idpath.
Qed.

Lemma monad_mor_bind_alt
      {C₁ C₂ : univalent_category}
      {F : C₁ ⟶ C₂}
      {M₁ : monad bicat_of_cats C₁}
      {M₂ : monad bicat_of_cats C₂}
      (FF : M₁ -->[F ] M₂)
      {A B : C₁}
      (f : A --> (monad_endo M₁ : _ ⟶ _) B)
  : #F (monad_bind M₁ f)
    =
    monad_mor_iso FF A
      · monad_bind M₂ (# F f · pr1 (monad_mor_iso FF B))
      · inv_from_iso (monad_mor_iso FF B).
Proof.
  use iso_inv_on_left.
  apply pathsinv0.
  apply monad_mor_bind.
Qed.

Library UniMath.Bicategories.DisplayedBicats.Examples.Monads