Library UniMath.SubstitutionSystems.MonadsFromSubstitutionSystems

**********************************************************
Benedikt Ahrens, Ralph Matthes
SubstitutionSystems
2015
**********************************************************
Contents :
  • Construction of a monad from a substitution system
  • Proof that morphism of hss gives morphism of monads
  • Bundling that into a functor
  • Proof that the functor is faithful

Unset Kernel Term Sharing.

Require Import UniMath.Foundations.PartD.

Require Import UniMath.MoreFoundations.Tactics.

Require Import UniMath.CategoryTheory.Categories.
Require Import UniMath.CategoryTheory.functor_categories.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Monads.Monads.
Require Import UniMath.CategoryTheory.FunctorAlgebras.
Require Import UniMath.CategoryTheory.limits.bincoproducts.
Require Import UniMath.CategoryTheory.PointedFunctors.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.HorizontalComposition.
Require Import UniMath.CategoryTheory.PointedFunctorsComposition.
Require Import UniMath.CategoryTheory.EndofunctorsMonoidal.

Local Open Scope cat.

Require Import UniMath.SubstitutionSystems.Signatures.
Require Import UniMath.SubstitutionSystems.SubstitutionSystems.
Require Import UniMath.SubstitutionSystems.Notation.
Local Open Scope subsys.

Section monad_from_hss.

Some variables and assumptions

Assume having a precategory C whose hom-types are sets
Variable C : precategory.
Variable hs : has_homsets C.

Variable CP : BinCoproducts C.

Local Notation "'EndC'":= ([C, C, hs]) .
Let hsEndC : has_homsets EndC := functor_category_has_homsets C C hs.
Let CPEndC : BinCoproducts EndC := BinCoproducts_functor_precat _ _ CP hs.

Variable H : Signature C hs C hs.

Let θ := theta H.

Let θ_strength1_int := Sig_strength_law1 _ _ _ _ H.
Let θ_strength2_int := Sig_strength_law2 _ _ _ _ H.

Let Id_H
: functor EndC EndC
  := BinCoproduct_of_functors _ _ CPEndC
                       (constant_functor _ _ (functor_identity _ : EndC))
                       H.

The precategory of pointed endofunctors on C
Local Notation "'Ptd'" := (precategory_Ptd C hs).
The category of endofunctors on C
Local Notation "'EndC'":= ([C, C, hs]) .
The product of two precategories

Definition of algebra structure τ of a pointed functor

Derivation of the monad laws from a heterogeneous substitution system


Section mu_from_fbracket.

We assume given a hss T

Variable T : hss CP H.

Local Notation "'p' T" := (ptd_from_alg T) (at level 3).
Local Notation "f ⊕ g" := (BinCoproductOfArrows _ (CPEndC _ _ ) (CPEndC _ _ ) f g).

Definition μ_0 : functor_identity C ⟹ functor_data_from_functor _ _ `T := η T.
Definition μ_0_ptd : id_Ptd C hs --> p T.
Proof.
  ∃ μ_0.
  intro c. simpl. apply id_left.
Defined.

Definition μ_1 : functor_composite (U (id_Ptd C hs)) (`T) ⟹ functor_data_from_functor _ _ `T
  := fbracket _ μ_0_ptd.

Lemma μ_1_identity : μ_1 = identity `T .
Proof.
  apply pathsinv0.
  apply fbracket_unique.
  split.
  - apply nat_trans_eq; try assumption.
    intros; simpl.
    rewrite id_right.
    apply idpath.
  - apply nat_trans_eq; try assumption.
    intro c. simpl.
    rewrite id_right.
    assert (H':= θ_Strength1_int_implies_θ_Strength1 _ _ _ _ _ _ θ_strength1_int).
    red in H'. simpl in H'.
    assert (H2 := H' (`T)).
    assert (H3 := nat_trans_eq_pointwise H2 c).
    simpl in ×.
    intermediate_path (identity _ · pr1 (τ T) c).
    + apply cancel_postcomposition. apply H3.
    + apply id_left.
Qed.

Lemma μ_1_identity' : ∏ c : C, μ_1 c = identity _.
Proof.
  intros c.
  assert (HA:= nat_trans_eq_pointwise μ_1_identity).
  apply HA.
Qed.




This is the multiplication of the monad to be constructed

Definition μ_2 : functor_composite (`T) (`T) ⟹ pr1 (`T)
  := fbracket T (identity _ ).

Definition functor_with_mu_from_hss : functor_with_μ C.
Proof.
  ∃ (`T).
  exact μ_2.
Defined.

Definition Monad_data_from_hss : Monad_data C.
Proof.
  ∃ functor_with_mu_from_hss.
  exact μ_0.
Defined.

Proof of the first monad law


Lemma Monad_law_1_from_hss :
  ∏ c : C, μ_0 (pr1 (`T) c)· μ_2 c = identity ((pr1 (`T)) c).
Proof.
  intro c.
  unfold μ_2. simpl.
  unfold μ_0. simpl.
  set (H':=fbracket_η T (identity _) ).
  set (H2:= nat_trans_eq_weq hs _ _ H').
  simpl in H2.
  apply pathsinv0.
  apply H2.
Qed.

Proof of the second monad law


Lemma Monad_law_2_from_hss:
  ∏ c : C, # (pr1 (`T)) (μ_0 c)· μ_2 c = identity ((pr1 (`T)) c).
Proof.
  intro c.
  intermediate_path (μ_1 c).
  - unfold μ_1.
    assert (H':= @fbracket_unique_target_pointwise _ _ _ _ T).
    assert (H1:= H' _ μ_0_ptd).
    set (x:= post_whisker μ_0 (`T)
             : EndC ⟦ `T • functor_identity _ , `T • `T ⟧).
    set (x':= x · μ_2).
    assert (H2 := H1 x').
    apply H2; clear H2.
    unfold x'. clear x'.
    unfold x; clear x.
    clear H1. clear H'. clear c.
    split.
    + apply nat_trans_eq; try apply hs.
      intro c.
      assert (H':=nat_trans_ax (η T)).
      simpl in H'.
      rewrite assoc.
      cbn.
      rewrite <- H'; clear H'.
      assert (H':= fbracket_η T (identity _ )).
      unfold μ_2.
      assert (H2 := nat_trans_eq_weq hs _ _ H').
      simpl in H2.
      rewrite <- assoc.
      rewrite <- H2.
      apply pathsinv0. apply id_right.     + rewrite functor_comp.
      apply nat_trans_eq; try assumption.
      intro c.
      rewrite <- horcomp_id_postwhisker.
      do 2 rewrite assoc.
      simpl in ×.
      intermediate_path ( # (pr1 (H ( (` T)))) (μ_0 c)· pr1 (θ ((`T) ⊗ (p T))) c ·
                  pr1 (# H μ_2) c · pr1 (τ T) c).
      × unfold tau_from_alg; cbn.
        do 2 rewrite assoc.
        apply cancel_postcomposition.
        apply cancel_postcomposition.
        apply cancel_postcomposition.
        assert (H':=θ_nat_2 _ _ _ _ H θ).
        assert (H2 := H' (`T) _ _ μ_0_ptd); clear H'.
        assert (H3:= nat_trans_eq_weq hs _ _ H2 c); clear H2.
        simpl in H3.
        rewrite id_left in H3.
        apply (!H3).       × assert (H':= fbracket_τ T (identity _ )).
        unfold μ_2.
        simpl.
        assert (H2:= nat_trans_eq_weq hs _ _ H' c); clear H'.
        simpl in ×.
        do 2 rewrite <- assoc.
        {
          intermediate_path ( # (pr1 (H (` T))) (μ_0 c)·
                       (pr1 (τ T) (pr1 (`T) c)· pr1 (fbracket T (identity (p T))) c)).
          - apply maponpaths.
            rewrite assoc.
            apply H2; clear H2.           - clear H2.
            do 2 rewrite assoc.
            apply cancel_postcomposition.
            eapply pathscomp0.
            apply (nat_trans_ax (τ T) ).
            apply cancel_postcomposition.
            apply pathsinv0.
            apply id_right.
        }
  - apply μ_1_identity'.
Qed.

T_squared is T∙T, η∙η, that is, the selfcomposition of T as a pointed functor

Definition T_squared : Ptd.
Proof.
  exact (ptd_composite _ _ (p T) (p T)).
Defined.

μ_2 is not just a natural transformation from T∙T to T, but also compatible with the pointed structure given by η

Lemma μ_2_is_ptd_mor :
  ∏ c : C, (ptd_pt C T_squared) c· μ_2 c = pr1 (η T) c.
Proof.
  intro c.
  unfold μ_2.
  unfold T_squared. simpl.
  assert (H':=Monad_law_2_from_hss c).
  simpl in H'.
  intermediate_path (pr1 (η T) c · identity _ ).
  - unfold eta_from_alg; simpl.
    repeat rewrite <- assoc.
    apply maponpaths.
    apply maponpaths.
    apply H'.
  - apply id_right.
Qed.

Definition μ_2_ptd : T_squared --> p T.
Proof.
  ∃ μ_2.
  unfold is_ptd_mor.
  apply μ_2_is_ptd_mor.
Defined.

Definition μ_3 : EndC ⟦ U T_squared • `T, `T⟧ := fbracket T μ_2_ptd.


Proof of the third monad law via transitivity

We show that both sides are equal to μ_3 = fbracket μ_2

Lemma μ_3_T_μ_2_μ_2 : μ_3 =
                      (`T ∘ μ_2 : EndC ⟦ `T • _ , `T • `T ⟧ ) · μ_2.
Proof.
  apply pathsinv0.
  apply (fbracket_unique T μ_2_ptd).
  split.
  - apply nat_trans_eq; try assumption.
    intro c.
    assert (H2 := nat_trans_ax (η T)); simpl in H2.
    rewrite assoc.
    simpl; rewrite <- H2 ; clear H2.
    intermediate_path (μ_2 c · identity _ ).
    + apply pathsinv0, id_right.
    + eapply pathscomp0. 2: apply assoc.
      apply pathsinv0.
      apply maponpaths. apply Monad_law_1_from_hss.
  - rewrite functor_comp.
    assert (H1 := θ_nat_2 _ _ _ _ H θ (`T) _ _ μ_2_ptd).
    simpl in H1.
    repeat rewrite assoc.
    match goal with |[H1 : ?g = _ |- _ · _ · ?f · ?h = _ ] ⇒
         intermediate_path (g · f · h) end.
    + apply cancel_postcomposition.
      apply cancel_postcomposition.
      apply pathsinv0.
      eapply pathscomp0. apply H1; clear H1.
      apply maponpaths.
      apply maponpaths.
      assert (H3:=horcomp_id_postwhisker).
      assert (H4 := H3 _ _ _ hs hs _ _ μ_2 (`T)); clear H3.
      apply H4.
    + clear H1.
      apply nat_trans_eq; try assumption.
      intro c; simpl.
      rewrite id_left.
      assert (H2 := fbracket_τ T (identity _ )).
      assert (H3:= nat_trans_eq_pointwise H2 c); clear H2.
      simpl in ×.
      match goal with |[H3 : _ = ?f |- ?e · _ · _ · _ = _ ] ⇒
         intermediate_path (e · f) end.
      × eapply pathscomp0. apply (!assoc _ _ _).
        eapply pathscomp0. apply (!assoc _ _ _ ).
        apply maponpaths.
        eapply pathscomp0. 2: apply H3.
        apply assoc.
      × clear H3.
        repeat rewrite assoc.
        apply cancel_postcomposition.
        assert (H1 := nat_trans_ax (τ T )).
        unfold tau_from_alg in H1.
        eapply pathscomp0; [ | apply H1]; clear H1.
        apply pathsinv0, assoc.
Qed.

Local Notation "'T•T²'" := (functor_compose hs hs (functor_composite (`T) (`T)) (`T) : [C, C, hs]).

Local Notation "'T²∙T'" := (@functor_composite C C C
                    (@functor_composite C C C (`T)
                                              (` T))
                    (` T) : functor C C).
Lemma μ_3_μ_2_T_μ_2 : (
    @compose (functor_precategory C C hs)
                  T²∙T _ _
                 
          ((μ_2 •• `T)
                   ) μ_2 :
             T•T² --> `T) = μ_3.
Proof.
  apply (fbracket_unique T μ_2_ptd).
  split.
  - apply nat_trans_eq; try assumption; intro c.
    simpl.
    transitivity (identity _ · μ_2 c).
    + apply pathsinv0, id_left.
    + eapply pathscomp0; [ | apply (!assoc _ _ _ ) ].
      apply cancel_postcomposition.
      assert (H1 := Monad_law_1_from_hss (pr1 (`T) c)).
      apply (!H1).
  - set (B:= τ T).
    match goal with | [|- _ · # ?H (?f · _ ) · _ = _ ] ⇒ set (F:=f : T•T² --> _ ) end.
    assert (H3:= functor_comp H F μ_2).
    unfold functor_compose in H3.
    eapply pathscomp0. apply cancel_postcomposition. apply maponpaths. apply H3.
    clear H3.
    apply nat_trans_eq; try assumption.
    intro c.
    simpl.
    match goal with | [ |- ?a · _ · _ = _ ] ⇒ set (Ac:= a) end.
    simpl in Ac.
    unfold θ_target_ob in ×.
    simpl in ×.
    unfold functor_compose in ×.
    assert (HX:=θ_nat_1 _ _ _ _ H θ _ _ μ_2).     assert (HX1:= HX (ptd_from_alg T)); clear HX.
    simpl in HX1.
    assert (HXX:=nat_trans_eq_pointwise HX1 c); clear HX1.
    simpl in HXX.
    rewrite (functor_id ( H (`T))) in HXX.
    rewrite id_right in HXX.     match goal with |[HXX : ?f · ?h = _ · _ |- _ · (_ · ?x ) · ?y = _ ] ⇒
      intermediate_path (pr1 (θ ((`T) ⊗ (ptd_from_alg T))) (pr1 (pr1 (pr1 T)) c)·
                       f · h · x· y) end.
    × repeat rewrite assoc.
      apply cancel_postcomposition.
      apply cancel_postcomposition.
      apply cancel_postcomposition.
      unfold Ac. clear Ac.
      eapply pathscomp0. 2: apply assoc.
      eapply pathscomp0.
      2: { apply maponpaths. apply (!HXX). }
      clear HXX.
      assert (Strength_2 : ∏ α : functor_compose hs hs (functor_composite (`T) (`T))(`T) --> functor_composite (` T) (`T),

                    pr1 (θ (`T ⊗ T_squared)) c · pr1 (# H α) c =
                     pr1 (θ ((`T) ⊗ (ptd_from_alg T))) ((pr1 (pr1 (pr1 T))) c)·
                     pr1 (θ (( ((`T) • (`T) : [_, _, hs])) ⊗ (ptd_from_alg T))) c·
                     pr1 (# H (α : functor_compose hs hs (`T) (functor_composite (`T) (` T))--> _)) c ).
      { (intro α;
          assert (HA := θ_Strength2_int_implies_θ_Strength2 _ _ _ _ _ _ θ_strength2_int);
          assert (HA':= HA (`T) (ptd_from_alg T) (ptd_from_alg T) _ α); clear HA;
          assert (HA2 := nat_trans_eq_pointwise HA' c ); clear HA';
          simpl in HA2; apply HA2 ).
      }
      eapply pathscomp0. apply (Strength_2 F).
      clear Strength_2.
      eapply pathscomp0. apply (!assoc _ _ _).
      apply maponpaths.
      apply maponpaths.
      match goal with |[ |- _ = ?pr1 (# ?G ?g) _ ] ⇒
              assert (X : F = g) end.
      { apply nat_trans_eq. assumption.
        intros. unfold F.
        simpl.
        rewrite functor_id.
        apply pathsinv0, id_right.
      }
      apply (maponpaths (λ T, pr1 (# H T) c)).
      apply X.
    × clear HXX. clear Ac. clear F. clear B.
      assert (H4 := fbracket_τ T (identity _ )).
      assert (H5:= nat_trans_eq_pointwise H4 c); clear H4.
      simpl in H5.
      unfold μ_2.
      {
        match goal with |[ H5 : _ = ?e |- ?a · ?b · _ · _ · _ = _ ] ⇒
                         intermediate_path (a · b · e) end.
        - repeat rewrite <- assoc.
          apply maponpaths.
          apply maponpaths.
          repeat rewrite <- assoc in H5. apply H5.
        - clear H5.
          repeat rewrite assoc.
          apply cancel_postcomposition.
          assert (HT := fbracket_τ T (identity _ )).
          assert (H6:= nat_trans_eq_pointwise HT); clear HT.
          unfold coproduct_nat_trans_in2_data.
          unfold tau_from_alg in H6.
          rewrite assoc in H6.
          apply H6.
      }
Qed.

proving a variant of the third monad law with assoc iso explicitly inserted

Section third_monad_law_with_assoc.

Lemma third_monad_law_from_hss :
  (`T ∘ μ_2 : EndC ⟦ functor_composite (functor_composite `T `T) `T , `T • `T ⟧) · μ_2
  =
  (α_functor _ _ _ : functor_compose hs hs _ _ --> _) · (μ_2 •• `T) · μ_2.
Proof.
  intermediate_path μ_3; [apply pathsinv0, μ_3_T_μ_2_μ_2 | ].
  apply pathsinv0.
  apply (fbracket_unique T μ_2_ptd).
  split.
  - apply nat_trans_eq; try assumption; intro c.
    simpl.
    rewrite assoc.
    intermediate_path (identity _ · μ_2 c).
    + apply pathsinv0, id_left.
    + apply cancel_postcomposition.
      rewrite id_left.
      assert (H1 := Monad_law_1_from_hss (pr1 (`T) c)).
      simpl in H1.
      apply (!H1).
  - rewrite functor_comp.
    rewrite functor_comp.
    rewrite assoc.
    rewrite assoc.
    rewrite assoc.
    rewrite assoc.
    unfold T_squared.
    apply nat_trans_eq; try assumption.
    intro x; simpl.
    assert (HTT := θ_strength2_int).
    assert (HX := HTT (`T) (ptd_from_alg T) (ptd_from_alg T)); clear HTT.
    assert (HX':= nat_trans_eq_pointwise HX x); clear HX.
    simpl in HX'.
    match goal with | [ H : _ = ?f |- _ · _ · ?g · ?h · ?i = _ ] ⇒
                      intermediate_path (f · g · h · i) end.
    + apply cancel_postcomposition.
      apply cancel_postcomposition.
      apply cancel_postcomposition.
      apply HX'.
    + clear HX'.
      rewrite id_left.
      rewrite id_right.
      assert (HX:=θ_nat_1 _ _ _ _ H θ _ _ μ_2).
      assert (HX1:= HX (ptd_from_alg T)); clear HX.
      simpl in HX1.
      assert (HXX:=nat_trans_eq_pointwise HX1 x); clear HX1.
      simpl in HXX.
      match goal with | [ H : ?x = _ |- ?e · _ · _ · ?f · ?g = _ ] ⇒
                 intermediate_path (e · x · f · g) end.
      × apply cancel_postcomposition.
        apply cancel_postcomposition.
        repeat rewrite <- assoc.
        apply maponpaths.
        {
          match goal with | [ H : _ = ?x |- _ ] ⇒ intermediate_path x end.
          - clear HXX.
             apply maponpaths.
             match goal with | [ |- _ ?a ?x = _ ?b ?y ] ⇒ assert (TTT : a = b) end.
             {
               match goal with | [ |- _ ?a = _ ?b ] ⇒ assert (TTTT : a = b) end.
               { apply nat_trans_eq; try assumption.
                 intros. simpl. rewrite functor_id. apply pathsinv0, id_right.
               }
               apply maponpaths. apply TTTT.
             }
             apply (nat_trans_eq_pointwise TTT).
          - repeat rewrite assoc.
            repeat rewrite assoc in HXX.
            apply (!HXX).
         }
      × clear HXX.
        assert (H4 := fbracket_τ T (identity _ )).
        assert (H5:= nat_trans_eq_pointwise H4 x); clear H4.
        unfold μ_2.
        repeat rewrite <- assoc.
        simpl in H5; repeat rewrite <- assoc in H5.
        eapply pathscomp0. apply maponpaths. apply maponpaths. apply maponpaths. apply H5.
        clear H5.
        rewrite functor_id.
        rewrite id_left.
        repeat rewrite assoc.
        apply cancel_postcomposition.
        assert (H4':= fbracket_τ T (identity _ )).
        assert (H6:= nat_trans_eq_pointwise H4' (pr1 `T x)); clear H4'.
        simpl in H6.
        unfold coproduct_nat_trans_in2_data in H6. simpl in H6.
        rewrite assoc in H6.
        apply H6.
Qed.

End third_monad_law_with_assoc.

Unset Printing All.
Set Printing Notations.
Unset Printing Implicit.

Finally putting together all the preparatory results to obtain a monad

Lemma Monad_laws_from_hss : Monad_laws Monad_data_from_hss.
Proof.
  split.
  - unfold Monad_data_from_hss; simpl; split.
    + apply Monad_law_1_from_hss.
    + apply Monad_law_2_from_hss.

  - unfold Monad_data_from_hss; simpl.
    intro c.
    intermediate_path (pr1 μ_3 c).
    + set (H1 := μ_3_T_μ_2_μ_2).
      set (H2 := nat_trans_eq_weq hs _ _ H1).
      apply pathsinv0, H2.
    + set (H1 := μ_3_μ_2_T_μ_2).
      set (H2 := nat_trans_eq_weq hs _ _ H1).
      apply pathsinv0, H2.
Qed.

Definition Monad_from_hss : Monad C.
Proof.
  ∃ Monad_data_from_hss.
  exact Monad_laws_from_hss.
Defined.

End mu_from_fbracket.

A functor from hss to monads

Objects are considered above, now morphisms

Definition Monad_Mor_laws_from_hssMor (T T' : hss CP H)(β : hssMor T T')
  : Monad_Mor_laws (T:=Monad_from_hss T) (T':=Monad_from_hss T') (pr1 (pr1 β)).
Proof.
  repeat split; simpl.
  - intro c.
    unfold μ_2. simpl.
    set (H':=isbracketMor_hssMor _ _ _ _ β).
    unfold isbracketMor in H'.
    set (H2:= H' _ (identity _ )).
    set (H3:=(nat_trans_eq_weq hs _ _ H2)).
    rewrite id_left in H3.
    simpl in H3.
    rewrite H3; clear H3 H2 H'.
    rewrite compute_fbracket.
    rewrite <- assoc.
    apply maponpaths.
    apply cancel_postcomposition.
    apply idpath.
  - unfold μ_0.
    intro c.
    set (H':=ptd_mor_commutes _ (ptd_from_alg_mor _ _ _ _ β)).
    apply H'.
Qed.

Definition Monad_Mor_from_hssMor {T T' : hss CP H}(β : hssMor T T')
  : Monad_Mor (Monad_from_hss T) (Monad_from_hss T')
  := tpair _ _ (Monad_Mor_laws_from_hssMor T T' β).

Definition hss_to_monad_functor_data : functor_data (hss_precategory CP H) (precategory_Monad C hs).
Proof.
  ∃ Monad_from_hss.
  exact @Monad_Mor_from_hssMor.
Defined.

Lemma is_functor_hss_to_monad : is_functor hss_to_monad_functor_data.
Proof.
  split; simpl.
  - intro a.
    apply (invmap (Monad_Mor_equiv hs _ _ )).
    apply idpath.
  - intros a b c f g.
    apply (invmap (Monad_Mor_equiv hs _ _ )).
    apply idpath.
Qed.

Definition hss_to_monad_functor : functor _ _ := tpair _ _ is_functor_hss_to_monad.

Lemma isaset_Monad_Mor (T T' : Monad C) : isaset (Monad_Mor T T').
Proof.
  intros β β'.
  apply (isofhlevelweqb _ (Monad_Mor_equiv hs _ _)).
  apply isaset_nat_trans.
  apply hs.
Qed.

Definition hssMor_Monad_Mor_eq {T T' : hss CP H} (β β' : hssMor T T')
  : β = β' ≃ Monad_Mor_from_hssMor β = Monad_Mor_from_hssMor β'.
Proof.
  eapply weqcomp.
  - apply hssMor_eq.
  - apply invweq.
    apply Monad_Mor_equiv.
    apply hs.
Defined.

The functor from hss to monads is faithful, i.e. forgets at most structure


Lemma faithful_hss_to_monad : faithful hss_to_monad_functor.
Proof.
  unfold faithful.
  intros T T'.
  apply isinclbetweensets.
  - apply isaset_hssMor.
  - apply isaset_Monad_Mor.
  - intros β β'.
    apply (invmap (hssMor_Monad_Mor_eq _ _ )).
Qed.

End monad_from_hss.