Library UniMath.Semantics.LinearLogic.LinearToLinearNonLinear

In this file, we show how any linear category induces a linear/non-linear model. This boils down to proving that the Eilenberg-Moore category of the (symmetric monoidal) comonad, given by a linear category, is cartesian monoidal.

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Monads.Comonads.
Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors.
Require Import UniMath.CategoryTheory.Monoidal.Categories.
Require Import UniMath.CategoryTheory.Monoidal.Functors.
Require Import UniMath.CategoryTheory.Monoidal.Adjunctions.
Require Import UniMath.CategoryTheory.Monoidal.FunctorCategories.
Require Import UniMath.CategoryTheory.Monoidal.Structure.Cartesian.
Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric.
Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed.
Require Import UniMath.CategoryTheory.Monoidal.Structure.SymmetricDiagonal.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
Require Import UniMath.CategoryTheory.categories.Dialgebras.

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

Require Import UniMath.CategoryTheory.Monoidal.Comonoids.Category.
Require Import UniMath.CategoryTheory.Monoidal.Comonoids.MonoidalCartesianBuilder.
Require Import UniMath.CategoryTheory.Monoidal.Comonoids.TransportComonoidAlongRetraction.

Require Import UniMath.CategoryTheory.categories.CoEilenbergMoore.
Require Import UniMath.CategoryTheory.Monoidal.Examples.MonoidalDialgebras.
Require Import UniMath.CategoryTheory.Monoidal.Examples.SymmetricMonoidalCoEilenbergMoore.

Require Import UniMath.Semantics.LinearLogic.LinearCategory.
Require Import UniMath.Semantics.LinearLogic.LinearCategoryEilenbergMooreAdjunction.
Require Import UniMath.Semantics.LinearLogic.LinearNonLinear.

Import MonoidalNotations.

Local Open Scope cat.
Local Open Scope moncat.

Import ComonoidNotations.

Section LiftingPropertyCoalgebraMorSection.

  Lemma postcomp_with_section_reflect_coalg_mor
    (๐•ƒ : linear_category)
    (xx aa bb : sym_monoidal_cat_co_eilenberg_moore (linear_category_bang ๐•ƒ))
    (i : aa --> bb)
    (f : ๐•ƒโŸฆpr11 xx, pr11 aaโŸง)
    (f_i_coalg : pr21 xx ยท #(linear_category_bang ๐•ƒ) (f ยท pr11 i) = (f ยท pr11 i) ยท pr21 bb)
    (r : ๐•ƒโŸฆpr11 bb, pr11 aaโŸง)
    (ir_id : is_retraction (pr11 i) r)
    : pr21 xx ยท #(linear_category_bang ๐•ƒ) f = f ยท pr21 aa.
  Show proof.
    pose (p := cancel_postcomposition _ _ (#(linear_category_bang ๐•ƒ) r) f_i_coalg).
    rewrite assoc' in p.
    rewrite <- functor_comp in p.
    rewrite assoc' in p.

    refine (_ @ p @ _).
    - do 2 apply maponpaths.
      refine (! id_right _ @ _).
      apply maponpaths.
      apply pathsinv0, ir_id.
    - rewrite ! assoc'.
      apply maponpaths.
      rewrite assoc.
      etrans. {
        apply maponpaths_2.
        exact (! pr21 i).
      }
      rewrite assoc'.
      rewrite <- functor_comp.
      refine (_ @ id_right _).
      apply maponpaths.
      refine (_ @ functor_id (linear_category_bang ๐•ƒ) _).
      apply maponpaths.
      exact ir_id.

  Definition lifting_is_coalg_mor
    {๐•ƒ : linear_category}
    {xx aa bb : sym_monoidal_cat_co_eilenberg_moore (linear_category_bang ๐•ƒ)}
    {g : xx --> bb} {i : aa --> bb} {f : ๐•ƒโŸฆpr11 xx, pr11 aaโŸง}
    {r : ๐•ƒโŸฆpr11 bb, pr11 aaโŸง}
    (ir_id : is_retraction (pr11 i) r)
    (p : f ยท pr11 i = pr11 g)
    : pr21 xx ยท #(linear_category_bang ๐•ƒ) f = f ยท pr21 aa.
  Show proof.
    use (postcomp_with_section_reflect_coalg_mor ๐•ƒ xx aa bb i f _ r ir_id).
    etrans. {
      do 2 apply maponpaths.
      exact p.
    }
    etrans.
    2: {
      apply maponpaths_2.
      exact (! p).
    }
    exact (pr21 g).

End LiftingPropertyCoalgebraMorSection.

Section TransportationFreeCoalgebraComonoid.

  Context (๐•ƒ : linear_category).
  Let bang : sym_monoidal_cmd ๐•ƒ
      := linear_category_bang ๐•ƒ.

  Context (xx : sym_monoidal_cat_co_eilenberg_moore (linear_category_bang ๐•ƒ)).
  Let x : ๐•ƒ := pr11 xx.
  Let hx : ๐•ƒโŸฆx, bang xโŸง := pr21 xx.

  Let comonoid_on_bang_x := linear_category_cocommutative_comonoid ๐•ƒ x.

  Lemma linear_category_comult_factors_through_comult_bang
    : ฮด (linear_category_bang ๐•ƒ) x
         ยท (linear_category_comult ๐•ƒ (bang x)
              ยท ฮต bang (bang x) #โŠ— ฮต bang (bang x))
       = linear_category_comult ๐•ƒ x.
  Show proof.
    rewrite assoc.
    etrans. {
      apply maponpaths_2.
      apply linear_category_counit_comonoid_mor_comult.
    }
    rewrite assoc'.
    rewrite <- tensor_comp_mor.
    refine (_ @ id_right _).
    apply maponpaths.
    rewrite <- tensor_id_id.
    use two_arg_paths ; apply Comonad_law1.

  Local Lemma transport_comonoid_from_free_lem
    : hx ยท ฮด_{comonoid_on_bang_x} ยท ฮต bang x #โŠ— ฮต bang x ยท hx #โŠ— hx
      = hx ยท ฮด_{comonoid_on_bang_x}.
  Show proof.
    cbn.
    etrans. {
      rewrite assoc'.
      apply maponpaths.
      rewrite <- tensor_comp_mor.
      apply maponpaths.
      apply pathsinv0.
      apply (pr2 (disp_ฮต _) _ _ hx).
    }
    etrans. {
      apply maponpaths.
      apply maponpaths_2.
      apply pathsinv0.
      apply (pr2 (disp_ฮต _) _ _ hx).
    }

    rewrite tensor_comp_mor.
    rewrite assoc.
    etrans. {
      apply maponpaths_2.
      rewrite assoc'.
      apply maponpaths.
      apply pathsinv0.
      apply linear_category_comult_nat.
    }
    rewrite assoc.
    etrans. {
      do 2 apply maponpaths_2.
      apply pathsinv0, (pr22 xx).
    }

    rewrite ! assoc'.
    apply maponpaths.
    exact linear_category_comult_factors_through_comult_bang.

  Definition transport_comonoid_struct_from_free
    : disp_cat_of_comonoids ๐•ƒ x.
  Show proof.
    use transported_comonoid.
    - exact comonoid_on_bang_x.
    - exact hx.
    - exact (ฮต (linear_category_bang ๐•ƒ) x).
    - exact (pr12 xx).
    - exact transport_comonoid_from_free_lem.

  Definition transport_comonoid_from_free
    : comonoid ๐•ƒ.
  Show proof.
    exists x.
    exact transport_comonoid_struct_from_free.

End TransportationFreeCoalgebraComonoid.

Section MakeComonoidInEilenbergMooreFromComonoidInLinear.

  Context (๐•ƒ : linear_category).

  Context (m : comonoid ๐•ƒ).

  Let bang := linear_category_bang ๐•ƒ.

  Context
    (x_b : ๐•ƒโŸฆm, bang mโŸง)
      (x_b_u : x_b ยท ฮต bang m = identity (pr1 m))
      (x_b_m : x_b ยท ฮด bang (pr1 m) = x_b ยท #bang x_b)
      (mx_t : x_b ยท #bang ฮด_{ m} = ฮด_{ m} ยท (x_b #โŠ— x_b ยท mon_functor_tensor (_ ,, lax_monoidal_from_symmetric_monoidal_comonad ๐•ƒ bang) m m))
      (mx_u : x_b ยท #bang ฮต_{ m} = ฮต_{ m} ยท mon_functor_unit (_ ,, lax_monoidal_from_symmetric_monoidal_comonad ๐•ƒ bang)).

  Definition make_comonoid_object_in_eilenberg_moore
    : sym_monoidal_cat_co_eilenberg_moore (linear_category_bang ๐•ƒ).
  Show proof.
    use make_ob_co_eilenberg_moore.
    - apply m.
    - exact x_b.
    - exact x_b_u.
    - exact x_b_m.

  Definition make_comonoid_struct_data_in_eilenberg_moore
    : disp_cat_of_comonoids_data (sym_monoidal_cat_co_eilenberg_moore (linear_category_bang ๐•ƒ))
        make_comonoid_object_in_eilenberg_moore.
  Show proof.
    use tpair.
    - use make_mor_co_eilenberg_moore.
      + exact ฮด_{m}.
      + abstract (
            refine (mx_t @ _);
            apply maponpaths;
            apply pathsinv0;
            refine (assoc' _ _ _ @ _);
            apply id_left).
    - use make_mor_co_eilenberg_moore.
      + exact ฮต_{m}.
      + abstract (
            refine (mx_u @ _);
        apply maponpaths;
        apply pathsinv0;
            apply id_left).

  Definition make_comonoid_laws_in_eilenberg_moore
    : comonoid_laws (sym_monoidal_cat_co_eilenberg_moore (linear_category_bang ๐•ƒ))
        (make_comonoid_object_in_eilenberg_moore ,, make_comonoid_struct_data_in_eilenberg_moore).
  Show proof.
    refine (_ ,, _ ,, _) ; use eq_mor_co_eilenberg_moore.
    - apply comonoid_to_law_unit_left.
    - apply comonoid_to_law_unit_right.
    - apply comonoid_to_law_assoc.

  Definition make_comonoid_in_eilenberg_moore
    : comonoid (sym_monoidal_cat_co_eilenberg_moore (linear_category_bang ๐•ƒ)).
  Show proof.
    exists make_comonoid_object_in_eilenberg_moore.
    exists make_comonoid_struct_data_in_eilenberg_moore.
    exact make_comonoid_laws_in_eilenberg_moore.

End MakeComonoidInEilenbergMooreFromComonoidInLinear.

Section ConstructionOfComonoidsInEilenbergMoore.

  Context (๐•ƒ : linear_category).

  Let EM := sym_monoidal_cat_co_eilenberg_moore (linear_category_bang ๐•ƒ).

  Let bang : sym_monoidal_cmd ๐•ƒ
      := linear_category_bang ๐•ƒ.

  Context (xx : EM).
  Let x : ๐•ƒ := pr11 xx.
  Let hx : ๐•ƒโŸฆx, bang xโŸง := pr21 xx.

  Lemma comonoid_in_eilenberg_moore_from_coalg_counit_alg_mor
    : hx ยท #bang ฮต_{transport_comonoid_from_free ๐•ƒ xx}
       = ฮต_{transport_comonoid_from_free ๐•ƒ xx}
           ยท mon_functor_unit (_,, lax_monoidal_from_symmetric_monoidal_comonad ๐•ƒ bang).
  Show proof.
    cbn.
    unfold transported_comonoid_counit_data.
    rewrite functor_comp.
    rewrite assoc.
    etrans. {
      apply maponpaths_2.
      apply pathsinv0.
      exact (pr22 xx).
    }

    do 2 rewrite assoc'.
    apply maponpaths.
    apply pathsinv0.
    apply linear_category_counit_coalgebra_mor.

  Lemma comonoid_in_eilenberg_moore_from_coalg_comult_alg_mor
    : hx ยท #bang ฮด_{transport_comonoid_from_free ๐•ƒ xx}
       = ฮด_{transport_comonoid_from_free ๐•ƒ xx}
           ยท (hx #โŠ— hx
     ยท mon_functor_tensor (_,,lax_monoidal_from_symmetric_monoidal_comonad ๐•ƒ (linear_category_bang ๐•ƒ)) x x).
  Show proof.
    assert (p : pr21 (xx โŠ— xx) = (hx #โŠ— hx
     ยท mon_functor_tensor
     (_,,lax_monoidal_from_symmetric_monoidal_comonad ๐•ƒ (linear_category_bang ๐•ƒ)) x x)).
    {
      refine (assoc' _ _ _ @ _).
      apply id_left.
    }
    rewrite <- p.

    assert (retr : is_retraction (hx #โŠ— hx) (ฮต bang x #โŠ— ฮต bang x)).
    {
      refine (! tensor_comp_mor _ _ _ _ @ _ @ tensor_id_id _ _).
      use two_arg_paths ; apply (pr2 xx).
    }

    use (lifting_is_coalg_mor
           (xx := xx)
           (aa := xx โŠ— xx)
           (bb := (eilenberg_moore_cofree ๐•ƒ x : EM) โŠ— (eilenberg_moore_cofree ๐•ƒ x : EM))
           (g := (hx ยท linear_category_comult ๐•ƒ x ,, _) ,, tt)
           (i := (hx #โŠ— hx,, _) ,, tt)
           (f := ฮด_{transport_comonoid_from_free ๐•ƒ xx})
           (r := ฮต bang x #โŠ— ฮต bang x)
           retr
        ).

    -
      cbn.
      unfold dialgebra_disp_tensor_op.
      cbn.
      rewrite id_left.
      rewrite ! assoc'.
      rewrite ! id_left.

      rewrite functor_comp.
      rewrite assoc.
      etrans. {
        apply maponpaths_2.
        exact (! pr22 xx).
      }

      etrans.
      2: {
        apply maponpaths.
        apply pathsinv0.
        exact (assoc _ _ _ @ linear_category_comult_coalgebra_mor x).
      }
      apply assoc'.

    - cbn.
      unfold dialgebra_disp_tensor_op.
      cbn.
      rewrite ! id_left.

      etrans. {
        rewrite assoc'.
        apply maponpaths.
        apply pathsinv0.
        apply (tensor_mon_functor_tensor (_ ,, lax_monoidal_from_symmetric_monoidal_comonad _ bang) hx hx).
      }

      do 2 rewrite assoc.
      apply maponpaths_2.
      refine (! tensor_comp_mor _ _ _ _ @ _ @ tensor_comp_mor _ _ _ _).
      use two_arg_paths ; exact (! pr22 xx).
    - apply transport_comonoid_from_free_lem.

  Definition comonoid_in_eilenberg_moore_from_coalg
    : comonoid EM.
  Show proof.
    use (make_comonoid_in_eilenberg_moore ๐•ƒ).
    - exact (transport_comonoid_from_free ๐•ƒ xx).
    - exact hx.
    - exact (pr12 xx).
    - exact (pr22 xx).
    - exact comonoid_in_eilenberg_moore_from_coalg_comult_alg_mor.
    - exact comonoid_in_eilenberg_moore_from_coalg_counit_alg_mor.

End ConstructionOfComonoidsInEilenbergMoore.

Section EilenbergMooreCartesian.

  Context (๐•ƒ : linear_category).

  Lemma comonoid_mor_in_eilenberg_moore
    {x y : sym_monoidal_cat_co_eilenberg_moore (linear_category_bang ๐•ƒ)}
    (f : x --> y)
    : comonoid_mor_struct
         (sym_monoidal_cat_co_eilenberg_moore (linear_category_bang ๐•ƒ))
         (comonoid_in_eilenberg_moore_from_coalg ๐•ƒ x)
         (comonoid_in_eilenberg_moore_from_coalg ๐•ƒ y)
         f.
  Show proof.
    use make_is_comonoid_mor.
    - use eq_mor_co_eilenberg_moore.
      cbn.
      unfold transported_comonoid_comult_data.
      cbn.
      refine (_ @ assoc' _ _ _).
      etrans.
      2: {
        apply maponpaths_2.
        rewrite assoc.
        apply maponpaths_2.
        exact (pr21 f).
      }
      rewrite ! assoc'.
      apply maponpaths.

      etrans.
      2: {
        rewrite assoc.
        apply maponpaths_2.
        exact (! linear_category_comult_nat (pr11 f)).
      }
      rewrite ! assoc'.
      apply maponpaths.
      rewrite tensor_mor_right.
      rewrite tensor_mor_left.
      etrans. {
        apply maponpaths.
        apply pathsinv0.
        apply tensor_split'.
      }
      refine (! tensor_comp_mor _ _ _ _ @ _).
      refine (_ @ tensor_comp_mor _ _ _ _).
      use two_arg_paths
      ; apply (! pr2 (disp_ฮต _) _ _ (pr11 f)).
    - use eq_mor_co_eilenberg_moore.
      refine (_ @ assoc' _ _ _).
      etrans.
      2: {
        apply maponpaths_2.
        exact (pr21 f).
      }
      rewrite id_right.
      cbn.
      unfold transported_comonoid_counit_data.
      rewrite assoc'.
      apply maponpaths.
      exact (! linear_category_counit_nat (pr11 f)).

  Local Lemma linear_category_eilenberg_moore_cartesian_lem
    (x y : sym_monoidal_cat_co_eilenberg_moore (linear_category_bang ๐•ƒ))
    :
    identity (pr11 x โŠ— pr11 y)
      ยท (pr21 x #โŠ— pr21 y)
      ยท fmonoidal_preservestensordata
      (lax_monoidal_from_symmetric_monoidal_comonad _ (linear_category_bang ๐•ƒ))
      (pr11 x) (pr11 y)
      ยท linear_category_comult ๐•ƒ (pr11 x โŠ— pr11 y)
      ยท ฮต (linear_category_bang ๐•ƒ) (pr11 x โŠ— pr11 y) #โŠ— ฮต (linear_category_bang ๐•ƒ) (pr11 x โŠ— pr11 y)
    = rightwhiskering_on_morphisms (pr1 ๐•ƒ) (pr11 y) _ _
        (pr21 x ยท linear_category_comult ๐•ƒ (pr11 x) ยท ฮต (linear_category_bang ๐•ƒ) (pr11 x) #โŠ— ฮต (linear_category_bang ๐•ƒ) (pr11 x))
        ยท leftwhiskering_on_morphisms (pr1 ๐•ƒ) (pr11 x โŠ— pr11 x) _ _
        (pr21 y ยท linear_category_comult ๐•ƒ (pr11 y)
           ยท ฮต (linear_category_bang ๐•ƒ) (pr11 y) #โŠ— ฮต (linear_category_bang ๐•ƒ) (pr11 y))
  ยท pr11 (inner_swap (sym_monoidal_cat_co_eilenberg_moore (linear_category_bang ๐•ƒ)) x x y y).
  Show proof.
    Opaque inner_swap.

    rewrite ! tensor_mor_right.
    rewrite ! tensor_mor_left.
    unfold dialgebra_disp_tensor_op.
    cbn.
    rewrite id_left.
    etrans.
    2: {
      apply maponpaths_2.
      apply tensor_split'.
    }
    etrans.
    2: {
      apply maponpaths_2.
      apply pathsinv0, tensor_comp_mor.
    }
    etrans.
    2: {
      do 2 apply maponpaths_2.
      apply pathsinv0, tensor_comp_mor.
    }

    rewrite ! assoc'.
    apply maponpaths.
    etrans.
    2: {
      apply maponpaths.
      apply naturality_inner_swap.
    }

    etrans.
    2: {
      do 2 apply maponpaths.
      etrans.
      2: {
        apply maponpaths.
        refine (_ @ id_right _).
        apply (symmetric_monoidal_comonad_extra_laws _ (linear_category_bang ๐•ƒ)).
      }
      apply maponpaths_2.
      refine (_ @ id_right _).
      apply (symmetric_monoidal_comonad_extra_laws _ (linear_category_bang ๐•ƒ)).
    }
    rewrite ! tensor_comp_mor.
    rewrite ! assoc.
    apply maponpaths_2.
    refine (linear_category_comult_preserves_tensor (pr11 x) (pr11 y) @ _).
    apply assoc.

  Definition linear_category_eilenberg_moore_cartesian
    : is_cartesian (sym_monoidal_cat_co_eilenberg_moore (linear_category_bang ๐•ƒ)).
  Show proof.
    use symm_monoidal_is_cartesian_from_comonoid.
    - intro ; apply comonoid_in_eilenberg_moore_from_coalg.
    - intro ; intros ; apply comonoid_mor_in_eilenberg_moore.
    - abstract (
          use eq_mor_co_eilenberg_moore;
          refine (assoc' _ _ _ @ _);
          refine (id_left _ @ _);
          apply linear_category_counit_preserves_unit).
    - intros x y.
      use eq_mor_co_eilenberg_moore.
      apply linear_category_eilenberg_moore_cartesian_lem.

End EilenbergMooreCartesian.

Section LinearToLNL.

  Context (๐•ƒ : linear_category).

  Local Definition em_projection
    : fmonoidal
        (sym_monoidal_cat_co_eilenberg_moore (linear_category_bang ๐•ƒ))
        ๐•ƒ
        (left_adjoint (eilenberg_moore_cmd_adj ๐•ƒ)).
  Show proof.
    use comp_fmonoidal.
    - apply mon_cat_co_eilenberg_moore_base.
    - apply projection_fmonoidal.
    - apply projection_fmonoidal.

  Local Lemma em_projection_is_symmetric
    : is_symmetric_monoidal_functor (sym_monoidal_cat_co_eilenberg_moore (linear_category_bang ๐•ƒ)) ๐•ƒ em_projection.
  Show proof.
    intros x y.
      etrans. {
        apply maponpaths.
        apply id_right.
      }
      refine (id_right _ @ _).
      cbn.
      refine (_ @ id_left _).
      rewrite id_right.
      apply pathsinv0.
      refine (id_left _ @ _).
      apply id_left.

  Definition linear_to_lnl
    : linear_non_linear_model.
  Show proof.
    use make_linear_non_linear_from_strong.
    - exact (linear_category_data_to_sym_mon_closed_cat ๐•ƒ).
    - exact (sym_monoidal_cat_co_eilenberg_moore (linear_category_bang ๐•ƒ)).
    - apply eilenberg_moore_cmd_adj.
    - apply linear_category_eilenberg_moore_cartesian.
    - exact em_projection.
    - exact em_projection_is_symmetric.

End LinearToLNL.