diff options
Diffstat (limited to 'Category')
| -rw-r--r-- | Category/BinaryBiproducts.agda | 44 | ||||
| -rw-r--r-- | Category/Dagger/2-Poset.agda | 49 | ||||
| -rw-r--r-- | Category/Dagger/Semiadditive.agda | 253 | ||||
| -rw-r--r-- | Category/Semiadditive.agda | 4 | ||||
| -rw-r--r-- | Category/Semiadditive/Monoidal.agda | 166 |
5 files changed, 474 insertions, 42 deletions
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 + } |