Library UniMath.Semantics.LinearLogic.LinearCategory

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.Monads.Comonads.
Require Import UniMath.CategoryTheory.Monoidal.Categories.
Require Import UniMath.CategoryTheory.Monoidal.Functors.
Require Import UniMath.CategoryTheory.Monoidal.FunctorCategories.
Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric.
Require Import UniMath.CategoryTheory.Monoidal.Structure.SymmetricDiagonal.
Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed.
Require Import UniMath.CategoryTheory.Monoidal.Comonoids.Category.
Require Import UniMath.CategoryTheory.Monoidal.Examples.ConstantFunctor.
Require Import UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids.
Require Import UniMath.CategoryTheory.categories.Dialgebras.
Require Import UniMath.CategoryTheory.Monoidal.Examples.DiagonalFunctor.

Import MonoidalNotations.

Local Open Scope cat.
Local Open Scope moncat.

1. Data of linear categories
Definition linear_category_data
  : UU
  := โˆ‘ (๐•ƒ : sym_mon_closed_cat)
       (bang : sym_monoidal_cmd ๐•ƒ),
     (โˆ (x : ๐•ƒ), bang x --> bang x โŠ— bang x)
     ร—
     (โˆ (x : ๐•ƒ), bang x --> I_{๐•ƒ}).

Definition make_linear_category_data
           (๐•ƒ : sym_mon_closed_cat)
           (bang : sym_monoidal_cmd ๐•ƒ)
           (ฮด : โˆ (x : ๐•ƒ), bang x --> bang x โŠ— bang x)
           (ฮต : โˆ (x : ๐•ƒ), bang x --> I_{๐•ƒ})
  : linear_category_data
  := ๐•ƒ ,, bang ,, ฮด ,, ฮต.

Coercion linear_category_data_to_sym_mon_closed_cat
         (๐•ƒ : linear_category_data)
  : sym_mon_closed_cat
  := pr1 ๐•ƒ.

Definition linear_category_bang
           (๐•ƒ : linear_category_data)
  : sym_monoidal_cmd ๐•ƒ
  := pr12 ๐•ƒ.

Definition linear_category_bang_functor
           (๐•ƒ : linear_category_data)
  : lax_monoidal_functor ๐•ƒ ๐•ƒ
  := _ ,, lax_monoidal_from_symmetric_monoidal_comonad _ (linear_category_bang ๐•ƒ).

Definition linear_category_comult
           (๐•ƒ : linear_category_data)
           (x : ๐•ƒ)
  : linear_category_bang ๐•ƒ x
    -->
    linear_category_bang ๐•ƒ x โŠ— linear_category_bang ๐•ƒ x
  := pr122 ๐•ƒ x.

Definition linear_category_counit
           (๐•ƒ : linear_category_data)
           (x : ๐•ƒ)
  : linear_category_bang ๐•ƒ x --> I_{๐•ƒ}
  := pr222 ๐•ƒ x.

2. Laws of linear categories
Definition linear_category_laws
           (๐•ƒ : linear_category_data)
  : UU
  :=
     (โˆ (x y : ๐•ƒ)
        (f : x --> y),
      #(linear_category_bang ๐•ƒ) f
      ยท linear_category_comult ๐•ƒ y
      =
      linear_category_comult ๐•ƒ x
      ยท (#(linear_category_bang ๐•ƒ) f #โŠ— #(linear_category_bang ๐•ƒ) f))
     ร—
     
     (โˆ (x y : ๐•ƒ)
        (f : x --> y),
      #(linear_category_bang ๐•ƒ) f ยท linear_category_counit ๐•ƒ y
      =
      linear_category_counit ๐•ƒ x)
     ร—
     
     (โˆ (x : ๐•ƒ),
      linear_category_comult ๐•ƒ x
      ยท (ฮด (linear_category_bang ๐•ƒ) x #โŠ— ฮด (linear_category_bang ๐•ƒ) x)
      ยท mon_functor_tensor (linear_category_bang_functor ๐•ƒ) _ _
      =
      ฮด (linear_category_bang ๐•ƒ) x
      ยท #(linear_category_bang ๐•ƒ) (linear_category_comult ๐•ƒ x))
     ร—
     
     (โˆ (x : ๐•ƒ),
      linear_category_counit ๐•ƒ x
      ยท mon_functor_unit (linear_category_bang_functor ๐•ƒ)
      =
      ฮด (linear_category_bang ๐•ƒ) x
      ยท #(linear_category_bang ๐•ƒ) (linear_category_counit ๐•ƒ x))
     ร—
     
     (โˆ (x : ๐•ƒ),
      ฮด (linear_category_bang ๐•ƒ) x
      ยท linear_category_counit ๐•ƒ (linear_category_bang ๐•ƒ x)
      =
      linear_category_counit ๐•ƒ x)
     ร—
     
     (โˆ (x : ๐•ƒ),
      ฮด (linear_category_bang ๐•ƒ) x
      ยท linear_category_comult ๐•ƒ (linear_category_bang ๐•ƒ x)
      =
      linear_category_comult ๐•ƒ x
      ยท (ฮด (linear_category_bang ๐•ƒ) x #โŠ— ฮด (linear_category_bang ๐•ƒ) x))
     ร—
     
     (โˆ (x : ๐•ƒ),
      linear_category_comult ๐•ƒ x
      ยท (identity _ #โŠ— linear_category_comult ๐•ƒ x)
      =
      linear_category_comult ๐•ƒ x
      ยท (linear_category_comult ๐•ƒ x #โŠ— identity _)
      ยท mon_lassociator _ _ _)
     ร—
     
     (โˆ (x : ๐•ƒ),
      linear_category_comult ๐•ƒ x
      ยท (linear_category_counit ๐•ƒ x #โŠ— identity _)
      ยท mon_lunitor _
      =
      identity _)
     ร—
     
     (โˆ (x : ๐•ƒ),
      linear_category_comult ๐•ƒ x
      ยท sym_mon_braiding ๐•ƒ _ _
      =
        linear_category_comult ๐•ƒ x)
     ร—
     
     (โˆ x y : ๐•ƒ,
         mon_functor_tensor (linear_category_bang_functor ๐•ƒ) x y
           ยท linear_category_comult ๐•ƒ (x โŠ— y)
         = (linear_category_comult ๐•ƒ x) #โŠ— (linear_category_comult ๐•ƒ y)
             ยท (inner_swap ๐•ƒ
                  (linear_category_bang ๐•ƒ x)
                  (linear_category_bang ๐•ƒ x)
                  (linear_category_bang ๐•ƒ y)
                  (linear_category_bang ๐•ƒ y)
                  ยท mon_functor_tensor (linear_category_bang_functor ๐•ƒ) x y
                  #โŠ— mon_functor_tensor (linear_category_bang_functor ๐•ƒ) x y))
     ร—
     
     (mon_functor_unit (linear_category_bang_functor ๐•ƒ)
                ยท linear_category_comult ๐•ƒ I_{๐•ƒ}
              = mon_linvunitor I_{๐•ƒ}
                  ยท mon_functor_unit (linear_category_bang_functor ๐•ƒ)
                  #โŠ— mon_functor_unit (linear_category_bang_functor ๐•ƒ))
     ร—
     
     (โˆ x y : ๐•ƒ, mon_functor_tensor (linear_category_bang_functor ๐•ƒ) x y
                           ยท linear_category_counit ๐•ƒ (x โŠ— y)
                         = linear_category_counit ๐•ƒ x #โŠ— linear_category_counit ๐•ƒ y
                             ยท mon_lunitor (monoidal_unit ๐•ƒ))
     ร—
     
     (mon_functor_unit (linear_category_bang_functor ๐•ƒ)
                ยท linear_category_counit ๐•ƒ I_{๐•ƒ}
              = identity I_{๐•ƒ}).

Definition linear_category
  : UU
  := โˆ‘ (๐•ƒ : linear_category_data), linear_category_laws ๐•ƒ.

Definition make_linear_category
           (๐•ƒ : linear_category_data)
           (H : linear_category_laws ๐•ƒ)
  : linear_category
  := ๐•ƒ ,, H.

Coercion linear_category_to_data
         (๐•ƒ : linear_category)
  : linear_category_data
  := pr1 ๐•ƒ.

Section AccessorsLaws.
  Context {๐•ƒ : linear_category}.

  Proposition linear_category_comult_nat
              {x y : ๐•ƒ}
              (f : x --> y)
    : #(linear_category_bang ๐•ƒ) f
      ยท linear_category_comult ๐•ƒ y
      =
      linear_category_comult ๐•ƒ x
      ยท (#(linear_category_bang ๐•ƒ) f #โŠ— #(linear_category_bang ๐•ƒ) f).
  Show proof.
    exact (pr12 ๐•ƒ x y f).

  Proposition linear_category_counit_nat
              {x y : ๐•ƒ}
              (f : x --> y)
    : #(linear_category_bang ๐•ƒ) f ยท linear_category_counit ๐•ƒ y
      =
      linear_category_counit ๐•ƒ x.
  Show proof.
    exact (pr122 ๐•ƒ x y f).

  Proposition linear_category_comult_coalgebra_mor
              (x : ๐•ƒ)
    : linear_category_comult ๐•ƒ x
      ยท (ฮด (linear_category_bang ๐•ƒ) x #โŠ— ฮด (linear_category_bang ๐•ƒ) x)
      ยท mon_functor_tensor (linear_category_bang_functor ๐•ƒ) _ _
      =
      ฮด (linear_category_bang ๐•ƒ) x
      ยท #(linear_category_bang ๐•ƒ) (linear_category_comult ๐•ƒ x).
  Show proof.
    exact (pr1 (pr222 ๐•ƒ) x).

  Proposition linear_category_counit_coalgebra_mor
              (x : ๐•ƒ)
    : linear_category_counit ๐•ƒ x
      ยท mon_functor_unit (linear_category_bang_functor ๐•ƒ)
      =
      ฮด (linear_category_bang ๐•ƒ) x
      ยท #(linear_category_bang ๐•ƒ) (linear_category_counit ๐•ƒ x).
  Show proof.
    exact (pr12 (pr222 ๐•ƒ) x).

  Proposition linear_category_counit_comonoid_mor_counit
              (x : ๐•ƒ)
    : ฮด (linear_category_bang ๐•ƒ) x
      ยท linear_category_counit ๐•ƒ (linear_category_bang ๐•ƒ x)
      =
      linear_category_counit ๐•ƒ x.
  Show proof.
    exact (pr122 (pr222 ๐•ƒ) x).

  Proposition linear_category_counit_comonoid_mor_comult
              (x : ๐•ƒ)
    : ฮด (linear_category_bang ๐•ƒ) x
      ยท linear_category_comult ๐•ƒ (linear_category_bang ๐•ƒ x)
      =
      linear_category_comult ๐•ƒ x
      ยท (ฮด (linear_category_bang ๐•ƒ) x #โŠ— ฮด (linear_category_bang ๐•ƒ) x).
  Show proof.
    exact (pr1 (pr222 (pr222 ๐•ƒ)) x).

  Proposition linear_category_coassoc
              (x : ๐•ƒ)
    : linear_category_comult ๐•ƒ x
      ยท (identity _ #โŠ— linear_category_comult ๐•ƒ x)
      =
      linear_category_comult ๐•ƒ x
      ยท (linear_category_comult ๐•ƒ x #โŠ— identity _)
      ยท mon_lassociator _ _ _.
  Show proof.
    exact (pr12 (pr222 (pr222 ๐•ƒ)) x).

  Proposition linear_category_counitality
              (x : ๐•ƒ)
    : linear_category_comult ๐•ƒ x
      ยท (linear_category_counit ๐•ƒ x #โŠ— identity _)
      ยท mon_lunitor _
      =
      identity _.
  Show proof.
    exact (pr122 (pr222 (pr222 ๐•ƒ)) x).

  Proposition linear_category_cocommutative
              (x : ๐•ƒ)
    : linear_category_comult ๐•ƒ x
      ยท sym_mon_braiding ๐•ƒ _ _
      =
      linear_category_comult ๐•ƒ x.
  Show proof.
    exact (pr1 (pr222 (pr222 (pr222 ๐•ƒ))) x).

  Proposition linear_category_comult_preserves_tensor
    (x y : ๐•ƒ)
    : mon_functor_tensor (linear_category_bang_functor ๐•ƒ) x y
           ยท linear_category_comult ๐•ƒ (x โŠ— y)
         = (linear_category_comult ๐•ƒ x) #โŠ— (linear_category_comult ๐•ƒ y)
             ยท (inner_swap ๐•ƒ
                  (linear_category_bang ๐•ƒ x)
                  (linear_category_bang ๐•ƒ x)
                  (linear_category_bang ๐•ƒ y)
                  (linear_category_bang ๐•ƒ y)
                  ยท mon_functor_tensor (linear_category_bang_functor ๐•ƒ) x y
                  #โŠ— mon_functor_tensor (linear_category_bang_functor ๐•ƒ) x y).
  Show proof.
    exact (pr12 (pr222 (pr222 (pr222 ๐•ƒ))) x y).

  Proposition linear_category_comult_preserves_unit
    : mon_functor_unit (linear_category_bang_functor ๐•ƒ)
        ยท linear_category_comult ๐•ƒ I_{๐•ƒ}
      = mon_linvunitor I_{๐•ƒ}
          ยท mon_functor_unit (linear_category_bang_functor ๐•ƒ)
          #โŠ— mon_functor_unit (linear_category_bang_functor ๐•ƒ).
  Show proof.
    exact (pr122 (pr222 (pr222 (pr222 ๐•ƒ)))).

  Proposition linear_category_counit_preserves_tensor
    (x y : ๐•ƒ)
    : mon_functor_tensor (linear_category_bang_functor ๐•ƒ) x y
        ยท linear_category_counit ๐•ƒ (x โŠ— y)
      = linear_category_counit ๐•ƒ x #โŠ— linear_category_counit ๐•ƒ y
          ยท mon_lunitor (monoidal_unit ๐•ƒ).
  Show proof.
    exact (pr1 (pr222 (pr222 (pr222 (pr222 ๐•ƒ)))) x y).

  Proposition linear_category_counit_preserves_unit
    : mon_functor_unit (linear_category_bang_functor ๐•ƒ)
        ยท linear_category_counit ๐•ƒ I_{๐•ƒ}
      = identity I_{๐•ƒ}.
  Show proof.
    exact (pr2 (pr222 (pr222 (pr222 (pr222 ๐•ƒ))))).

End AccessorsLaws.

3. Other accessors for linear categories
Definition linear_category_cocommutative_comonoid
           (๐•ƒ : linear_category)
           (x : ๐•ƒ)
  : commutative_comonoid ๐•ƒ.
Show proof.
  use make_commutative_comonoid.
  - exact (linear_category_bang ๐•ƒ x).
  - exact (linear_category_comult ๐•ƒ x).
  - exact (linear_category_counit ๐•ƒ x).
  - exact (linear_category_counitality x).
  - exact (!(linear_category_coassoc x)).
  - exact (linear_category_cocommutative x).

Proposition linear_category_counit_comonoid_mor_struct
            (๐•ƒ : linear_category)
            (x : ๐•ƒ)
  : comonoid_mor_struct
      ๐•ƒ
      (linear_category_cocommutative_comonoid ๐•ƒ x)
      (linear_category_cocommutative_comonoid ๐•ƒ
         (linear_category_cocommutative_comonoid ๐•ƒ x))
      (ฮด (linear_category_bang ๐•ƒ) x).
Show proof.
  use make_is_comonoid_mor ; cbn.
  - exact (!(linear_category_counit_comonoid_mor_comult x)).
  - rewrite id_right.
    exact (!(linear_category_counit_comonoid_mor_counit x)).

Definition linear_category_comult_nat_trans
           (๐•ƒ : linear_category)
  : linear_category_bang ๐•ƒ
    โŸน
    linear_category_bang ๐•ƒโˆ™ diag_functor ๐•ƒ.
Show proof.
  use make_nat_trans.
  - exact (ฮป x, linear_category_comult ๐•ƒ x).
  - abstract
      (intros x y f ; cbn ;
       apply linear_category_comult_nat).

Definition linear_category_counit_nat_trans
           (๐•ƒ : linear_category)
  : linear_category_bang ๐•ƒ โŸน constant_functor _ _ I_{๐•ƒ}.
Show proof.
  use make_nat_trans.
  - exact (ฮป x, linear_category_counit ๐•ƒ x).
  - abstract
      (intros x y f ; cbn ;
       rewrite id_right ;
       apply linear_category_counit_nat).

Definition linear_category_comult_is_mon_nat_trans
  (๐•ƒ : linear_category):
  is_mon_nat_trans (linear_category_bang_functor ๐•ƒ)
    (comp_fmonoidal_lax (linear_category_bang_functor ๐•ƒ) (diag_functor_fmonoidal_lax ๐•ƒ))
    (linear_category_comult_nat_trans ๐•ƒ).
Show proof.
  split.
  - intros x y. apply linear_category_comult_preserves_tensor.
  - apply linear_category_comult_preserves_unit.

Definition linear_category_counit_is_mon_nat_trans
  (๐•ƒ : linear_category):
  is_mon_nat_trans (linear_category_bang_functor ๐•ƒ)
    (constant_functor_fmonoidal_lax _ (unit_monoid ๐•ƒ)) (linear_category_counit_nat_trans ๐•ƒ).
Show proof.
  split.
  - intros x y. apply linear_category_counit_preserves_tensor.
  - apply linear_category_counit_preserves_unit.

Definition linear_category_comult_coalgebra_morphism
  (๐•ƒ : linear_category) (x : ๐•ƒ)
  : CoAlg_category (linear_category_bang ๐•ƒ)
        โŸฆ ((linear_category_bang ๐•ƒ) x) ,, ฮด (linear_category_bang ๐•ƒ) x,
          (linear_category_bang ๐•ƒ x โŠ— linear_category_bang ๐•ƒ x ,,
             (ฮด (linear_category_bang ๐•ƒ) x #โŠ— ฮด (linear_category_bang ๐•ƒ) x)
             ยท mon_functor_tensor (linear_category_bang_functor ๐•ƒ) _ _ )โŸง.
Show proof.
  use tpair.
  - exact (linear_category_comult ๐•ƒ x).
  - abstract (cbn; rewrite assoc; apply pathsinv0, linear_category_comult_coalgebra_mor).

Definition linear_category_counit_coalgebra_morphism
  (๐•ƒ : linear_category) (x : ๐•ƒ)
  : CoAlg_category (linear_category_bang ๐•ƒ)
        โŸฆ ((linear_category_bang ๐•ƒ) x) ,, ฮด (linear_category_bang ๐•ƒ) x,
          (I_{๐•ƒ} ,, mon_functor_unit (linear_category_bang_functor ๐•ƒ)) โŸง.
Show proof.
  use tpair.
  - exact (linear_category_counit ๐•ƒ x).
  - abstract (apply pathsinv0, linear_category_counit_coalgebra_mor).