Library UniMath.ModelCategories.Generated.LNWFSMonoidalStructure

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Monads.Monads.
Require Import UniMath.CategoryTheory.Monads.Comonads.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.
Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.

Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Arrow.
Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Three.
Require Import UniMath.ModelCategories.Lifting.
Require Import UniMath.ModelCategories.NWFS.
Require Import UniMath.ModelCategories.Helpers.
Require Import UniMath.ModelCategories.Generated.LNWFSHelpers.
Require Import UniMath.ModelCategories.Generated.FFMonoidalStructure.

Local Open Scope cat.
Local Open Scope morcls.

Section LNWFS_composition.

Context {C : category}.

Local Definition left_reduced_lp
    (F : Ff C) {f g : arrow C}
    (γ : f --> g) : (f --> fact_R F g).
Show proof.

Local Lemma left_reduced_lp_lift
    {F : Ff C} (L : lnwfs_over F)
    {f g : arrow C} (γ : (fact_L F f) --> g) :
  filler (arrow_mor_comm (left_reduced_lp F γ)).
Show proof.

Local Definition LNWFS_lcomp_comp_helper
    (F F' : Ff C) (f : arrow C) :=
  fact_L F f · fact_L F' (fact_R F f).

Definition LNWFS_lcomp_comul_L_lp
    {F : Ff C}
    (L : lnwfs_over F)
    (F' : Ff C)
    (f : arrow C) :
  fact_L F f --> LNWFS_lcomp_comp_helper F F' f.
Show proof.

Definition LNWFS_lcomp_comul_L'_lp
    {F' F : Ff C}
    (L' : lnwfs_over F')
    (L : lnwfs_over F)
    (f : arrow C) :
  fact_L F' (fact_R F f) --> fact_R F (LNWFS_lcomp_comp_helper F F' f).
Show proof.

Definition LNWFS_lcomp_comul_data {F' F : Ff C} (L' : lnwfs_over F') (L : lnwfs_over F) :
    nat_trans_data (fact_L (F' ⊗ F)) ((fact_L (F' ⊗ F)) ∙ (fact_L (F' ⊗ F))).
Show proof.

Lemma LNWFS_lcomp_comul_axioms {F' F : Ff C} (L' : lnwfs_over F') (L : lnwfs_over F) :
    is_nat_trans _ _ (LNWFS_lcomp_comul_data L' L).
Show proof.

Definition LNWFS_lcomp_comul {F' F : Ff C} (L' : lnwfs_over F') (L : lnwfs_over F) :
    (fact_L (F' ⊗ F)) ⟹ ((fact_L (F' ⊗ F)) ∙ (fact_L (F' ⊗ F))) :=
  (_,, LNWFS_lcomp_comul_axioms L' L).

Global Opaque left_reduced_lp.
Global Opaque left_reduced_lp_lift.
Global Opaque LNWFS_lcomp_comul_L_lp.
Global Opaque LNWFS_lcomp_comul_L'_lp.

Lemma LNWFS_lcomp_comul_mul_law11 {F' F : Ff C}
    (L' : lnwfs_over F') (L : lnwfs_over F) (a : arrow C) :
    arrow_mor11 (
      (disp_δ (L_monad_data (F' ⊗ F) (LNWFS_lcomp_comul L' L)) a)
      · (# (fact_L (F' ⊗ F))
          (disp_δ (L_monad_data (F' ⊗ F) (LNWFS_lcomp_comul L' L)) a))
    )
    =
    arrow_mor11 (
      (disp_δ (L_monad_data (F' ⊗ F) (LNWFS_lcomp_comul L' L)) a)
    · (disp_δ (L_monad_data (F' ⊗ F) (LNWFS_lcomp_comul L' L))
        (fact_L (F' ⊗ F) a))
    ).
Show proof.

Definition LNWFS_lcomp_comul_monad_laws {F' F : Ff C} (L' : lnwfs_over F') (L : lnwfs_over F) :
    disp_Comonad_laws (L_monad_data (F' ⊗ F) (LNWFS_lcomp_comul L' L)).
Show proof.

Definition LNWFS_lcomp {F' F : Ff C} (L' : LNWFS C F') (L : LNWFS C F) :
    LNWFS C (F' ⊗ F) :=
  (LNWFS_lcomp_comul L' L,, LNWFS_lcomp_comul_monad_laws L' L).

Definition LNWFS_tot_lcomp (L' L : total_category (LNWFS C)) :
    total_category (LNWFS C) :=
  (_,, LNWFS_lcomp (pr2 L') (pr2 L)).

Notation "l L⊗ l'" := (LNWFS_lcomp l l') (at level 50).
Notation "l Ltot⊗ l'" := (LNWFS_tot_lcomp l l') (at level 50).

Definition LNWFS_lcomp_unit_comul_data :
    nat_trans_data (fact_L (@Ff_lcomp_unit C)) ((fact_L Ff_lcomp_unit) ∙ (fact_L Ff_lcomp_unit)).
Show proof.

Definition LNWFS_lcomp_unit_comul_axioms :
    is_nat_trans _ _ LNWFS_lcomp_unit_comul_data.
Show proof.

Definition LNWFS_lcomp_unit_comul :
    (fact_L (@Ff_lcomp_unit C)) ⟹ ((fact_L Ff_lcomp_unit) ∙ (fact_L Ff_lcomp_unit)) :=
  (_,, LNWFS_lcomp_unit_comul_axioms).

Definition LNWFS_lcomp_unit_comul_monad_laws :
  disp_Comonad_laws (L_monad_data (@Ff_lcomp_unit C) (LNWFS_lcomp_unit_comul)).
Show proof.

Definition LNWFS_lcomp_unit :
    LNWFS C (@Ff_lcomp_unit C) :=
  (LNWFS_lcomp_unit_comul,, LNWFS_lcomp_unit_comul_monad_laws).

Definition LNWFS_tot_lcomp_unit :
    total_category (LNWFS C) :=
  (_,, LNWFS_lcomp_unit).

Definition LNWFS_l_id_left {F : Ff C} (L : LNWFS _ F) :
    (LNWFS_lcomp_unit L⊗ L) -->[Ff_l_id_left F] L.
Show proof.

Definition LNWFS_tot_l_id_left (L : total_category (LNWFS C)) :
    (LNWFS_tot_lcomp_unit Ltot⊗ L) --> L :=
  (_,, LNWFS_l_id_left (pr2 L)).

Definition LNWFS_l_id_left_rev {F : Ff C} (L : LNWFS _ F) :
    L -->[Ff_l_id_left_rev F] (LNWFS_lcomp_unit L⊗ L).
Show proof.

Definition LNWFS_tot_l_id_left_rev (L : total_category (LNWFS C)) :
    L --> (LNWFS_tot_lcomp_unit Ltot⊗ L) :=
  (_,, LNWFS_l_id_left_rev (pr2 L)).

Definition LNWFS_l_id_right {F : Ff C} (L : LNWFS _ F) :
    (L L⊗ LNWFS_lcomp_unit) -->[Ff_l_id_right F] L.
Show proof.

Definition LNWFS_tot_l_id_right (L : total_category (LNWFS C)) :
    (L Ltot⊗ LNWFS_tot_lcomp_unit) --> L :=
  (_,, LNWFS_l_id_right (pr2 L)).

Definition LNWFS_l_id_right_rev {F : Ff C} (L : LNWFS _ F) :
    L -->[Ff_l_id_right_rev F] (L L⊗ LNWFS_lcomp_unit).
Show proof.

Definition LNWFS_tot_l_id_right_rev (L : total_category (LNWFS C)) :
    L --> (L Ltot⊗ LNWFS_tot_lcomp_unit) :=
  (_,, LNWFS_l_id_right_rev (pr2 L)).

Definition LNWFS_l_assoc_rev {F F' F'' : Ff C}
    (L : LNWFS _ F) (L' : LNWFS _ F') (L'' : LNWFS _ F'') :
  (L L⊗ (L' L⊗ L'')) -->[Ff_l_assoc_rev F F' F''] ((L L⊗ L') L⊗ L'').
Show proof.

Definition LNWFS_tot_l_assoc_rev (L L' L'' : total_category (LNWFS C)) :
    (L Ltot⊗ (L' Ltot⊗ L'')) --> ((L Ltot⊗ L') Ltot⊗ L'') :=
  (_,, LNWFS_l_assoc_rev (pr2 L) (pr2 L') (pr2 L'')).

Definition LNWFS_l_assoc {F F' F'' : Ff C}
    (L : LNWFS _ F) (L' : LNWFS _ F') (L'' : LNWFS _ F'') :
  ((L L⊗ L') L⊗ L'') -->[Ff_l_assoc F F' F''] (L L⊗ (L' L⊗ L'')).
Show proof.

Definition LNWFS_tot_l_assoc (L L' L'' : total_category (LNWFS C)) :
    ((L Ltot⊗ L') Ltot⊗ L'' ) --> (L Ltot⊗ (L' Ltot⊗ L'')) :=
  (_,, LNWFS_l_assoc (pr2 L) (pr2 L') (pr2 L'')).

Definition LNWFS_l_rightwhisker {F G G': Ff C}
    {Λ : LNWFS _ G} {Λ' : LNWFS _ G'} {τG : G --> G'}
    (τ : Λ -->[τG] Λ') (L : LNWFS _ F) :
  (Λ L⊗ L) -->[τG ⊗post F] (Λ' L⊗ L).
Show proof.

Definition LNWFS_tot_l_rightwhisker
    {Λ Λ' : total_category (LNWFS C)}
    (τ : Λ --> Λ') (L : total_category (LNWFS C)) :
  (Λ Ltot⊗ L) --> (Λ' Ltot⊗ L) :=
    (_,, LNWFS_l_rightwhisker (pr2 τ) (pr2 L)).

Notation "τ L⊗post l" := (LNWFS_l_rightwhisker τ l) (at level 50).
Notation "τ Ltot⊗post l" := (LNWFS_tot_l_rightwhisker τ l) (at level 50).

Lemma LNWFS_tot_l_rightwhisker_id
    (Λ L : total_category (LNWFS C)) :
  (identity Λ Ltot⊗post L) = identity _.
Show proof.

Lemma LNWFS_tot_l_rightwhisker_comp
    {Λ Λ' Λ'': total_category (LNWFS C)}
    (τ : Λ --> Λ') (τ' : Λ' --> Λ'')
    (L : total_category (LNWFS C)) :
  ((τ · τ') Ltot⊗post L) = (τ Ltot⊗post L) · (τ' Ltot⊗post L).
Show proof.

Definition LNWFS_l_leftwhisker {F G G': Ff C}
    {Λ : LNWFS _ G} {Λ' : LNWFS _ G'} {τG : G --> G'}
    (L : LNWFS _ F) (τ : Λ -->[τG] Λ') :
  (L L⊗ Λ) -->[F ⊗pre τG] (L L⊗ Λ').
Show proof.

Definition LNWFS_tot_l_leftwhisker {Λ Λ' : total_category (LNWFS C)}
  (L : total_category (LNWFS C)) (τ : Λ --> Λ') :
  (L Ltot⊗ Λ) --> (L Ltot⊗ Λ'):=
    (_,, LNWFS_l_leftwhisker (pr2 L) (pr2 τ)).

Notation "l L⊗pre τ" := (LNWFS_l_leftwhisker l τ) (at level 50).
Notation "l Ltot⊗pre τ" := (LNWFS_tot_l_leftwhisker l τ) (at level 50).

Lemma LNWFS_tot_l_leftwhisker_id
    (L Λ : total_category (LNWFS C)) :
  (L Ltot⊗pre (identity Λ)) = identity _.
Show proof.

Lemma LNWFS_tot_l_leftwhisker_comp
    {Λ Λ' Λ'': total_category (LNWFS C)}
    (L : total_category (LNWFS C))
    (τ : Λ --> Λ') (τ' : Λ' --> Λ'') :
  (L Ltot⊗pre (τ · τ')) = (L Ltot⊗pre τ) · (L Ltot⊗pre τ').
Show proof.

Definition LNWFS_l_mor_comp {F F' G G' : Ff C}
    {τF : F --> F'} {ρG : G --> G'}
    {L : LNWFS _ F} {L' : LNWFS _ F'}
    {Λ : LNWFS _ G} {Λ' : LNWFS _ G'}
    (τ : L -->[τF] L') (ρ : Λ -->[ρG] Λ') :
  (L L⊗ Λ) -->[Ff_l_mor_comp τF ρG] (L' L⊗ Λ').
Show proof.

Definition LNWFS_tot_l_mor_comp {L L' Λ Λ' : total_category (LNWFS C)}
    (τ : L --> L') (ρ : Λ --> Λ') :
  (L Ltot⊗ Λ) --> (L' Ltot⊗ Λ') :=
    (_,, LNWFS_l_mor_comp (pr2 τ) (pr2 ρ)).

Definition LNWFS_l_point {F : Ff C} (L : LNWFS _ F) :
    LNWFS_lcomp_unit -->[Ff_l_point F] L.
Show proof.

Definition LNWFS_tot_l_point (L : total_category (LNWFS C)) :
    LNWFS_tot_lcomp_unit --> L :=
  (_,, LNWFS_l_point (pr2 L)).

Lemma LNWFS_tot_mor_eq {L L' : total_category (LNWFS C)}
    (τ τ' : L --> L') :
  (∏ (f : arrow C), pr1 (pr11 τ f) = pr1 (pr11 τ' f)) ->
      τ = τ'.
Show proof.

End LNWFS_composition.

Notation "l L⊗ l'" := (LNWFS_lcomp l l') (at level 50).
Notation "l Ltot⊗ l'" := (LNWFS_tot_lcomp l l') (at level 50).
Notation "l L⊗pre τ" := (LNWFS_l_leftwhisker l τ) (at level 50).
Notation "l Ltot⊗pre τ" := (LNWFS_tot_l_leftwhisker l τ) (at level 50).
Notation "τ L⊗post l" := (LNWFS_l_rightwhisker τ l) (at level 50).
Notation "τ Ltot⊗post l" := (LNWFS_tot_l_rightwhisker τ l) (at level 50).

Require Import UniMath.CategoryTheory.Monoidal.Categories.
Require Import UniMath.CategoryTheory.Monoidal.Displayed.Monoidal.
Require Import UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal.

Section LNWFS_monoidal.

Context {C : category}.

Definition LNWFS_disp_tensor_data : disp_tensor (LNWFS C) Ff_monoidal.
Show proof.

Definition LNWFS_disp_monoidal_data : disp_monoidal_data (LNWFS C) Ff_monoidal.
Show proof.

Definition LNWFS_disp_monoidal_laws : disp_monoidal_laws LNWFS_disp_monoidal_data.
Show proof.

Definition LNWFS_monoidal : disp_monoidal (LNWFS C) Ff_monoidal :=
    (_,, LNWFS_disp_monoidal_laws).

Definition LNWFS_tot_monoidal : monoidal _ :=
    total_monoidal LNWFS_monoidal.

Definition Ff_monoidal : monoidal (Ff C) :=
    (_,, Ff_monoidal_laws).

End LNWFS_monoidal.

Require Import UniMath.CategoryTheory.Monads.Monads.
Require Import UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids.

Section LNWFS_monoid_is_NWFS.

Context {C : category}.
Local Definition LNWFSC := total_category (LNWFS C).

Definition LNWFS_tot_monoid_is_NWFS_monoid_data
    {L : LNWFSC} (R : monoid (LNWFS_tot_monoidal) L) :
  monoid_data Ff_monoidal (pr1 L).
Show proof.

Definition LNWFS_tot_monoid_is_NWFS_monoid_axioms
    {L : LNWFSC} (R : monoid (LNWFS_tot_monoidal) L) :
  monoid_laws _ (LNWFS_tot_monoid_is_NWFS_monoid_data R).
Show proof.

Definition LNWFS_tot_monoid_projection
      {L : LNWFSC} (R : monoid (LNWFS_tot_monoidal) L) :
  monoid Ff_monoidal (pr1 L) :=
    (_,, LNWFS_tot_monoid_is_NWFS_monoid_axioms R).

Definition LNWFS_tot_monoid_is_NWFS
    {L : LNWFSC} (R : monoid (LNWFS_tot_monoidal) L) :
  NWFS C (pr1 L).
Show proof.

End LNWFS_monoid_is_NWFS.