Library UniMath.ModelCategories.Generated.GenericFreeMonoidSequence

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.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Limits.Graphs.Coequalizers.
Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Chains.Chains.

Require Import UniMath.Combinatorics.StandardFiniteSets.

Require Import UniMath.CategoryTheory.Monoidal.Categories.
Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors.
Require Import UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids.

Require Import UniMath.ModelCategories.Generated.GenericFreeMonoid.
Require Import UniMath.ModelCategories.Generated.MonoidalHelpers.
Require Import UniMath.ModelCategories.Helpers.

Local Open Scope cat.

Section free_monoid_colim.

Import BifunctorNotations.
Import MonoidalNotations.

Context {C : category}.
Context (V : monoidal C).
Local Definition CMon : monoidal_cat := (_,, V).
Context (T : pointed V).

Context (CL : Chains C).
Context (CE : Coequalizers C).

              TXβ
                |
                | xβ
                v
  Xβ --------> Xβ1
     τXβ · xβ

Local Definition pair_diagram : UU :=
    ∑ (x0 x1 : C), (T ⊗_{V} x0 --> x1).

Local Definition pair_diagram_lob (X : pair_diagram) : C :=
    pr1 X.
Local Definition pair_diagram_rob (X : pair_diagram) : C :=
    pr12 X.
#[reversible] Coercion pair_diagram_arr (X : pair_diagram) :=
    pr22 X.

Local Definition pair_diagram_horizontal_arrow (X : pair_diagram) : (pair_diagram_lob X) --> (pair_diagram_rob X).
Show proof.

Definition next_pair_diagram_coeq_arr0 (xβ : pair_diagram) :
    T ⊗_{V} (pair_diagram_lob xβ) -->
        T ⊗_{V} (pair_diagram_rob xβ).
Show proof.

Definition next_pair_diagram_coeq_arr1 (xβ : pair_diagram) :
    T ⊗_{V} (pair_diagram_lob xβ) -->
        T ⊗_{V} (pair_diagram_rob xβ).
Show proof.

Definition next_pair_diagram_coeq (xβ : pair_diagram) :=
    CE _ _ (next_pair_diagram_coeq_arr0 xβ) (next_pair_diagram_coeq_arr1 xβ).

  TXβ-1 --> TXβ ----> TXβ1
    |        |         |
    |     xβ |         | xβ1
    v        v         v
    Xβ ----> Xβ1 ----> Xβ2
        fβ

Definition next_pair_diagram (xβ : pair_diagram) : pair_diagram.
Show proof.

Definition free_monoid_coeq_sequence_on (A : C) :
    nat -> pair_diagram.
Show proof.

Definition free_monoid_coeq_sequence_diagram_on (A : C) :
    chain C.
Show proof.

Definition rightwhisker_chain_with (P : CMon) (d : chain C) :
    chain C := mapchain (monoidal_right_tensor P) d.
Definition leftwhisker_chain_with (P : CMon) (d : chain C) :
    chain C := mapchain (monoidal_left_tensor P) d.

Definition free_monoid_coeq_sequence_colim_on (A : C) :
  ColimCocone (free_monoid_coeq_sequence_diagram_on A) :=
    CL _.

Local Definition free_monoid_coeq_sequence_colim_unit :=
    free_monoid_coeq_sequence_colim_on I_{V}.
Local Definition Tinf : pointed V.
Show proof.

Definition free_monoid_coeq_sequence_leftwhisker_colim_on (P A : C) :
    ColimCocone (leftwhisker_chain_with P (free_monoid_coeq_sequence_diagram_on A)) :=
        CL _.
Definition free_monoid_coeq_sequence_rightwhisker_colim_on (P A : C) :
    ColimCocone (rightwhisker_chain_with P (free_monoid_coeq_sequence_diagram_on A)) :=
        CL _.

Definition chain_shift_left (c : chain C) : chain C.
Show proof.

Definition chain_shift_left_base_cocone (c : chain C)
    (clmsh := colim (CL (chain_shift_left c))) :
  cocone c clmsh.
Show proof.

Definition chain_shift_left_shl_cocone (c : chain C)
    (clm := colim (CL c)) :
  cocone (chain_shift_left c) clm.
Show proof.

Definition chain_shift_left_fwd_cocone (c : chain C)
    {k : C} (cc : cocone c k) :
  cocone (chain_shift_left c) k.
Show proof.

Definition chain_shift_left_inv_cocone (c : chain C)
    {k : C} (cc : cocone (chain_shift_left c) k) :
  cocone c k.
Show proof.

Definition chain_shift_left_base_isColimCocone (c : chain C) :
    isColimCocone _ _ (chain_shift_left_base_cocone c).
Show proof.

Definition chain_shift_left_shl_colim_cocone (c : chain C)
    (clmsh := colim (CL (chain_shift_left c))) :
  ColimCocone c.
Show proof.


Definition chain_shift_left_colim_iso (c : chain C)
    (clm := colim (CL c))
    (clmls := colim (CL (chain_shift_left c))) :
  z_iso clm clmls.
Show proof.

Lemma colimσ_on_welldefined
    (A : C)
    (m : vertex nat_graph) :
  T ⊗^{ V}_{l} pair_diagram_horizontal_arrow (free_monoid_coeq_sequence_on A m)
  · next_pair_diagram (free_monoid_coeq_sequence_on A m) =
  free_monoid_coeq_sequence_on A m
  · pair_diagram_horizontal_arrow (next_pair_diagram (free_monoid_coeq_sequence_on A m)).
Show proof.

Definition colimσ_on (A : C) :
    colim (free_monoid_coeq_sequence_leftwhisker_colim_on T A) -->
      colim (CL (chain_shift_left (free_monoid_coeq_sequence_diagram_on A))).
Show proof.

Lemma can_colimArrow_forms_cocone (A : C) :
    forms_cocone
      (leftwhisker_chain_with T (free_monoid_coeq_sequence_diagram_on A))
      (λ n : nat, T ⊗^{ V}_{l} colimIn (free_monoid_coeq_sequence_colim_on A) n).
Show proof.

Local Definition can (A : C) :
    colim (free_monoid_coeq_sequence_leftwhisker_colim_on T A) --> T ⊗_{V} colim (free_monoid_coeq_sequence_colim_on A).
Show proof.

Local Definition top (A : C) :
    colim (free_monoid_coeq_sequence_leftwhisker_colim_on T A) --> T ⊗_{V} colim (free_monoid_coeq_sequence_colim_on A).
Show proof.

Local Definition free_monoid_coeq_sequence_limit_step_coeq (A : C) :=
    CE _ _ (can A) (top A).

Definition free_monoid_coeq_sequence_limit_ordinal_step_on (A : C) :
    pair_diagram.
Show proof.

Definition free_monoid_coeq_sequence_converges_on (A : C) :=
    is_z_isomorphism (
      pair_diagram_horizontal_arrow
        (free_monoid_coeq_sequence_limit_ordinal_step_on A)
    ).

Section Convergence.

Definition T_preserves_diagram_on (A : C) : UU :=
  preserves_colimit
    (monoidal_left_tensor (T : CMon))
    (free_monoid_coeq_sequence_diagram_on A)
    _ (colimCocone (free_monoid_coeq_sequence_colim_on A)).

Definition T_preserves_chains_impl_T_preserves_diagram_on (A : C) :
  preserves_colimits_of_shape
    (monoidal_left_tensor (T : CMon)) nat_graph
      -> T_preserves_diagram_on A.
Show proof.

Context (A : C).
Context (HT : ∏ B, T_preserves_diagram_on B).

Local Definition HCC := HT _ (pr2 (free_monoid_coeq_sequence_colim_on A)).
Local Definition iso :=
    isColim_is_z_iso _
        (free_monoid_coeq_sequence_leftwhisker_colim_on T A)
        _ _ HCC.

Definition T_preserves_diagram_coeqout_arrow_on :
  T ⊗_{ V} colim (free_monoid_coeq_sequence_colim_on A) -->
    pair_diagram_lob (free_monoid_coeq_sequence_limit_ordinal_step_on A) :=
    (pr1 iso) · ((colimσ_on A) · (z_iso_inv (chain_shift_left_colim_iso _))).

Local Lemma chain_shift_left_colimIn_commutes
  (u : vertex nat_graph) :
  colimIn (CL (chain_shift_left (free_monoid_coeq_sequence_diagram_on A))) u
  · colimArrow
      (chain_shift_left_shl_colim_cocone (free_monoid_coeq_sequence_diagram_on A))
      _ (colimCocone (free_monoid_coeq_sequence_colim_on A))
  = coconeIn (colimCocone (free_monoid_coeq_sequence_colim_on A)) (S u).
Show proof.

Local Lemma leftwhisker_colimIn_equals_on
    (u : vertex nat_graph)
    (ltCC := (make_ColimCocone _ _ _ HCC)) :
  T ⊗^{ V}_{l} colimIn (free_monoid_coeq_sequence_colim_on A) u
  = colimIn (ltCC) u.
Show proof.

Local Lemma TcolimIn_T_preserves_diagram_coeqout_arrow_on
    (u : vertex nat_graph) :
  T ⊗^{ V}_{l} colimIn (free_monoid_coeq_sequence_colim_on A) u
  · T_preserves_diagram_coeqout_arrow_on
  = free_monoid_coeq_sequence_on A u
  · coconeIn (colimCocone (free_monoid_coeq_sequence_colim_on A)) (S u).
Show proof.

Lemma T_preserves_diagram_coeqout_arrow_on_is_coeqout :
    can A · T_preserves_diagram_coeqout_arrow_on =
    top A · T_preserves_diagram_coeqout_arrow_on.
Show proof.

Definition T_preserves_diagram_convergence_inv :
    pair_diagram_rob (free_monoid_coeq_sequence_limit_ordinal_step_on A)
    --> pair_diagram_lob (free_monoid_coeq_sequence_limit_ordinal_step_on A).
Show proof.

Lemma T_preserves_diagram_convergence_inverse_in_precat :
  is_inverse_in_precat
    (pair_diagram_horizontal_arrow (free_monoid_coeq_sequence_limit_ordinal_step_on A))
  T_preserves_diagram_convergence_inv.
Show proof.

Lemma T_preserves_diagram_impl_convergence_on :
    free_monoid_coeq_sequence_converges_on A.
Show proof.

End Convergence.

Section Monoid.

Context (Hconv: free_monoid_coeq_sequence_converges_on I_{V}).

Lemma free_monoid_coeq_sequence_converges_gives_adjoint_mon_alg :
  Mon_alg _ T.
Show proof.

Local Definition TinfM := free_monoid_coeq_sequence_converges_gives_adjoint_mon_alg.

Definition Tinf_pd_Tinf_map
    (n : nat)
    (p := free_monoid_coeq_sequence_on I_{V} n) :=
  ∑ (τn : pair_diagram_lob p ⊗_{V} Tinf --> Tinf)
    (τn1 : pair_diagram_rob p ⊗_{V} Tinf --> Tinf),
      (pair_diagram_arr p ⊗^{V}_{r} Tinf) · τn1
      = α_{V} _ _ _ · (T ⊗^{V}_{l} τn) · (Mon_alg_map _ (pr2 TinfM)).

Lemma free_monoid_coeq_sequence_on_Tinf_pd_Tinf_map_coeqout_rel
    (n : nat)
    (Hn : Tinf_pd_Tinf_map n)
    (Xn := free_monoid_coeq_sequence_on I_{V} n) :
  next_pair_diagram_coeq_arr0 (free_monoid_coeq_sequence_on I_{ V} n) ⊗^{ V}_{r} Tinf
  · (α_{ V } _ _ _
     · T ⊗^{ V}_{l} pr12 Hn · Mon_alg_map _ (pr2 TinfM)) =
  next_pair_diagram_coeq_arr1 (free_monoid_coeq_sequence_on I_{ V} n) ⊗^{ V}_{r} Tinf
  · (α_{ V } _ _ _
      · T ⊗^{ V}_{l} pr12 Hn · Mon_alg_map _ (pr2 TinfM)).
Show proof.

Definition rt_coeq_coequalizer
    {A : C}
    (rt_coeq : preserves_colimits_of_shape
          (monoidal_right_tensor (A : CMon)) Coequalizer_graph)
    {a b : C} {f g : a --> b}
    (coeq : Coequalizer _ f g) :
  Coequalizer _ (f ⊗^{V}_{r} A) (g ⊗^{V}_{r} A).
Show proof.


Context (rt_coeq : rt_preserves_coequalizers V).

Definition free_monoid_coeq_sequence_on_Tinf_pd_Tinf_map_coeqout
    (n : nat)
    (Hn : Tinf_pd_Tinf_map n)
    (Xn1 := free_monoid_coeq_sequence_on I_{V} (S n)) :
  pair_diagram_rob Xn1 ⊗_{V} Tinf --> Tinf.
Show proof.

Definition free_monoid_coeq_sequence_on_Tinf_pd_Tinf_map
    (n : nat) :
  Tinf_pd_Tinf_map n.
Show proof.

Definition free_monoid_coeq_sequence_diagram_on_Tinf_Tinf_map
    (n : vertex nat_graph) :
  dob (free_monoid_coeq_sequence_diagram_on I_{V}) n ⊗_{V} Tinf --> Tinf.
Show proof.

Lemma free_monoid_coeq_sequence_colim_on_Tinf_Tinf_map_formscocone
    (m : vertex nat_graph) :
  pair_diagram_horizontal_arrow (free_monoid_coeq_sequence_on I_{V} m) ⊗^{V}_{r} Tinf
  · free_monoid_coeq_sequence_diagram_on_Tinf_Tinf_map (S m)
  = free_monoid_coeq_sequence_diagram_on_Tinf_Tinf_map m.
Show proof.

Definition free_monoid_coeq_sequence_colim_on_Tinf_Tinf_map :
    colim (free_monoid_coeq_sequence_rightwhisker_colim_on Tinf I_{V}) --> Tinf.
Show proof.

Context (rt_chain : rt_preserves_chains V).

Definition Tinf_monoid_mul_iso
    (rt_colim := free_monoid_coeq_sequence_rightwhisker_colim_on Tinf I_{V}) :
  z_iso (colim (rt_colim)) (Tinf ⊗_{V} Tinf).
Show proof.

Definition Tinf_monoid_mul :
  (Tinf ⊗_{V} Tinf) --> Tinf.
Show proof.

Definition Tinf_monoid_data :
    monoid_data V Tinf :=
  (Tinf_monoid_mul,, colimIn free_monoid_coeq_sequence_colim_unit 0).

Lemma Tinf_monoid_mul_iso_precomp_with_colimIn
    (v : vertex nat_graph) :
  colimIn free_monoid_coeq_sequence_colim_unit v ⊗^{V}_{r} Tinf
  · z_iso_inv Tinf_monoid_mul_iso
  = coconeIn (colimCocone (free_monoid_coeq_sequence_rightwhisker_colim_on Tinf I_{V})) v.
Show proof.

Lemma Tinf_monoid_unit_left :
    monoid_laws_unit_left V Tinf_monoid_data.
Show proof.

Definition Tinf_rightwhisker_inclusion
    (v : vertex nat_graph) :
  dob (free_monoid_coeq_sequence_diagram_on I_{V}) v
  --> dob (rightwhisker_chain_with Tinf (free_monoid_coeq_sequence_diagram_on I_{V})) v.
Show proof.

Lemma Tinf_rightwhisker_inclusion_commutes
    (v : vertex nat_graph) :
  Tinf_rightwhisker_inclusion v
  · dmor (free_monoid_coeq_sequence_diagram_on I_{ V}) (idpath (S v)) ⊗^{V}_{r} Tinf =
  dmor (free_monoid_coeq_sequence_diagram_on I_{V}) (idpath (S v))
  · Tinf_rightwhisker_inclusion (S v).
Show proof.

Context (HT : ∏ B, T_preserves_diagram_on B).

Lemma Tinf_limit_step_colimIn_commutes
    (v : vertex nat_graph) :
  T ⊗^{ V}_{l} colimIn free_monoid_coeq_sequence_colim_unit (S v)
  · CoequalizerArrow C (free_monoid_coeq_sequence_limit_step_coeq I_{ V})
  = CoequalizerArrow C (next_pair_diagram_coeq (free_monoid_coeq_sequence_on I_{V} v))
  · colimIn free_monoid_coeq_sequence_colim_unit (S (S v))
  · pair_diagram_horizontal_arrow (free_monoid_coeq_sequence_limit_ordinal_step_on I_{V}).
Show proof.

Lemma Tinf_colimIn_alg_map_commutes
    (v : vertex nat_graph) :
  T ⊗^{ V}_{l} colimIn free_monoid_coeq_sequence_colim_unit v
  · (Mon_alg_map _ (pr2 TinfM))
  = free_monoid_coeq_sequence_on I_{ V} (v)
  · colimIn free_monoid_coeq_sequence_colim_unit (S v).
Show proof.

Lemma CoequalizerOutUnique' {a b : C} {f g : C⟦a, b⟧}
    (E : Coequalizer C f g) {e : C} {w w' : C⟦colim E, e⟧}
    (H : CoequalizerArrow _ E · w = CoequalizerArrow _ E · w') :
  w = w'.
Show proof.

                                  mon_map
  Xα+ --> Xα+ ⊗ I --> Xα+ ⊗ T∞ -------> T∞
                    =
  Xα+ ----------------------------------> T∞
                  colimIn

Lemma Tinf_monoid_unit_right_pointwise (v : vertex nat_graph) :
  ruinv^{ V }_{ pair_diagram_lob (free_monoid_coeq_sequence_on I_{ V} v)}
  · (pair_diagram_lob (free_monoid_coeq_sequence_on I_{ V} v)
    ⊗^{ V}_{l} colimIn free_monoid_coeq_sequence_colim_unit 0
    · free_monoid_coeq_sequence_diagram_on_Tinf_Tinf_map v) =
  colimIn free_monoid_coeq_sequence_colim_unit v.
Show proof.

Lemma Tinf_monoid_unit_right :
    monoid_laws_unit_right V Tinf_monoid_data.
Show proof.

Definition rt_chain_iso_v (A : C) (v : vertex nat_graph) :=
  z_iso
    (dob (rightwhisker_chain_with A (free_monoid_coeq_sequence_diagram_on I_{V})) v)
    (dob (free_monoid_coeq_sequence_diagram_on A) v).

Definition z_iso_from_rt_chain_iso_v {A : C} {v : vertex nat_graph}
    (Cisv : rt_chain_iso_v A v) : z_iso _ _ := Cisv.
Coercion z_iso_from_rt_chain_iso_v : rt_chain_iso_v >-> z_iso.

Definition rt_chain_iso_pair_total_rel {A : C} {v : vertex nat_graph}
    (iv : rt_chain_iso_v A v) (iSv : rt_chain_iso_v A (S v)) :=
  (z_iso_mor iv) · (dmor (free_monoid_coeq_sequence_diagram_on A) (idpath (S v)))
  = (dmor (rightwhisker_chain_with A (free_monoid_coeq_sequence_diagram_on I_{V})) (idpath (S v)))
  · (z_iso_mor iSv).

Definition rt_chain_iso_pair_rel {A : C} {v : vertex nat_graph}
    (iv : rt_chain_iso_v A v) (iSv : rt_chain_iso_v A (S v)) :=
  free_monoid_coeq_sequence_on I_{ V} v ⊗^{ V}_{r} A
  · (z_iso_mor iSv)
  = α^{ V }_{_, _, _}
  · T ⊗^{ V}_{l} (z_iso_mor iv)
  · free_monoid_coeq_sequence_on A v.

Lemma rt_chain_iso_pair_rel_impl_total_rel
    {A : C} {v : vertex nat_graph}
    {iv : rt_chain_iso_v A v} {iSv : rt_chain_iso_v A (S v)}
    (H : rt_chain_iso_pair_rel iv iSv) :
  rt_chain_iso_pair_total_rel iv iSv.
Show proof.

Definition rt_chain_iso_pair
    (A : C)
    (v : vertex nat_graph) :=
  ∑ (iv : rt_chain_iso_v A v) (iSv : rt_chain_iso_v A (S v)),
      rt_chain_iso_pair_rel iv iSv.
Definition rtisp_liso
    {A : C} {v : vertex nat_graph}
    (Cisv : rt_chain_iso_pair A v) :=
  pr1 Cisv.
Definition rtisp_riso
    {A : C} {v : vertex nat_graph}
    (Cisv : rt_chain_iso_pair A v) :=
  pr12 Cisv.
Definition rtisp_rel
    {A : C} {v : vertex nat_graph}
    (Cisv : rt_chain_iso_pair A v) :=
  pr22 Cisv.

Definition make_rt_chain_iso_pair
    {A : C} {v : vertex nat_graph}
    {iv : rt_chain_iso_v A v} {iSv : rt_chain_iso_v A (S v)}
    (rel : rt_chain_iso_pair_rel iv iSv) :
      rt_chain_iso_pair A v :=
  (_,, _,, rel).

Lemma rt_chain_iso_pair_ind_iscoeqout
    (A : C) (v : vertex nat_graph)
    (Cisp : rt_chain_iso_pair A v) :
    next_pair_diagram_coeq_arr0 (free_monoid_coeq_sequence_on I_{ V} v) ⊗^{ V}_{r} A
    · (α^{ V }_{_, _, _}
       · (T ⊗^{ V}_{l} z_iso_mor (rtisp_riso Cisp)
          · CoequalizerArrow C (next_pair_diagram_coeq (free_monoid_coeq_sequence_on A v)))) =
    next_pair_diagram_coeq_arr1 (free_monoid_coeq_sequence_on I_{ V} v) ⊗^{ V}_{r} A
    · (α^{ V }_{_, _, _}
       · (T ⊗^{ V}_{l} z_iso_mor (rtisp_riso Cisp)
          · CoequalizerArrow C
              (next_pair_diagram_coeq (free_monoid_coeq_sequence_on A v)))).
Show proof.

Lemma rt_chain_iso_pair_ind_inv_iscoeqout
  (A : C) (v : vertex nat_graph)
  (Cisp : rt_chain_iso_pair A v) :
    next_pair_diagram_coeq_arr0 (free_monoid_coeq_sequence_on A v)
    · (T ⊗^{ V}_{l} z_iso_inv (rtisp_riso Cisp)
      · (αinv^{ V }_{_, _, _}
        · CoequalizerArrow C (next_pair_diagram_coeq (free_monoid_coeq_sequence_on I_{ V} v)) ⊗^{V}_{r} A
        )
      )
    = next_pair_diagram_coeq_arr1 (free_monoid_coeq_sequence_on A v)
    · (T ⊗^{ V}_{l} z_iso_inv (rtisp_riso Cisp)
      · (αinv^{ V }_{_, _, _}
        · CoequalizerArrow C (next_pair_diagram_coeq (free_monoid_coeq_sequence_on I_{ V} v)) ⊗^{V}_{r} A
        )
      ).
Show proof.

Lemma rt_chain_iso_pairs (A : C) (v : vertex nat_graph) :
    rt_chain_iso_pair A v.
Show proof.

Lemma rt_chain_isos (A : C) (v : vertex nat_graph) :
    rt_chain_iso_v A v.
Show proof.

Lemma rt_chain_isos_commute (A : C) (v : vertex nat_graph) :
    dmor (rightwhisker_chain_with A (free_monoid_coeq_sequence_diagram_on I_{ V})) (idpath (S v))
    · z_iso_mor (rt_chain_isos A (S v)) =
    z_iso_mor (rt_chain_isos A v)
    · dmor (free_monoid_coeq_sequence_diagram_on A) (idpath (S v)).
Show proof.

Opaque rt_chain_iso_pairs.

Lemma rt_chain_colim_iso (A : C) :
    z_iso
      (colim (free_monoid_coeq_sequence_rightwhisker_colim_on A I_{V}))
      (colim (free_monoid_coeq_sequence_colim_on A)).
Show proof.

Lemma Tinf_mul_alg_map_commutes :
    (Mon_alg_map _ (pr2 TinfM)) ⊗^{ V}_{r} Tinf · Tinf_monoid_mul
    = α^{V}_{_, _, _}
    · T ⊗^{ V}_{l} Tinf_monoid_mul · (Mon_alg_map _ (pr2 TinfM)).
Show proof.

Local Lemma Tinf_mul_assoc_pointwise_associator_mess
    (t s l : C) (f : (l ⊗_{V} s) --> s) :
  αinv^{V}_{t ⊗_{V} l, s, s}
  · (α^{V}_{t, l, s}
     · t ⊗^{V}_{l} f) ⊗^{V}_{r} s
  · α^{V}_{t, s, s}
  = α^{V}_{t, l, s ⊗_{V} s}
  · t ⊗^{V}_{l} (
    αinv^{V}_{l, s, s}
    · f ⊗^{V}_{r} s
  ).
Show proof.

Lemma Tinf_monoid_assoc_pointwise
    (v : vertex nat_graph) :
  αinv^{V}_{_, _, _}
  · free_monoid_coeq_sequence_diagram_on_Tinf_Tinf_map v ⊗^{V}_{r} Tinf
  · Tinf_monoid_mul
  = pair_diagram_lob (free_monoid_coeq_sequence_on I_{V} v) ⊗^{V}_{l} Tinf_monoid_mul
  · free_monoid_coeq_sequence_diagram_on_Tinf_Tinf_map v.
Show proof.

Lemma Tinf_monoid_assoc :
    monoid_laws_assoc V Tinf_monoid_data.
Show proof.

Definition Tinf_monoid_axioms :
    monoid_laws V Tinf_monoid_data :=
  (Tinf_monoid_unit_left,, Tinf_monoid_unit_right,, Tinf_monoid_assoc).

Definition Tinf_monoid : monoid V Tinf :=
    (_,, Tinf_monoid_axioms).

End Monoid.

End free_monoid_colim.