From 514bb6e3e235f37c4e49bd703ad02a5ab31e8c0a Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Mon, 3 Aug 2026 19:08:47 -0500 Subject: Show category of maps is monoidal --- Category/BinaryBiproducts.agda | 44 ++++++ Category/Dagger/2-Poset.agda | 49 ++---- Category/Dagger/Semiadditive.agda | 253 +++++++++++++++++++++++++++++++ Category/Semiadditive.agda | 4 +- Category/Semiadditive/Monoidal.agda | 166 ++++++++++++++++++++ Data/WiringDiagram/Monoidal.agda | 38 ++--- Data/WiringDiagram/Monoidal/Braided.agda | 19 +-- Data/WiringDiagram/Monoidal/Core.agda | 24 +-- 8 files changed, 496 insertions(+), 101 deletions(-) create mode 100644 Category/Semiadditive/Monoidal.agda diff --git a/Category/BinaryBiproducts.agda b/Category/BinaryBiproducts.agda index 81a23cf..3ded5a7 100644 --- a/Category/BinaryBiproducts.agda +++ b/Category/BinaryBiproducts.agda @@ -285,3 +285,47 @@ record BinaryBiproducts : Set (levelOfTerm 𝒞) where ×₁∘second : {A B C D E : Obj} {f : A ⇒ B} {g : D ⇒ E} {h : C ⇒ D} → (f ×₁ g) ∘ second h ≈ f ×₁ (g ∘ h) ×₁∘second = ×₁∘×₁ ○ ×₁-cong₂ identityʳ Equiv.refl + + -- Swap middle two of four + + σ₂₃ : {A B C D : Obj} → (A ⊕ B) ⊕ (C ⊕ D) ⇒ (A ⊕ C) ⊕ (B ⊕ D) + σ₂₃ = ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ + + σ₂₃-σ₂₃ + : {A B C D : Obj} + → σ₂₃ {A} {B} {C} {D} ∘ σ₂₃ ≈ id + σ₂₃-σ₂₃ = begin + ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ ∘ σ₂₃ ≈⟨ ⟨⟩∘ ⟩ + ⟨ π₁ ×₁ π₁ ∘ σ₂₃ , π₂ ×₁ π₂ ∘ σ₂₃ ⟩ ≈⟨ ⟨⟩-cong₂ ×₁∘⟨⟩ ×₁∘⟨⟩ ⟩ + ⟨ ⟨ π₁ ∘ π₁ ×₁ π₁ , π₁ ∘ π₂ ×₁ π₂ ⟩ , ⟨ π₂ ∘ _ , π₂ ∘ _ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ (⟨⟩-cong₂ π₁∘×₁ π₁∘×₁) (⟨⟩-cong₂ π₂∘×₁ π₂∘×₁) ⟩ + ⟨ ⟨ π₁ ∘ π₁ , π₂ ∘ π₁ ⟩ , ⟨ π₁ ∘ π₂ , π₂ ∘ π₂ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ g-η g-η ⟩ + ⟨ π₁ , π₂ ⟩ ≈⟨ η ⟩ + id ∎ + + σ₂₃-×₁ + : {A A′ B B′ C C′ D D′ : Obj} + {f : A ⇒ A′} + {g : B ⇒ B′} + {h : C ⇒ C′} + {i : D ⇒ D′} + → (f ×₁ g) ×₁ (h ×₁ i) ∘ σ₂₃ ≈ σ₂₃ ∘ (f ×₁ h) ×₁ (g ×₁ i) + σ₂₃-×₁ {f = f} {g} {h} {i} = begin + (f ×₁ g) ×₁ (h ×₁ i) ∘ ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ ≈⟨ ×₁∘⟨⟩ ⟩ + ⟨ f ×₁ g ∘ π₁ ×₁ π₁ , h ×₁ i ∘ π₂ ×₁ π₂ ⟩ ≈⟨ ⟨⟩-cong₂ ×₁∘×₁ ×₁∘×₁ ⟩ + ⟨ (f ∘ π₁) ×₁ (g ∘ π₁) , (h ∘ π₂) ×₁ (i ∘ π₂) ⟩ ≈⟨ ⟨⟩-cong₂ (×₁-cong₂ π₁∘×₁ π₁∘×₁) (×₁-cong₂ π₂∘×₁ π₂∘×₁) ⟨ + ⟨ (π₁ ∘ f ×₁ h) ×₁ (π₁ ∘ g ×₁ i) , (π₂ ∘ f ×₁ h) ×₁ (π₂ ∘ g ×₁ i) ⟩ ≈⟨ ⟨⟩-cong₂ ×₁∘×₁ ×₁∘×₁ ⟨ + ⟨ π₁ ×₁ π₁ ∘ (f ×₁ h) ×₁ (g ×₁ i) , π₂ ×₁ π₂ ∘ (f ×₁ h) ×₁ (g ×₁ i) ⟩ ≈⟨ ⟨⟩∘ ⟨ + σ₂₃ ∘ (f ×₁ h) ×₁ (g ×₁ i) ∎ + + σ₂₃-⟨⟩ + : {X A B C D : Obj} + {f : X ⇒ A} + {g : X ⇒ B} + {h : X ⇒ C} + {i : X ⇒ D} + → σ₂₃ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ ≈ ⟨ ⟨ f , h ⟩ , ⟨ g , i ⟩ ⟩ + σ₂₃-⟨⟩ {f = f} {g} {h} {i} = begin + σ₂₃ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ ≈⟨ ⟨⟩∘ ⟩ + ⟨ π₁ ×₁ π₁ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ , π₂ ×₁ π₂ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ ×₁∘⟨⟩ ×₁∘⟨⟩ ⟩ + ⟨ ⟨ π₁ ∘ ⟨ f , g ⟩ , π₁ ∘ ⟨ h , i ⟩ ⟩ , ⟨ π₂ ∘ ⟨ f , g ⟩ , π₂ ∘ ⟨ h , i ⟩ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ (⟨⟩-cong₂ project₁ project₁) (⟨⟩-cong₂ project₂ project₂) ⟩ + ⟨ ⟨ f , h ⟩ , ⟨ g , i ⟩ ⟩ ∎ diff --git a/Category/Dagger/2-Poset.agda b/Category/Dagger/2-Poset.agda index 27c01af..fcd7e4a 100644 --- a/Category/Dagger/2-Poset.agda +++ b/Category/Dagger/2-Poset.agda @@ -1,7 +1,6 @@ {-# OPTIONS --without-K --safe #-} open import Categories.Category using (Category) -open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger) open import Level using (Level; suc; _⊔_) module Category.Dagger.2-Poset {o ℓ e : Level} where @@ -17,7 +16,7 @@ open import Categories.Enriched.Category Posets-Monoidal using () renaming (Cate open import Data.Product using (_,_) open import Data.Unit.Polymorphic using (tt) open import Relation.Binary using (Poset) -open import Relation.Binary.Morphism.Bundles using (PosetHomomorphism; mkPosetHomo) +open import Relation.Binary.Morphism.Bundles using (PosetHomomorphism) open PosetHomomorphism using (⟦_⟧; cong; mono) @@ -51,49 +50,13 @@ record Dagger-2-Poset : Set (suc (o ⊔ ℓ ⊔ e)) where private module P {A B : Obj} = Poset (hom A B) - open P using (_≤_) public + open P using (_≤_; reflexive) public open Category category hiding (Obj) public open HasDagger hasDagger public field †-resp-≤ : {A B : Obj} {f g : A ⇒ B} → f ≤ g → f † ≤ g † -dagger-2-poset : {𝒞 : Category o ℓ e} (ISA† : IdempotentSemiadditiveDagger 𝒞) → Dagger-2-Poset -dagger-2-poset {𝒞} ISA† = record - { 2-poset = record - { Obj = Obj - ; hom = λ A B → record - { Carrier = A ⇒ B - ; _≈_ = _≈_ - ; _≤_ = ISA†._≤_ - ; isPartialOrder = record - { isPreorder = record - { isEquivalence = equiv - ; reflexive = λ x≈y → Equiv.trans (ISA†.+-congʳ x≈y) ISA†.≤-refl - ; trans = ISA†.≤-trans - } - ; antisym = ISA†.≤-antisym - } - } - ; id = mkPosetHomo _ _ (λ _ → id) (λ _ → ISA†.≤-refl) - ; ⊚ = mkPosetHomo _ _ (λ (f , g) → f ∘ g) (λ (≤₁ , ≤₂) → ISA†.≤-resp-∘ ≤₁ ≤₂) - ; ⊚-assoc = assoc - ; unitˡ = identityˡ - ; unitʳ = identityʳ - } - ; hasDagger = record - { _† = ISA†._† - ; †-identity = ISA†.†-identity - ; †-homomorphism = ISA†.†-homomorphism - ; †-resp-≈ = ISA†.⟨_⟩† - ; †-involutive = ISA†.†-involutive - } - ; †-resp-≤ = ISA†.†-resp-≤ - } - where - module ISA† = IdempotentSemiadditiveDagger ISA† - open Category 𝒞 - module _ (S : Dagger-2-Poset) where open Dagger-2-Poset S @@ -104,6 +67,14 @@ module _ (S : Dagger-2-Poset) where functional : f ∘ f † ≤ id entire : id ≤ f † ∘ f + open import Categories.Morphism category using (Iso) + + unitary-isMap : {A B : Obj} {f : A ⇒ B} → Iso f (f †) → IsMap f + unitary-isMap iso = let open Iso iso in record + { functional = reflexive isoʳ + ; entire = reflexive (Equiv.sym isoˡ) + } + record Map (A B : Obj) : Set (ℓ ⊔ e) where field diff --git a/Category/Dagger/Semiadditive.agda b/Category/Dagger/Semiadditive.agda index a5b03ab..424f8df 100644 --- a/Category/Dagger/Semiadditive.agda +++ b/Category/Dagger/Semiadditive.agda @@ -5,11 +5,21 @@ 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 @@ -41,6 +51,42 @@ record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where Δ † † ≈⟨ †-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 ∘ π₂ ⟩ † ≈⟨ ⟨⟩-† ⟩ @@ -77,6 +123,21 @@ record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where 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 @@ -127,6 +188,41 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where (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} @@ -156,3 +252,160 @@ record IdempotentSemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where ∇ ∘ Δ ≈⟨ 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 + } diff --git a/Category/Semiadditive.agda b/Category/Semiadditive.agda index 05ce264..86b5585 100644 --- a/Category/Semiadditive.agda +++ b/Category/Semiadditive.agda @@ -13,6 +13,7 @@ open import Categories.Category.CMonoidEnriched using (CM-Category) open import Categories.Category.Cartesian 𝒞 using (Cartesian) open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal) open import Categories.Category.Cocartesian 𝒞 using (Cocartesian) +open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) open import Categories.Object.Zero 𝒞 using (Zero) open import Category.BinaryBiproducts 𝒞 using (BinaryBiproducts) open import Data.Product using (_,_) @@ -176,6 +177,3 @@ record Semiadditive : Set (levelOfTerm 𝒞) where { initial = initial ; coproducts = binaryCoproducts } - - open CartesianMonoidal cartesian using (monoidal) public - open CartesianSymmetricMonoidal cartesian using (symmetric) public 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 + } diff --git a/Data/WiringDiagram/Monoidal.agda b/Data/WiringDiagram/Monoidal.agda index 3d7ea78..96ff101 100644 --- a/Data/WiringDiagram/Monoidal.agda +++ b/Data/WiringDiagram/Monoidal.agda @@ -28,7 +28,7 @@ open import Data.WiringDiagram.Balanced S using (BWD; Push; Pull) open import Data.WiringDiagram.Core S using (_□_; _⧈_; id-⧈; _≈-⧈_; _⌸_; _⌻_) open import Data.WiringDiagram.Directed S using (DWD; Pulsh) open import Data.WiringDiagram.Monoidal.Braided S using (swap-⧈; DWD-Braided) public -open import Data.WiringDiagram.Monoidal.Core S using (DWD-Monoidal; BWD-Monoidal; _⊞_; _⊞₁_; σ₂₃; associator⇒; unitorˡ⇒; unitorʳ⇒; ⊞-identity) public +open import Data.WiringDiagram.Monoidal.Core S using (DWD-Monoidal; BWD-Monoidal; _⊞_; _⊞₁_; associator⇒; unitorˡ⇒; unitorʳ⇒; ⊞-identity) public open import Data.WiringDiagram.Monoidal.Symmetric S using (DWD-Symmetric; BWD-Symmetric) public module DWD = Category DWD @@ -141,23 +141,19 @@ module Directed where unitaryˡ : {A B : Obj} - → Pulsh.₁ (⟨ ! {A} , id {A} ⟩ , π₂ {𝟘} {B}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ + → Pulsh.₁ (i₂ {𝟘} {A} , π₂ {𝟘} {B}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ unitorˡ⇒ unitaryˡ = begin - Pulsh.₁ (⟨ ! , id ⟩ , π₂) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Pulsh.₁ (⟨ ! , id ⟩ , π₂) ≈⟨ Pulsh.F-resp-≈ (⟨⟩-congʳ (!-unique zero⇒) , refl) ⟩ - Pulsh.₁ (⟨ zero⇒ , id ⟩ , π₂) ≈⟨ Pulsh.F-resp-≈ (⟨⟩-unique π₁∘i₂≈0 π₂∘i₂≈id , refl) ⟩ - unitorˡ⇒ ∎ + Pulsh.₁ (i₂ , π₂) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ + unitorˡ⇒ ∎ unitaryʳ : {A B : Obj} - → Pulsh.₁ (⟨ id {A} , ! {A} ⟩ , π₁ {B} {𝟘}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ + → Pulsh.₁ (i₁ {A} {𝟘} , π₁ {B} {𝟘}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ unitorʳ⇒ unitaryʳ = begin - Pulsh.₁ (⟨ id , ! ⟩ , π₁) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Pulsh.₁ (⟨ id , ! ⟩ , π₁) ≈⟨ Pulsh.F-resp-≈ (⟨⟩-congˡ (!-unique zero⇒) , refl) ⟩ - Pulsh.₁ (⟨ id , zero⇒ ⟩ , π₁) ≈⟨ Pulsh.F-resp-≈ (⟨⟩-unique π₁∘i₁≈id π₂∘i₁≈0 , refl) ⟩ - unitorʳ⇒ ∎ + Pulsh.₁ (i₁ , π₁) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ + unitorʳ⇒ ∎ braiding-compat : {A B C D : Obj} @@ -302,25 +298,21 @@ module BalancedPull where unitaryˡ : {A : Obj} - → Pull.₁ ⟨ ! {A} , id {A} ⟩ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ + → Pull.₁ (i₂ {𝟘} {A}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ unitorˡ⇒ unitaryˡ = begin - Pull.₁ ⟨ ! , id ⟩ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Pull.₁ ⟨ ! , id ⟩ ≈⟨ Pull.F-resp-≈ (⟨⟩-congʳ (!-unique zero⇒)) ⟩ - Pull.₁ ⟨ zero⇒ , id ⟩ ≈⟨ Pull.F-resp-≈ (⟨⟩-unique π₁∘i₂≈0 π₂∘i₂≈id) ⟩ - Pull.₁ i₂ ≈⟨ refl ⌸ i₂† ⟩ - unitorˡ⇒ ∎ + Pull.₁ i₂ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ + Pull.₁ i₂ ≈⟨ refl ⌸ i₂† ⟩ + unitorˡ⇒ ∎ unitaryʳ : {A : Obj} - → Pull.₁ ⟨ id {A} , ! {A} ⟩ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ + → Pull.₁ (i₁ {A} {𝟘}) ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈-⧈ unitorʳ⇒ unitaryʳ = begin - Pull.₁ ⟨ id , ! ⟩ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ - Pull.₁ ⟨ id , ! ⟩ ≈⟨ Pull.F-resp-≈ (⟨⟩-congˡ (!-unique zero⇒)) ⟩ - Pull.₁ ⟨ id , zero⇒ ⟩ ≈⟨ Pull.F-resp-≈ (⟨⟩-unique π₁∘i₁≈id π₂∘i₁≈0) ⟩ - Pull.₁ i₁ ≈⟨ refl ⌸ i₁† ⟩ - unitorʳ⇒ ∎ + Pull.₁ i₁ ⌻ id-⧈ ⌻ id-⧈ ⊞₁ id-⧈ ≈⟨ elimʳ (elimʳ ⊞-identity) ⟩ + Pull.₁ i₁ ≈⟨ refl ⌸ i₁† ⟩ + unitorʳ⇒ ∎ braiding-compat : {A B : Obj} diff --git a/Data/WiringDiagram/Monoidal/Braided.agda b/Data/WiringDiagram/Monoidal/Braided.agda index 7b28d85..d45d8d2 100644 --- a/Data/WiringDiagram/Monoidal/Braided.agda +++ b/Data/WiringDiagram/Monoidal/Braided.agda @@ -11,6 +11,7 @@ module Data.WiringDiagram.Monoidal.Braided where import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning +import Category.Semiadditive.Monoidal as SemiadditiveMonoidal import Data.WiringDiagram.Core as WD open import Categories.Category.Monoidal using (Monoidal) @@ -21,12 +22,15 @@ open import Categories.Functor.Bifunctor using (flip-bifunctor) open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper) open import Data.Product using (uncurry; _,_) open import Data.WiringDiagram.Monoidal.Core S - using (_⊞_; _⊞₁_; σ₂₃; associator⇒; associator⇐; DWD-Monoidal; BWD-Monoidal) + using (_⊞_; _⊞₁_; associator⇒; associator⇐; DWD-Monoidal; BWD-Monoidal) renaming (module Directed to D; module Balanced to B) open import Function using (flip) open Category 𝒞 open SemiadditiveDagger S + +open SemiadditiveMonoidal semiadditive using (symmetric) + open Symmetric symmetric using (braided; hexagon₁; hexagon₂) open WD S using (Box; WiringDiagram; _□_; _⧈_; _≈-⧈_; _⌸_; id-⧈; _⌻_; ≈-sym) @@ -34,19 +38,6 @@ open HomReasoning open ⇒-Reasoning open Equiv -σ₂₃-⟨⟩ - : {X A B C D : Obj} - {f : X ⇒ A} - {g : X ⇒ B} - {h : X ⇒ C} - {i : X ⇒ D} - → σ₂₃ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ ≈ ⟨ ⟨ f , h ⟩ , ⟨ g , i ⟩ ⟩ -σ₂₃-⟨⟩ {f = f} {g} {h} {i} = begin - σ₂₃ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ ≈⟨ ⟨⟩∘ ⟩ - ⟨ π₁ ×₁ π₁ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ , π₂ ×₁ π₂ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ ×₁∘⟨⟩ ×₁∘⟨⟩ ⟩ - ⟨ ⟨ π₁ ∘ ⟨ f , g ⟩ , π₁ ∘ ⟨ h , i ⟩ ⟩ , ⟨ π₂ ∘ ⟨ f , g ⟩ , π₂ ∘ ⟨ h , i ⟩ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ (⟨⟩-cong₂ project₁ project₁) (⟨⟩-cong₂ project₂ project₂) ⟩ - ⟨ ⟨ f , h ⟩ , ⟨ g , i ⟩ ⟩ ∎ - swap-⧈ : (X Y : Box) → WiringDiagram (X ⊞ Y) (Y ⊞ X) swap-⧈ X Y = swap ∘ π₂ ⧈ swap diff --git a/Data/WiringDiagram/Monoidal/Core.agda b/Data/WiringDiagram/Monoidal/Core.agda index 5abd60f..daed109 100644 --- a/Data/WiringDiagram/Monoidal/Core.agda +++ b/Data/WiringDiagram/Monoidal/Core.agda @@ -13,33 +13,28 @@ module Data.WiringDiagram.Monoidal.Core import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning import Categories.Morphism as Morphism import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning +import Category.Semiadditive.Monoidal as SemiadditiveMonoidal import Data.WiringDiagram.Balanced as BalancedWD import Data.WiringDiagram.Core as WD import Data.WiringDiagram.Directed as DirectedWD open import Categories.Category.Monoidal using (Monoidal) -open import Categories.Category.Monoidal.Symmetric using (module Symmetric) open import Categories.Category.Monoidal.Utilities using (pentagon-inv) open import Categories.Functor.Bifunctor using (Bifunctor) open import Categories.Object.Initial using (Initial; IsInitial) open import Data.Product using (_,_; uncurry′) open SemiadditiveDagger S +open SemiadditiveMonoidal semiadditive using (monoidal) open BalancedWD S using (BWD) open Category 𝒞 open DirectedWD S using (DWD) open Monoidal monoidal using (triangle; pentagon) -open Symmetric symmetric using (braided) open WD S using (Box; WiringDiagram; _□_; _⧈_; _≈-⧈_; _⌸_; id-⧈; _⌻_; ≈-sym) module DWD = Category DWD --- Swap middle two of four - -σ₂₃ : {A B C D : Obj} → (A ⊕ B) ⊕ (C ⊕ D) ⇒ (A ⊕ C) ⊕ (B ⊕ D) -σ₂₃ = ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ - -- Monoidal unit and initial object 𝟘-□ : Box @@ -123,21 +118,6 @@ open Equiv ⟨ ⟨ π₁ , id ⟩ ∘ π₁ ×₁ π₁ , ⟨ π₁ , id ⟩ ∘ π₂ ×₁ π₂ ⟩ ≈⟨ ×₁∘⟨⟩ ⟨ ⟨ π₁ , id ⟩ ×₁ ⟨ π₁ , id ⟩ ∘ ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ ∎ -σ₂₃-×₁ - : {A A′ B B′ C C′ D D′ : Obj} - {f : A ⇒ A′} - {g : B ⇒ B′} - {h : C ⇒ C′} - {i : D ⇒ D′} - → (f ×₁ g) ×₁ (h ×₁ i) ∘ σ₂₃ ≈ σ₂₃ ∘ (f ×₁ h) ×₁ (g ×₁ i) -σ₂₃-×₁ {f = f} {g} {h} {i} = begin - (f ×₁ g) ×₁ (h ×₁ i) ∘ ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩ ≈⟨ ×₁∘⟨⟩ ⟩ - ⟨ f ×₁ g ∘ π₁ ×₁ π₁ , h ×₁ i ∘ π₂ ×₁ π₂ ⟩ ≈⟨ ⟨⟩-cong₂ ×₁∘×₁ ×₁∘×₁ ⟩ - ⟨ (f ∘ π₁) ×₁ (g ∘ π₁) , (h ∘ π₂) ×₁ (i ∘ π₂) ⟩ ≈⟨ ⟨⟩-cong₂ (×₁-cong₂ π₁∘×₁ π₁∘×₁) (×₁-cong₂ π₂∘×₁ π₂∘×₁) ⟨ - ⟨ (π₁ ∘ f ×₁ h) ×₁ (π₁ ∘ g ×₁ i) , (π₂ ∘ f ×₁ h) ×₁ (π₂ ∘ g ×₁ i) ⟩ ≈⟨ ⟨⟩-cong₂ ×₁∘×₁ ×₁∘×₁ ⟨ - ⟨ π₁ ×₁ π₁ ∘ (f ×₁ h) ×₁ (g ×₁ i) , π₂ ×₁ π₂ ∘ (f ×₁ h) ×₁ (g ×₁ i) ⟩ ≈⟨ ⟨⟩∘ ⟨ - σ₂₃ ∘ (f ×₁ h) ×₁ (g ×₁ i) ∎ - ⊞-homo : {A B C D E F : Box} {f : WiringDiagram A C} -- cgit v1.2.3