{-# 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
    }