Show category of maps is monoidal

1 files changed, 166 insertions, 0 deletions

diff --git a/Category/Semiadditive/Monoidal.agda b/Category/Semiadditive/Monoidal.agda
new file mode 100644
index 0000000..3a4a3b7
--- /dev/null
+++ b/Category/Semiadditive/Monoidal.agda
@@ -0,0 +1,166 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+open import Category.Semiadditive using (Semiadditive)
+open import Level using (Level)
+
+module Category.Semiadditive.Monoidal {o ℓ e : Level} {𝒞 : Category o ℓ e} (semiadditive : Semiadditive 𝒞) where
+
+open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Braided using (Braided)
+open import Categories.Category.Monoidal.Symmetric using (Symmetric)
+open import Categories.Functor.Bifunctor using (flip-bifunctor)
+open import Categories.Morphism 𝒞 using (_≅_)
+open import Categories.Morphism.Reasoning 𝒞
+open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper)
+
+open Category 𝒞
+open Equiv
+open HomReasoning
+open Semiadditive semiadditive
+
+-- Structure isomorphisms
+
+unitorˡ : {X : Obj} → 𝟘 ⊕ X ≅ X
+unitorˡ {X} = record
+    { from = π₂
+    ; to = i₂
+    ; iso = record
+        { isoˡ = sym (⟨⟩-unique !-unique₂ (pullˡ π₂∘i₂≈id)) ○ id×₁id
+        ; isoʳ = π₂∘i₂≈id
+        }
+    }
+
+unitorʳ : {X : Obj} → X ⊕ 𝟘 ≅ X
+unitorʳ {X} = record
+    { from = π₁
+    ; to = i₁
+    ; iso = record
+        { isoˡ = sym (⟨⟩-unique (pullˡ π₁∘i₁≈id) !-unique₂) ○ id×₁id
+        ; isoʳ = π₁∘i₁≈id
+        }
+    }
+
+associator : {X Y Z : Obj} → (X ⊕ Y) ⊕ Z ≅ X ⊕ (Y ⊕ Z)
+associator = record
+    { from = assocˡ
+    ; to = assocʳ
+    ; iso = record
+        { isoˡ = assocʳ∘assocˡ
+        ; isoʳ = assocˡ∘assocʳ
+        }
+    }
+
+braiding : -×- ≃ flip-bifunctor -×-
+braiding = niHelper record
+    { η = λ _ → swap
+    ; η⁻¹ = λ _ → swap
+    ; commute = λ _ → swap∘×₁
+    ; iso = λ X → record
+        { isoˡ = swap∘swap
+        ; isoʳ = swap∘swap
+        }
+    }
+
+-- Naturality conditions
+
+unitorˡ-commute-to
+    : {X Y : Obj}
+      {f : X ⇒ Y}
+    → i₂ ∘ f
+    ≈ id ×₁ f ∘ i₂ {𝟘} {X}
+unitorˡ-commute-to {f = f} = sym +₁∘i₂ ○ sym (×₁-+₁ id f) ⟩∘⟨refl
+
+unitorʳ-commute-to
+    : {X Y : Obj}
+      {f : X ⇒ Y}
+    → i₁ ∘ f
+    ≈ f ×₁ id ∘ i₁ {X} {𝟘}
+unitorʳ-commute-to {f = f} = sym +₁∘i₁ ○ sym (×₁-+₁ f id) ⟩∘⟨refl
+
+-- Coherence conditions
+
+triangle
+    : {X Y : Obj}
+    → id ×₁ π₂ ∘ assocˡ {X} {𝟘} {Y} ≈ π₁ ×₁ id
+triangle {X} {Y} = begin
+    id ×₁ π₂ ∘ assocˡ                   ≈⟨ second∘⟨⟩ ⟩
+    ⟨ π₁ ∘ π₁ , π₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ ⟨⟩-congˡ (project₂ ○ (sym identityˡ)) ⟩
+    π₁ ×₁ id                            ∎
+
+pentagon
+    : {W X Y Z : Obj}
+    → id {W} ×₁ assocˡ {X} {Y} {Z} ∘ assocˡ ∘ assocˡ ×₁ id ≈ assocˡ ∘ assocˡ
+pentagon {W} {X} {Y} {Z} = begin
+    id ×₁ assocˡ ∘ assocˡ ∘ assocˡ ×₁ id                                        ≈⟨ pullˡ second∘⟨⟩ ⟩
+    ⟨ π₁ ∘ π₁ , assocˡ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ assocˡ ×₁ id                      ≈⟨ ⟨⟩∘ ⟩
+    ⟨ (π₁ ∘ π₁) ∘ assocˡ ×₁ id , (assocˡ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ assocˡ ×₁ id ⟩   ≈⟨ ⟨⟩-congʳ (pullʳ π₁∘×₁) ⟩
+    ⟨ π₁ ∘ assocˡ ∘ π₁ , (assocˡ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ _ ×₁ id ⟩                ≈⟨ ⟨⟩-congʳ (extendʳ project₁) ⟩
+    ⟨ π₁ ∘ π₁ ∘ π₁ , (assocˡ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ assocˡ ×₁ id ⟩               ≈⟨ ⟨⟩-congˡ (⟨⟩∘ ⟩∘⟨refl)⟩
+    ⟨ π₁ ∘ _ , ⟨ (π₁ ∘ π₁) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ , _ ∘ _ ⟩ ∘ _ ×₁ id ⟩             ≈⟨ ⟨⟩-congˡ (⟨⟩-congʳ (pullʳ project₁) ⟩∘⟨refl) ⟩
+    ⟨ π₁ ∘ _ , ⟨ π₁ ∘ π₂ ∘ π₁  , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ ⟨ _ , π₂ ⟩ ⟩ ∘ _ ⟩          ≈⟨ ⟨⟩-congˡ (⟨⟩-congˡ ⟨⟩∘ ⟩∘⟨refl) ⟩
+    ⟨ π₁ ∘ _ , ⟨ π₁ ∘ _  , ⟨ (π₂ ∘ π₁) ∘ ⟨ _ , π₂ ⟩ , π₂ ∘ ⟨ _ , π₂ ⟩ ⟩ ⟩ ∘ _ ⟩ ≈⟨ ⟨⟩-congˡ (⟨⟩-congˡ (⟨⟩-cong₂ (pullʳ project₁) project₂) ⟩∘⟨refl) ⟩
+    ⟨ π₁ ∘ π₁ ∘ π₁ , ⟨ π₁ ∘ π₂ ∘ π₁ , ⟨ π₂ ∘ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ assocˡ ×₁ id ⟩  ≈⟨ ⟨⟩-congˡ ⟨⟩∘ ⟩
+    ⟨ π₁ ∘ π₁ ∘ π₁ , ⟨ (π₁ ∘ π₂ ∘ π₁) ∘ _ ×₁ id , ⟨ _ , π₂ ⟩ ∘ assocˡ ×₁ id ⟩ ⟩ ≈⟨ ⟨⟩-congˡ (⟨⟩-congʳ (pullʳ (pullʳ π₁∘×₁))) ⟩
+    ⟨ π₁ ∘ π₁ ∘ π₁ , ⟨ π₁ ∘ π₂ ∘ assocˡ ∘ π₁  , ⟨ _ , π₂ ⟩ ∘ assocˡ ×₁ id ⟩ ⟩   ≈⟨ ⟨⟩-congˡ (⟨⟩-congʳ (refl⟩∘⟨ pullˡ project₂)) ⟩
+    ⟨ π₁ ∘ π₁ ∘ π₁ , ⟨ π₁ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ π₁  , ⟨ _ , π₂ ⟩ ∘ _ ×₁ id ⟩ ⟩   ≈⟨ ⟨⟩-congˡ (⟨⟩-congʳ (extendʳ project₁)) ⟩
+    ⟨ π₁ ∘ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ ∘ π₁ , ⟨ π₂ ∘ π₂ ∘ π₁ , π₂ ⟩ ∘ assocˡ ×₁ id ⟩ ⟩  ≈⟨ ⟨⟩-congˡ (⟨⟩-congˡ ⟨⟩∘) ⟩
+    ⟨ π₁ ∘ _ , ⟨ _ , ⟨ (π₂ ∘ π₂ ∘ π₁) ∘ assocˡ ×₁ id , π₂ ∘ assocˡ ×₁ id ⟩ ⟩ ⟩  ≈⟨ ⟨⟩-congˡ (⟨⟩-congˡ (⟨⟩-cong₂ (pullʳ (pullʳ π₁∘×₁)) π₂∘first)) ⟩
+    ⟨ π₁ ∘ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ ∘ π₁ , ⟨ π₂ ∘ π₂ ∘ assocˡ ∘ π₁ , π₂ ⟩ ⟩ ⟩        ≈⟨ ⟨⟩-congˡ (⟨⟩-congˡ (⟨⟩-congʳ (refl⟩∘⟨ pullˡ project₂))) ⟩
+    ⟨ π₁ ∘ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ ∘ π₁ , ⟨ π₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ π₁ , π₂ ⟩ ⟩ ⟩   ≈⟨ ⟨⟩-congˡ (⟨⟩-congˡ (⟨⟩-congʳ (pullˡ project₂))) ⟩
+    ⟨ π₁ ∘ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ⟩                      ≈⟨ ⟨⟩-cong₂ (pullʳ project₁) (⟨⟩-cong₂ (pullʳ project₁) project₂) ⟨
+    ⟨ (π₁ ∘ π₁) ∘ assocˡ , ⟨ (π₂ ∘ π₁) ∘ assocˡ , π₂ ∘ assocˡ ⟩ ⟩               ≈⟨ ⟨⟩-congˡ ⟨⟩∘ ⟨
+    ⟨ (π₁ ∘ π₁) ∘ assocˡ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ assocˡ ⟩                          ≈⟨ ⟨⟩∘ ⟨
+    assocˡ ∘ assocˡ                                                             ∎
+
+hexagon₁ : {X Y Z : Obj} → id ×₁ swap ∘ assocˡ {X} {Y} {Z} ∘ swap ×₁ id ≈ assocˡ ∘ swap ∘ assocˡ
+hexagon₁ = begin
+    id ×₁ swap ∘ assocˡ ∘ swap ×₁ id                          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congʳ ⟨⟩∘ ⟩
+    id ×₁ swap ∘ assocˡ ∘ ⟨ ⟨ π₂ ∘ π₁ , π₁ ∘ π₁ ⟩ , id ∘ π₂ ⟩ ≈⟨ refl⟩∘⟨ assocˡ∘⟨⟩ ⟩
+    id ×₁ swap ∘ ⟨ π₂ ∘ π₁ , ⟨ π₁ ∘ π₁ , id ∘ π₂ ⟩ ⟩          ≈⟨ ×₁∘⟨⟩ ⟩
+    ⟨ id ∘ π₂ ∘ π₁ , swap ∘ ⟨ π₁ ∘ π₁ , id ∘ π₂ ⟩ ⟩           ≈⟨ ⟨⟩-cong₂ identityˡ swap∘⟨⟩ ⟩
+    ⟨ π₂ ∘ π₁ , ⟨ id ∘ π₂ , π₁ ∘ π₁ ⟩ ⟩                       ≈⟨ ⟨⟩-congˡ (⟨⟩-congʳ identityˡ) ⟩
+    ⟨ π₂ ∘ π₁ , ⟨ π₂ , π₁ ∘ π₁ ⟩ ⟩                            ≈⟨ assocˡ∘⟨⟩ ⟨
+    assocˡ ∘ ⟨ ⟨ π₂ ∘ π₁ , π₂ ⟩ , π₁ ∘ π₁ ⟩                   ≈⟨ refl⟩∘⟨ swap∘⟨⟩ ⟨
+    assocˡ ∘ swap ∘ assocˡ                                    ∎
+
+hexagon₂ : {X Y Z : Obj} → (swap ×₁ id ∘ assocʳ {X} {Y} {Z}) ∘ id ×₁ swap ≈ (assocʳ ∘ swap) ∘ assocʳ
+hexagon₂ {X} {Y} {Z} = begin
+    (swap ×₁ id ∘ assocʳ) ∘ id ×₁ swap                        ≈⟨ pullʳ (refl⟩∘⟨ ⟨⟩-congˡ ⟨⟩∘) ⟩
+    swap ×₁ id ∘ assocʳ ∘ ⟨ id ∘ π₁ , ⟨ π₂ ∘ π₂ , π₁ ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ assocʳ∘⟨⟩ ⟩
+    swap ×₁ id ∘ ⟨ ⟨ id ∘ π₁ , π₂ ∘ π₂ ⟩ , π₁ ∘ π₂ ⟩          ≈⟨ first∘⟨⟩ ⟩
+    ⟨ swap ∘ ⟨ id ∘ π₁ , π₂ ∘ π₂ ⟩ , π₁ ∘ π₂ ⟩                ≈⟨ ⟨⟩-congʳ swap∘⟨⟩ ⟩
+    ⟨ ⟨ π₂ ∘ π₂ , id ∘ π₁ ⟩ , π₁ ∘ π₂ ⟩                       ≈⟨ ⟨⟩-congʳ (⟨⟩-congˡ identityˡ) ⟩
+    ⟨ ⟨ π₂ ∘ π₂ , π₁ ⟩ , π₁ ∘ π₂ ⟩                            ≈⟨ assocʳ∘⟨⟩ ⟨
+    assocʳ ∘ ⟨ π₂ ∘ π₂ , ⟨ π₁ , π₁ ∘ π₂ ⟩ ⟩                   ≈⟨ pushʳ (sym swap∘⟨⟩) ⟩
+    (assocʳ ∘ swap) ∘ assocʳ                                  ∎
+
+monoidal : Monoidal 𝒞
+monoidal = record
+    { ⊗ = -×-
+    ; unit = 𝟘
+    ; unitorˡ = unitorˡ
+    ; unitorʳ = unitorʳ
+    ; associator = associator
+    ; unitorˡ-commute-from = π₂∘×₁
+    ; unitorˡ-commute-to = unitorˡ-commute-to
+    ; unitorʳ-commute-from = π₁∘×₁
+    ; unitorʳ-commute-to = unitorʳ-commute-to
+    ; assoc-commute-from = assocˡ∘×₁
+    ; assoc-commute-to = assocʳ∘×₁
+    ; triangle = triangle
+    ; pentagon = pentagon
+    }
+
+braided : Braided monoidal
+braided = record
+    { braiding = braiding
+    ; hexagon₁ = hexagon₁
+    ; hexagon₂ = hexagon₂
+    }
+
+symmetric : Symmetric monoidal
+symmetric = record
+    { braided = braided
+    ; commutative = swap∘swap
+    }