Library interfaces.MonoidalCategory

Require Import interfaces.Category.
Require Import interfaces.Functor.

Monoidal structures

Since a given category may involve several monoidal structure, we separate the corresponding interface into a submodule.

Module Type MonoidalStructure (C : Category).
  Import C.

  Include Bifunctor C C C.

  Parameter unit : C.t.
  Parameter assoc : ∀ A B C, C.iso (omap A (omap B C)) (omap (omap A B) C).
  Parameter lunit : ∀ A, C.iso (omap unit A) A.
  Parameter runit : ∀ A, C.iso (omap A unit) A.

Naturality properties

  Axiom assoc_nat :
    ∀ {A1 B1 C1 A2 B2 C2: C.t} (f: C.m A1 A2) (g: C.m B1 B2) (h: C.m C1 C2),
      fmap (fmap f g) h @ assoc A1 B1 C1 = assoc A2 B2 C2 @ fmap f (fmap g h).

  Axiom lunit_nat :
    ∀ {A1 A2 : C.t} (f : C.m A1 A2),
      f @ lunit A1 = lunit A2 @ fmap (C.id unit) f.

  Axiom runit_nat :
    ∀ {A1 A2 : C.t} (f : C.m A1 A2),
      f @ runit A1 = runit A2 @ fmap f (C.id unit).

Pentagon identity

  Axiom assoc_coh :
    ∀ A B C D : C.t,
      fmap (assoc A B C) (C.id D) @
        assoc A (omap B C) D @
        fmap (C.id A) (assoc B C D) =
      assoc (omap A B) C D @
        assoc A B (omap C D).

Triangle identity

  Axiom unit_coh :
    ∀ A B : C.t,
      fmap (runit A) (C.id B) @ assoc A unit B =
      fmap (C.id A) (lunit B).

End MonoidalStructure.

Then a monoidal category is a category with a submodule for a tensor product.

Module Type MonoidalDefinition (C : Category).
  Declare Module Tens : MonoidalStructure C.
End MonoidalDefinition.

Module MonoidalTheory (C : Category) (M : MonoidalDefinition C).
  Import C M.

  Notation "1" := Tens.unit : obj_scope.
  Infix "×" := Tens.omap : obj_scope.
  Infix "×" := Tens.fmap : hom_scope.
  Notation α := Tens.assoc.
  Notation λ := Tens.lunit.
  Notation ρ := Tens.runit.

End MonoidalTheory.

Module Type Monoidal (C : Category) :=
  MonoidalDefinition C <+
  MonoidalTheory C.

Module Type MonoidalCategory :=
  Category.Category <+
  Monoidal.

Monoidal closure

Module Type MonoidalClosureDefinition (C : Category) (M : MonoidalStructure C).
  Import C.
  Infix "×" := M.omap : obj_scope.
  Infix "×" := M.fmap : hom_scope.

  Include Bifunctor C.Op C C.

  Parameter curry : ∀ {A B C}, (M.omap A B ~~> C ) → (A ~~> omap B C ).
  Parameter uncurry : ∀ {A B C}, (A ~~> omap B C ) → (M.omap A B ~~> C ).

  Axiom uncurry_curry :
    ∀ {A B C} (f : A × B ~~> C), uncurry (curry f) = f.
  Axiom curry_uncurry :
    ∀ {A B C} (g : A ~~> omap B C), curry (uncurry g) = g.

  Axiom curry_natural_l :
    ∀ {A1 A2 B C} (x : A1 ~~> A2) (f : A2 × B ~~> C),
      curry (f @ (x × id B )) = curry f @ x.
  Axiom curry_natural_r :
    ∀ {A B C1 C2} (f : A × B ~~> C1) (y : C1 ~~> C2),
      curry (y @ f) = fmap (id B) y @ curry f.

End MonoidalClosureDefinition.

Module MonoidalClosureTheory (C : Category) (M : MonoidalStructure C)
  (W : MonoidalClosureDefinition C M).

  Import C W.

  Theorem curry_natural :
    ∀ {A1 A2 B C1 C2} (x : A1 ~~> A2) (f : A2 × B ~~> C1) (y : C1 ~~> C2),
      curry (y @ f @ (x × id B )) = fmap (id B) y @ curry f @ x.

  (* Theorem uncurry_natural :
    .... *)

End MonoidalClosureTheory.

Cartesian monoidal structures

Definition

Module Type CartesianStructureDefinition (C : Category).
Import C.

Terminal object

  Parameter unit : t.
  Parameter ter : ∀ X, C.m X unit.

  Axiom ter_uni : ∀ {X} (x y : C.m X unit), x = y.

Binary products

  Parameter omap : t → t → t.
  Parameter p1 : ∀ {A B}, m (omap A B) A.
  Parameter p2 : ∀ {A B}, m (omap A B) B.
  Parameter pair : ∀ {X A B}, m X A → m X B → m X (omap A B).

  Axiom p1_pair : ∀ {X A B} (f : m X A) (g : m X B), p1 @ pair f g = f.
  Axiom p2_pair : ∀ {X A B} (f : m X A) (g : m X B), p2 @ pair f g = g.
  Axiom pair_pi : ∀ {X A B} x, @pair X A B (p1 @ x) (p2 @ x) = x.

End CartesianStructureDefinition.

Consequences

We show in particular that cartesian structures are a special case of monoidal structure. Note that we cannot include BifunctorTheory until the omap field from CartesianStructureDefinition and the fmap field from CartesianStructureTheory have been consolidated into a single module. As a result we need to defer this until we define the overall CartesianStructure interface.

Module CartesianStructureTheory (C : Category) (P : CartesianStructureDefinition C).

Import C P.

Useful lemmas

  Lemma p1_pair_rewrite {X A B Y} (f : m X A) (g : m X B) (x : m Y X) :
    p1 @ pair f g @ x = f @ x.

  Lemma p2_pair_rewrite {X A B Y} (f : m X A) (g : m X B) (x : m Y X) :
    p2 @ pair f g @ x = g @ x.

  Lemma pair_uni {X A B} (x : m X (omap A B)) (f : m X A) (g : m X B) :
    p1 @ x = f →
    p2 @ x = g →
    x = pair f g.

  Lemma pair_compose {X A B Y} (f : m X A) (g : m X B) (x : m Y X) :
    pair f g @ x = pair (f @ x) (g @ x).

  Global Hint Rewrite
    @p1_pair @p1_pair_rewrite
    @p2_pair @p2_pair_rewrite
    @pair_compose @compose_assoc : pair.

Bifunctor structure

  Definition fmap {A1 A2 B1 B2} (f1 : m A1 B1) (f2 : m A2 B2) :=
    pair (f1 @ p1) (f2 @ p2).

  Proposition fmap_id (A B : t) :
    fmap (id A) (id B) = id (omap A B).

  Proposition fmap_compose {A1 A2 B1 B2 C1 C2} :
    ∀ (g1 : m B1 C1) (g2 : m B2 C2) (f1: m A1 B1) (f2: m A2 B2),
      fmap (g1 @ f1) (g2 @ f2) = fmap g1 g2 @ fmap f1 f2.

Monoidal structure

  Program Definition assoc (A B C : t) : C.iso (A & (B & C )) ((A & B ) & C) :=
    {|
      fw := pair (pair p1 (p1 @ p2)) (p2 @ p2);
      bw := pair (p1 @ p1) (pair (p2 @ p1) p2);
    |}.

  Program Definition lunit (A : t) : iso (unit & A) A :=
    {|
      fw := p2;
      bw := pair (ter A) (id A);
    |}.

  Program Definition runit (A : t) : iso (A & unit) A :=
    {|
      fw := p1;
      bw := pair (id A) (ter A);
    |}.

Naturality

  Proposition assoc_nat {A1 B1 C1 A2 B2 C2} f g h :
    ((f & g ) & h ) @ assoc A1 B1 C1 = assoc A2 B2 C2 @ (f & (g & h )).

  Proposition lunit_nat {A1 A2 : C.t} (f : C.m A1 A2) :
    f @ lunit A1 = lunit A2 @ fmap (C.id unit) f.

  Proposition runit_nat {A1 A2 : C.t} (f : C.m A1 A2) :
    f @ runit A1 = runit A2 @ fmap f (C.id unit).

Pentagon diagram

  Proposition assoc_coh (A B C D : t) :
    (assoc A B C & id D ) @ assoc A (B & C) D @ (id A & assoc B C D ) =
    assoc (A & B) C D @ assoc A B (C & D).

Triangle diagram

Proposition unit_coh (A B : t) :
(runit A & id B ) @ assoc A unit B = id A & lunit B.

End CartesianStructureTheory.

Once we add in the definitions provided by BifunctorTheory, we can check the result against MonoidalStructure.

Module Type CartesianStructure (C : Category) <: MonoidalStructure C :=
  CartesianStructureDefinition C <+
  CartesianStructureTheory C <+
  BifunctorTheory C C C.

Cartesian category interface

Module Type CartesianDefinition (C : Category).
  Declare Module Prod : CartesianStructure C.
End CartesianDefinition.

Module CartesianTheory (C : Category) (M : CartesianDefinition C).
  Import C M.
  Notation T := Prod.unit.
  Infix "&&" := Prod.omap (at level 40, left associativity) : obj_scope.
  Infix "&&" := Prod.fmap : hom_scope.
End CartesianTheory.

Module Type Cartesian (C : Category) :=
  CartesianDefinition C <+
  CartesianTheory C.

Module Type CartesianCategory :=
  Category.Category <+
  Cartesian.

Monoidal functors

Module Type FunctorMonoidal (C D : Category) (CM : MonoidalStructure C)
  (DM : MonoidalStructure D) (F : Functor C D).

  Import (coercions, notations) D.

  Parameter omap_unit :
    D.iso DM.unit (F.omap CM.unit).

  Parameter omap_prod :
    ∀ X Y, D.iso (DM.omap (F.omap X) (F.omap Y)) (F.omap (CM.omap X Y)).

  Parameter omap_prod_nat :
    ∀ {X1 X2 Y1 Y2} (f : C.m X1 X2) (g : C.m Y1 Y2),
      omap_prod X2 Y2 @ DM.fmap (F.fmap f) (F.fmap g) =
      F.fmap (CM.fmap f g) @ omap_prod X1 Y1.

End FunctorMonoidal.

Module Type MonoidalFunctor (C D : MonoidalCategory) :=
  Functor.Functor C D <+
  FunctorMonoidal C D C.Tens D.Tens.