{-# OPTIONS --without-K --safe #-}

open import Level using (Level; suc; _⊔_)
open import Categories.Category using (Category)

module Category.Dagger.Semiadditive {o ℓ e : Level} (𝒞 : Category o ℓ e) where

import Categories.Morphism as Morphism
import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning
import Category.Semiadditive.Monoidal as SemiadditiveMonoidal

open import Categories.Category.Dagger using (HasDagger)
open import Categories.Category.Monoidal using (Monoidal)
open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory)
open import Categories.Functor.Bifunctor using (Bifunctor)
open import Categories.Morphism using (Iso)
open import Categories.Morphism.Properties 𝒞 using (Iso-resp-≈; Iso-swap)
open import Category.Dagger.2-Poset using (Dagger-2-Poset; Map; Maps; unitary-isMap)
open import Category.Semiadditive using (Semiadditive)
open import Data.Product using (_,_)
open import Relation.Binary using (Rel)
open import Relation.Binary.Morphism.Bundles using (PosetHomomorphism; mkPosetHomo)

record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where

  field
    semiadditive : Semiadditive 𝒞
    dagger : HasDagger 𝒞

  open Category 𝒞
  open HasDagger dagger public
  open Semiadditive semiadditive public

  field
    π₁† : {A B : Obj} → π₁ {A} {B} † ≈ i₁
    π₂† : {A B : Obj} → π₂ {A} {B} † ≈ i₂
    ⟨⟩-† : {A B C : Obj} {f : A ⇒ B} {g : A ⇒ C} → ⟨ f , g ⟩ † ≈ [ f † , g † ]

  open HomReasoning
  open ⇒-Reasoning

  Δ† : {A : Obj} → Δ {A} † ≈ ∇
  Δ† = begin
      ⟨ id , id ⟩ †   ≈⟨ ⟨⟩-† ⟩
      [ id † , id † ] ≈⟨ []-cong₂ †-identity †-identity ⟩
      [ id , id ]     ∎

  ∇† : {A : Obj} → ∇ {A} † ≈ Δ
  ∇† = begin
      ∇ †   ≈⟨ ⟨ Δ† ⟩† ⟨
      Δ † † ≈⟨ †-involutive Δ ⟩
      Δ     ∎

  i₁† : {A B : Obj} → i₁ {A} {B} † ≈ π₁
  i₁† = begin
      i₁ †    ≈⟨ ⟨ π₁† ⟩† ⟨
      π₁ † †  ≈⟨ †-involutive π₁ ⟩
      π₁      ∎

  i₂† : {A B : Obj} → i₂ {A} {B} † ≈ π₂
  i₂† = begin
      i₂ †    ≈⟨ ⟨ π₂† ⟩† ⟨
      π₂ † †  ≈⟨ †-involutive π₂ ⟩
      π₂      ∎

  module _ {A B C : Obj} where

    α⇒† : assocˡ {A} {B} {C} † ≈ assocʳ
    α⇒† = begin
        ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ †          ≈⟨ ⟨⟩-† ⟩
        [ (π₁ ∘ π₁) † , ⟨ π₂ ∘ π₁ , π₂ ⟩ † ]      ≈⟨ []-cong₂ †-homomorphism ⟨⟩-† ⟩
        [ π₁ † ∘ π₁ † , [ (π₂ ∘ π₁) † , π₂ † ] ]  ≈⟨ []-congˡ ([]-congʳ †-homomorphism) ⟩
        [ π₁ † ∘ π₁ † , [ π₁ † ∘ π₂ † , π₂ † ] ]  ≈⟨ []-cong₂ (π₁† ⟩∘⟨ π₁†) ([]-cong₂ (π₁† ⟩∘⟨ π₂†) π₂†) ⟩
        [ i₁ ∘ i₁ , [ i₁ ∘ i₂ , i₂ ] ]            ≈⟨ assocʳ≈+-assocʳ ⟨
        assocʳ                                    ∎

    α⇐† : assocʳ {A} {B} {C} † ≈ assocˡ
    α⇐† = begin
        assocʳ †    ≈⟨ ⟨ α⇒† ⟩† ⟨
        assocˡ † †  ≈⟨ †-involutive assocˡ ⟩
        assocˡ      ∎

  swap† : {A B : Obj} → swap {A} {B} † ≈ swap {B} {A}
  swap† {A} {B} = begin
      ⟨ π₂ , π₁ ⟩ †   ≈⟨ ⟨⟩-† ⟩
      [ π₂ † , π₁ † ] ≈⟨ []-cong₂ π₂† π₁† ⟩
      [ i₂ , i₁ ]     ≈⟨ swap≈+-swap ⟨
      ⟨ π₂ , π₁ ⟩     ∎

  †-resp-×₁ : {A B C D : Obj} {f : A ⇒ B} {g : C ⇒ D} → (f ×₁ g) † ≈ (f †) ×₁ (g †)
  †-resp-×₁ {f = f} {g} = begin
      ⟨ f ∘ π₁ , g ∘ π₂ ⟩ †       ≈⟨ ⟨⟩-† ⟩
      [ (f ∘ π₁) † , (g ∘ π₂) † ] ≈⟨ []-cong₂ †-homomorphism †-homomorphism ⟩
      [ π₁ † ∘ f † , π₂ † ∘ g † ] ≈⟨ []-cong₂ (π₁† ⟩∘⟨refl) (π₂† ⟩∘⟨refl) ⟩
      [ i₁ ∘ f † , i₂ ∘ g † ]     ≈⟨ ×₁-+₁ (f †) (g †) ⟨
      ⟨ f † ∘ π₁ , g † ∘ π₂ ⟩     ∎

  +-congˡ : {A B : Obj} {f g h : A ⇒ B} → g ≈ h → f + g ≈ f + h
  +-congˡ g≈h = +-cong Equiv.refl g≈h

  +-congʳ : {A B : Obj} {f g h : A ⇒ B} → f ≈ g → f + h ≈ g + h
  +-congʳ f≈g = +-cong f≈g Equiv.refl

  +-† : {A B : Obj} {f g : A ⇒ B} → (f + g) † ≈ (f †) + (g †)
  +-† {f = f} {g} = begin
      (∇ ∘ f ×₁ g ∘ Δ) †     ≈⟨ †-homomorphism ⟩
      (f ×₁ g ∘ Δ) † ∘ ∇ †   ≈⟨ pushˡ †-homomorphism ⟩
      Δ † ∘ (f ×₁ g) † ∘ ∇ † ≈⟨ Δ† ⟩∘⟨ †-resp-×₁ ⟩∘⟨ ∇† ⟩
      ∇ ∘ (f †) ×₁ (g †) ∘ Δ ∎

  -- bilinearity of composition
  ∘-distribˡ : {A B C : Obj} {f : B ⇒ C} {g h : A ⇒ B} → f ∘ (g + h) ≈ f ∘ g + f ∘ h
  ∘-distribˡ {f = f} {g} {h} = begin
      f ∘ (g + h)             ≈⟨ refl⟩∘⟨ identityʳ ⟨
      f ∘ (g + h) ∘ id        ≈⟨ +-resp-∘ ⟩
      f ∘ g ∘ id + f ∘ h ∘ id ≈⟨ +-cong (refl⟩∘⟨ identityʳ) (refl⟩∘⟨ identityʳ) ⟩
      f ∘ g + f ∘ h           ∎

  ∘-distribʳ : {A B C : Obj} {f g : B ⇒ C} {h : A ⇒ B} → (f + g) ∘ h ≈ f ∘ h + g ∘ h
  ∘-distribʳ {f = f} {g} {h} = begin
      (f + g) ∘ h             ≈⟨ pushˡ (Equiv.sym identityˡ) ⟩
      id ∘ (f + g) ∘ h        ≈⟨ +-resp-∘ ⟩
      id ∘ f ∘ h + id ∘ g ∘ h ≈⟨ +-cong (pullˡ identityˡ) (pullˡ identityˡ) ⟩
      f ∘ h + g ∘ h           ∎

  open SemiadditiveMonoidal semiadditive using (monoidal; symmetric)

  monoidalCategory : MonoidalCategory o ℓ e
  monoidalCategory = record
      { U = 𝒞
      ; monoidal = monoidal
      }

  symmetricMonoidalCategory : SymmetricMonoidalCategory o ℓ e
  symmetricMonoidalCategory = record
      { U = 𝒞
      ; monoidal = monoidal
      ; symmetric = symmetric
      }

record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where

  field
    semiadditiveDagger : SemiadditiveDagger

  open SemiadditiveDagger semiadditiveDagger public

  open Category 𝒞
  open HomReasoning
  open ⇒-Reasoning

  field
    idempotent : {A B : Obj} {f : A ⇒ B} → f + f ≈ f

  _≤_ : {A B : Obj} → Rel (A ⇒ B) e
  _≤_ {A} {B} f g = f + g ≈ g

  ≤-refl : {A B : Obj} {f : A ⇒ B} → f ≤ f
  ≤-refl = idempotent

  ≤-antisym : {A B : Obj} {f g : A ⇒ B} → f ≤ g → g ≤ f → f ≈ g
  ≤-antisym {A} {B} {f} {g} f≤g g≤f = begin
      f     ≈⟨ g≤f ⟨
      g + f ≈⟨ +-comm g f ⟩
      f + g ≈⟨ f≤g ⟩
      g ∎

  ≤-trans : {A B : Obj} {f g h : A ⇒ B} → f ≤ g → g ≤ h → f ≤ h
  ≤-trans {A} {B} {f} {g} {h} f≤g g≤h = begin
      f + h       ≈⟨ refl⟩∘⟨ ×₁-congˡ g≤h ⟩∘⟨refl ⟨
      f + (g + h) ≈⟨ +-assoc f g h ⟨
      (f + g) + h ≈⟨ refl⟩∘⟨ ×₁-congʳ f≤g ⟩∘⟨refl ⟩
      g + h       ≈⟨ g≤h ⟩
      h           ∎

  ≤-resp-+
      : {A B : Obj}
        {f g h i : A ⇒ B}
      → f ≤ h
      → g ≤ i
      → (f + g) ≤ (h + i)
  ≤-resp-+ {f = f} {g} {h} {i} f≤h g≤i = begin
      (f + g) + (h + i) ≈⟨ +-assoc f g (h + i) ⟩
      f + (g + (h + i)) ≈⟨ +-congˡ (+-assoc g h i) ⟨
      f + ((g + h) + i) ≈⟨ +-congˡ (+-congʳ (+-comm g h)) ⟩
      f + ((h + g) + i) ≈⟨ +-congˡ (+-assoc h g i) ⟩
      f + (h + (g + i)) ≈⟨ +-assoc f h (g + i) ⟨
      (f + h) + (g + i) ≈⟨ +-cong f≤h g≤i ⟩
      h + i             ∎

  Δ-⊕ : {X Y : Obj} → Δ {X ⊕ Y} ≈ σ₂₃ ∘ Δ ×₁ Δ
  Δ-⊕ {X} {Y} = begin
      ⟨ id , id ⟩                                     ≈⟨ ⟨⟩-cong₂ id×₁id id×₁id ⟨
      ⟨ id ×₁ id , id ×₁ id ⟩                         ≈⟨ ⟨⟩-cong₂ (×₁-cong₂ project₁ project₁) (×₁-cong₂ project₂ project₂) ⟨
      ⟨ (π₁ ∘ Δ) ×₁ (π₁ ∘ Δ) , (π₂ ∘ Δ) ×₁ (π₂ ∘ Δ) ⟩ ≈⟨ ⟨⟩-cong₂ ×₁∘×₁ ×₁∘×₁ ⟨
      ⟨ π₁ ×₁ π₁ ∘ Δ ×₁ Δ , π₂ ×₁ π₂ ∘ Δ ×₁ Δ ⟩       ≈⟨ ⟨⟩∘ ⟨
      σ₂₃ ∘ Δ ×₁ Δ                                    ∎

  ∇-⊕ : {X Y : Obj} → ∇ {X ⊕ Y} ≈ ∇ ×₁ ∇ ∘ σ₂₃
  ∇-⊕ {X} {Y} = begin
      [ id , id ]                                       ≈⟨ []-cong₂ id×₁id id×₁id ⟨
      [ id ×₁ id , id ×₁ id ]                           ≈⟨ []-cong₂ (×₁-cong₂ inject₁ inject₁) (×₁-cong₂ inject₂ inject₂) ⟨
      [ (∇ ∘ i₁) ×₁ (∇ ∘ i₁) , (∇ ∘ i₂) ×₁ (∇ ∘ i₂) ]   ≈⟨ []-cong₂ ×₁∘×₁ ×₁∘×₁ ⟨
      [ ∇ ×₁ ∇ ∘ i₁ ×₁ i₁ , ∇ ×₁ ∇ ∘ i₂ ×₁ i₂ ]         ≈⟨ ∘[] ⟨
      ∇ ×₁ ∇ ∘ [ i₁ ×₁ i₁ , i₂ ×₁ i₂ ]                  ≈⟨ refl⟩∘⟨ ⟨⟩-unique (∘[] ○ []-cong₂ π₁∘×₁ π₁∘×₁) (∘[] ○ []-cong₂ π₂∘×₁ π₂∘×₁) ⟨
      ∇ ×₁ ∇ ∘ ⟨ π₁ +₁ π₁ , π₂ +₁ π₂ ⟩                  ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (×₁-+₁ π₁ π₁) (×₁-+₁ π₂ π₂) ⟨
      ∇ ×₁ ∇ ∘ σ₂₃                                      ∎

  ≤-resp-×₁
      : {A B C D : Obj}
        {f h : A ⇒ B}
        {g i : C ⇒ D}
      → f ≤ h
      → g ≤ i
      → (f ×₁ g) ≤ (h ×₁ i)
  ≤-resp-×₁ {f = f} {h} {g} {i} f≤h g≤i = begin
      ∇ ∘ (f ×₁ g) ×₁ (h ×₁ i) ∘ Δ                        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ Δ-⊕ ⟩
      ∇ ∘ (f ×₁ g) ×₁ (h ×₁ i) ∘ σ₂₃ ∘ Δ ×₁ Δ             ≈⟨ refl⟩∘⟨ extendʳ σ₂₃-×₁ ⟩
      ∇ ∘ σ₂₃ ∘ (f ×₁ h) ×₁ (g ×₁ i) ∘ Δ ×₁ Δ             ≈⟨ pushˡ ∇-⊕ ⟩
      ∇ ×₁ ∇ ∘ σ₂₃ ∘ σ₂₃ ∘ (f ×₁ h) ×₁ (g ×₁ i) ∘ Δ ×₁ Δ  ≈⟨ refl⟩∘⟨ cancelˡ σ₂₃-σ₂₃ ⟩
      ∇ ×₁ ∇ ∘ (f ×₁ h) ×₁ (g ×₁ i) ∘ Δ ×₁ Δ              ≈⟨ refl⟩∘⟨ ×₁∘×₁ ⟩
      ∇ ×₁ ∇ ∘ (f ×₁ h ∘ Δ) ×₁ (g ×₁ i ∘ Δ)               ≈⟨ ×₁∘×₁ ⟩
      (∇ ∘ f ×₁ h ∘ Δ) ×₁ (∇ ∘ g ×₁ i ∘ Δ)                ≈⟨ ×₁-cong₂ f≤h g≤i ⟩
      h ×₁ i                                              ∎

  ≤-resp-∘
      : {A B C : Obj}
        {f h : B ⇒ C}
        {g i : A ⇒ B}
      → f ≤ h
      → g ≤ i
      → (f ∘ g) ≤ (h ∘ i)
  ≤-resp-∘ {f = f} {h} {g} {i} f≤h g≤i = begin
      f ∘ g + (h ∘ i)         ≈⟨ +-congˡ (f≤h ⟩∘⟨refl) ⟨
      f ∘ g + ((f + h) ∘ i)   ≈⟨ +-congˡ ∘-distribʳ ⟩
      f ∘ g + (f ∘ i + h ∘ i) ≈⟨ +-assoc (f ∘ g) (f ∘ i) (h ∘ i) ⟨
      (f ∘ g + f ∘ i) + h ∘ i ≈⟨ +-congʳ ∘-distribˡ ⟨
      f ∘ (g + i) + h ∘ i     ≈⟨ +-congʳ (refl⟩∘⟨ g≤i) ⟩
      f ∘ i + h ∘ i           ≈⟨ ∘-distribʳ ⟨
      (f + h) ∘ i             ≈⟨ f≤h ⟩∘⟨refl ⟩
      h ∘ i                   ∎

  †-resp-≤ : {A B : Obj} {f g : A ⇒ B} → f ≤ g → (f †) ≤ (g †)
  †-resp-≤ {A} {B} {f} {g} f≤g = begin
      (f †) + (g †) ≈⟨ +-† ⟨
      (f + g) †     ≈⟨ ⟨ f≤g ⟩† ⟩
      g †           ∎

  -- special law
  ∇∘Δ : {A : Obj} → ∇ ∘ Δ ≈ id {A}
  ∇∘Δ = begin
      ∇ ∘ Δ             ≈⟨ refl⟩∘⟨ introˡ id×₁id ⟩
      ∇ ∘ id ×₁ id ∘ Δ  ≈⟨ idempotent ⟩
      id                ∎

  dagger-2-poset : Dagger-2-Poset
  dagger-2-poset = record
      { 2-poset = record
          { Obj = Obj
          ; hom = λ A B → record
              { Carrier = A ⇒ B
              ; _≈_ = _≈_
              ; _≤_ = _≤_
              ; isPartialOrder = record
                  { isPreorder = record
                      { isEquivalence = equiv
                      ; reflexive = λ x≈y → Equiv.trans (+-congʳ x≈y) ≤-refl
                      ; trans = ≤-trans
                      }
                  ; antisym = ≤-antisym
                  }
              }
          ; id = mkPosetHomo _ _ (λ _ → id) (λ _ → ≤-refl)
          ; ⊚ = mkPosetHomo _ _ (λ (f , g) → f ∘ g) (λ (≤₁ , ≤₂) → ≤-resp-∘ ≤₁ ≤₂)
          ; ⊚-assoc = assoc
          ; unitˡ = identityˡ
          ; unitʳ = identityʳ
          }
      ; hasDagger = record
          { _† = _†
          ; †-identity = †-identity
          ; †-homomorphism = †-homomorphism
          ; †-resp-≈ = ⟨_⟩†
          ; †-involutive = †-involutive
          }
      ; †-resp-≤ = †-resp-≤
      }

  maps : Category o (ℓ ⊔ e) e
  maps = Maps dagger-2-poset

  open Dagger-2-Poset dagger-2-poset using (category)
  open SemiadditiveMonoidal semiadditive using (monoidal)

  module M = Monoidal monoidal

  ×₁-functional
      : {A B C D : Obj}
        {f : A ⇒ B}
        {g : C ⇒ D}
      → (f ∘ f †) ≤ id
      → (g ∘ g †) ≤ id
      → (f ×₁ g ∘ (f ×₁ g) †) ≤ id
  ×₁-functional {f = f} {g} f∘f†≤id g∘g†≤id = begin
      f ×₁ g ∘ (f ×₁ g) † + id          ≈⟨ +-congʳ (refl⟩∘⟨ †-resp-×₁) ⟩
      f ×₁ g ∘ (f †) ×₁ (g †) + id      ≈⟨ +-cong ×₁∘×₁ (Equiv.sym id×₁id) ⟩
      (f ∘ f †) ×₁ (g ∘ g †) + id ×₁ id ≈⟨ ≤-resp-×₁ f∘f†≤id g∘g†≤id ⟩
      id ×₁ id                          ≈⟨ id×₁id ⟩
      id                                ∎

  ×₁-entire
      : {A B C D : Obj}
        {f : A ⇒ B}
        {g : C ⇒ D}
      → id ≤ (f † ∘ f)
      → id ≤ (g † ∘ g)
      → id ≤ ((f ×₁ g) † ∘ f ×₁ g)
  ×₁-entire {f = f} {g} id≤f†∘f id≤g†∘g = begin
      id + (f ×₁ g) † ∘ (f ×₁ g)        ≈⟨ +-congˡ (†-resp-×₁ ⟩∘⟨refl) ⟩
      id + (f †) ×₁ (g †) ∘ f ×₁ g      ≈⟨ +-cong (Equiv.sym id×₁id) ×₁∘×₁ ⟩
      id ×₁ id + (f † ∘ f) ×₁ (g † ∘ g) ≈⟨ ≤-resp-×₁ id≤f†∘f id≤g†∘g ⟩
      (f † ∘ f) ×₁ (g † ∘ g)            ≈⟨ ×₁∘×₁ ⟨
      (f †) ×₁ (g †) ∘ f ×₁ g           ≈⟨ †-resp-×₁ ⟩∘⟨refl ⟨
      (f ×₁ g) † ∘ f ×₁ g               ∎

  open Map

  ⊗ : Bifunctor maps maps maps
  ⊗ = record
      { F₀ = M.⊗.₀
      ; F₁ = λ (f , g) → record
          { map = map f M.⊗₁ map g
          ; isMap = record
              { functional = ×₁-functional (functional f) (functional g)
              ; entire = ×₁-entire (entire f) (entire g)
              }
          }
      ; identity = M.⊗.identity
      ; homomorphism = M.⊗.homomorphism
      ; F-resp-≈ = M.⊗.F-resp-≈
      }

  open Morphism maps using (_≅_)
  open Equiv

  λ⇒-unitary : {X : Obj} → Iso category (π₂ {𝟘} {X}) (π₂ †)
  λ⇒-unitary = record { Iso (Iso-resp-≈ M.unitorˡ.iso refl (sym π₂†)) }

  λ⇐-unitary : {X : Obj} → Iso category (i₂ {𝟘} {X}) (i₂ †)
  λ⇐-unitary = record { Iso (Iso-swap (Iso-resp-≈ M.unitorˡ.iso (sym i₂†) refl)) }

  ρ⇒-unitary : {X : Obj} → Iso category (π₁ {X} {𝟘}) (π₁ †)
  ρ⇒-unitary = record { Iso (Iso-resp-≈ M.unitorʳ.iso refl (sym π₁†)) }

  ρ⇐-unitary : {X : Obj} → Iso category (i₁ {X} {𝟘}) (i₁ †)
  ρ⇐-unitary = record { Iso (Iso-swap (Iso-resp-≈ M.unitorʳ.iso (sym i₁†) refl)) }

  α⇒-unitary : {X Y Z : Obj} → Iso category (assocˡ {X} {Y} {Z}) (assocˡ †)
  α⇒-unitary = record { Iso (Iso-resp-≈ M.associator.iso refl (sym α⇒†)) }

  α⇐-unitary : {X Y Z : Obj} → Iso category (assocʳ {X} {Y} {Z}) (assocʳ †)
  α⇐-unitary = record { Iso (Iso-swap (Iso-resp-≈ M.associator.iso (sym α⇐†) refl)) }

  unitorˡ : {X : Obj} → 𝟘 M.⊗₀ X ≅ X
  unitorˡ = record
      { from = record
          { map = M.unitorˡ.from
          ; isMap = unitary-isMap dagger-2-poset λ⇒-unitary
          }
      ; to = record
          { map = M.unitorˡ.to
          ; isMap = unitary-isMap dagger-2-poset λ⇐-unitary
          }
      ; iso = record { M.unitorˡ }
      }

  unitorʳ : {X : Obj} → X M.⊗₀ 𝟘 ≅ X
  unitorʳ = record
      { from = record
          { map = M.unitorʳ.from
          ; isMap = unitary-isMap dagger-2-poset ρ⇒-unitary
          }
      ; to = record
          { map = M.unitorʳ.to
          ; isMap = unitary-isMap dagger-2-poset ρ⇐-unitary
          }
      ; iso = record { M.unitorʳ }
      }

  associator : {X Y Z : Obj} → (X M.⊗₀ Y) M.⊗₀ Z ≅ X M.⊗₀ (Y M.⊗₀ Z)
  associator = record
      { from = record
          { map = M.associator.from
          ; isMap = unitary-isMap dagger-2-poset α⇒-unitary
          }
      ; to = record
          { map = M.associator.to
          ; isMap = unitary-isMap dagger-2-poset α⇐-unitary
          }
      ; iso = record { M.associator }
      }

  maps-monoidal : Monoidal maps
  maps-monoidal = record
      { ⊗ = ⊗
      ; unit = 𝟘
      ; unitorˡ = unitorˡ
      ; unitorʳ = unitorʳ
      ; associator = associator
      ; M
      }