diff options
Diffstat (limited to 'Category/Instance')
| -rw-r--r-- | Category/Instance/FinitelyCocompletes.agda | 1 | ||||
| -rw-r--r-- | Category/Instance/Properties/FinitelyCocompletes.agda | 210 | ||||
| -rw-r--r-- | Category/Instance/Properties/SymMonCat.agda | 166 | ||||
| -rw-r--r-- | Category/Instance/SymMonCat.agda | 74 |
4 files changed, 241 insertions, 210 deletions
diff --git a/Category/Instance/FinitelyCocompletes.agda b/Category/Instance/FinitelyCocompletes.agda index 0847165..2766df2 100644 --- a/Category/Instance/FinitelyCocompletes.agda +++ b/Category/Instance/FinitelyCocompletes.agda @@ -62,6 +62,7 @@ _×_ 𝒞 𝒟 = record where module 𝒞 = FinitelyCocompleteCategory 𝒞 module 𝒟 = FinitelyCocompleteCategory 𝒟 +{-# INJECTIVE_FOR_INFERENCE _×_ #-} module _ (𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e) where diff --git a/Category/Instance/Properties/FinitelyCocompletes.agda b/Category/Instance/Properties/FinitelyCocompletes.agda deleted file mode 100644 index dedfa16..0000000 --- a/Category/Instance/Properties/FinitelyCocompletes.agda +++ /dev/null @@ -1,210 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -open import Level using (Level) -module Category.Instance.Properties.FinitelyCocompletes {o ℓ e : Level} where - -import Categories.Morphism.Reasoning as ⇒-Reasoning - -open import Categories.Category.BinaryProducts using (BinaryProducts) -open import Categories.Category.Cartesian.Bundle using (CartesianCategory) -open import Categories.Category.Product using (Product) renaming (_⁂_ to _⁂′_) -open import Categories.Diagram.Coequalizer using (IsCoequalizer) -open import Categories.Functor.Core using (Functor) -open import Categories.Functor using (_∘F_) renaming (id to idF) -open import Categories.Object.Coproduct using (IsCoproduct; IsCoproduct⇒Coproduct; Coproduct) -open import Categories.Object.Initial using (IsInitial) -open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) -open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes; FinitelyCocompletes-Cartesian; _×₁_) -open import Data.Product.Base using (_,_) renaming (_×_ to _×′_) -open import Functor.Exact using (IsRightExact; RightExactFunctor) -open import Level using (_⊔_; suc) - -FinitelyCocompletes-CC : CartesianCategory (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) -FinitelyCocompletes-CC = record - { U = FinitelyCocompletes - ; cartesian = FinitelyCocompletes-Cartesian - } - -module FinCoCom = CartesianCategory FinitelyCocompletes-CC -open BinaryProducts (FinCoCom.products) using (_×_; π₁; π₂; _⁂_; assocˡ) -- hiding (unique) - -module _ (𝒞 : FinitelyCocompleteCategory o ℓ e) where - - private - module 𝒞 = FinitelyCocompleteCategory 𝒞 - module 𝒞×𝒞 = FinitelyCocompleteCategory (𝒞 × 𝒞) - - open 𝒞 using ([_,_]; +-unique; i₁; i₂; _∘_; _+_; module Equiv; _⇒_; _+₁_; -+-) - open Equiv - - private - module -+- = Functor -+- - - +-resp-⊥ - : {(A , B) : 𝒞×𝒞.Obj} - → IsInitial 𝒞×𝒞.U (A , B) - → IsInitial 𝒞.U (A + B) - +-resp-⊥ {A , B} A,B-isInitial = record - { ! = [ A-isInitial.! , B-isInitial.! ] - ; !-unique = λ { f → +-unique (sym (A-isInitial.!-unique (f ∘ i₁))) (sym (B-isInitial.!-unique (f ∘ i₂))) } - } - where - open IsRightExact - open RightExactFunctor - module A-isInitial = IsInitial (F-resp-⊥ (isRightExact (π₁ {𝒞} {𝒞})) A,B-isInitial) - module B-isInitial = IsInitial (F-resp-⊥ (isRightExact (π₂ {𝒞} {𝒞})) A,B-isInitial) - - +-resp-+ - : {(A₁ , A₂) (B₁ , B₂) (C₁ , C₂) : 𝒞×𝒞.Obj} - {(i₁-₁ , i₁-₂) : (A₁ ⇒ C₁) ×′ (A₂ ⇒ C₂)} - {(i₂-₁ , i₂-₂) : (B₁ ⇒ C₁) ×′ (B₂ ⇒ C₂)} - → IsCoproduct 𝒞×𝒞.U (i₁-₁ , i₁-₂) (i₂-₁ , i₂-₂) - → IsCoproduct 𝒞.U (i₁-₁ +₁ i₁-₂) (i₂-₁ +₁ i₂-₂) - +-resp-+ {A₁ , A₂} {B₁ , B₂} {C₁ , C₂} {i₁-₁ , i₁-₂} {i₂-₁ , i₂-₂} isCoproduct = record - { [_,_] = λ { h₁ h₂ → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] } - ; inject₁ = inject₁ - ; inject₂ = inject₂ - ; unique = unique - } - where - open IsRightExact - open RightExactFunctor - module Coprod₁ = Coproduct (IsCoproduct⇒Coproduct 𝒞.U (F-resp-+ (isRightExact (π₁ {𝒞} {𝒞})) isCoproduct)) - module Coprod₂ = Coproduct (IsCoproduct⇒Coproduct 𝒞.U (F-resp-+ (isRightExact (π₂ {𝒞} {𝒞})) isCoproduct)) - open 𝒞 using ([]-cong₂; []∘+₁; +-g-η; +₁∘i₁; +₁∘i₂) - open 𝒞 using (Obj; _≈_; module HomReasoning; assoc) - open HomReasoning - open ⇒-Reasoning 𝒞.U - inject₁ - : {X : Obj} - {h₁ : A₁ + A₂ ⇒ X} - {h₂ : B₁ + B₂ ⇒ X} - → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₁-₁ +₁ i₁-₂) ≈ h₁ - inject₁ {_} {h₁} {h₂} = begin - [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₁-₁ +₁ i₁-₂) ≈⟨ []∘+₁ ⟩ - [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] ∘ i₁-₁ , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ∘ i₁-₂ ] ≈⟨ []-cong₂ Coprod₁.inject₁ Coprod₂.inject₁ ⟩ - [ h₁ ∘ i₁ , h₁ ∘ i₂ ] ≈⟨ +-g-η ⟩ - h₁ ∎ - inject₂ - : {X : Obj} - {h₁ : A₁ + A₂ ⇒ X} - {h₂ : B₁ + B₂ ⇒ X} - → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₂-₁ +₁ i₂-₂) ≈ h₂ - inject₂ {_} {h₁} {h₂} = begin - [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₂-₁ +₁ i₂-₂) ≈⟨ []∘+₁ ⟩ - [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] ∘ i₂-₁ , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ∘ i₂-₂ ] ≈⟨ []-cong₂ Coprod₁.inject₂ Coprod₂.inject₂ ⟩ - [ h₂ ∘ i₁ , h₂ ∘ i₂ ] ≈⟨ +-g-η ⟩ - h₂ ∎ - unique - : {X : Obj} - {i : C₁ + C₂ ⇒ X} - {h₁ : A₁ + A₂ ⇒ X} - {h₂ : B₁ + B₂ ⇒ X} - (eq₁ : i ∘ (i₁-₁ +₁ i₁-₂) ≈ h₁) - (eq₂ : i ∘ (i₂-₁ +₁ i₂-₂) ≈ h₂) - → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ≈ i - unique {X} {i} {h₁} {h₂} eq₁ eq₂ = begin - [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ≈⟨ []-cong₂ (Coprod₁.unique eq₁-₁ eq₂-₁) (Coprod₂.unique eq₁-₂ eq₂-₂) ⟩ - [ i ∘ i₁ , i ∘ i₂ ] ≈⟨ +-g-η ⟩ - i ∎ - where - eq₁-₁ : (i ∘ i₁) ∘ i₁-₁ ≈ h₁ ∘ i₁ - eq₁-₁ = begin - (i ∘ i₁) ∘ i₁-₁ ≈⟨ pushʳ +₁∘i₁ ⟨ - i ∘ (i₁-₁ +₁ i₁-₂) ∘ i₁ ≈⟨ pullˡ eq₁ ⟩ - h₁ ∘ i₁ ∎ - eq₂-₁ : (i ∘ i₁) ∘ i₂-₁ ≈ h₂ ∘ i₁ - eq₂-₁ = begin - (i ∘ i₁) ∘ i₂-₁ ≈⟨ pushʳ +₁∘i₁ ⟨ - i ∘ (i₂-₁ +₁ i₂-₂) ∘ i₁ ≈⟨ pullˡ eq₂ ⟩ - h₂ ∘ i₁ ∎ - eq₁-₂ : (i ∘ i₂) ∘ i₁-₂ ≈ h₁ ∘ i₂ - eq₁-₂ = begin - (i ∘ i₂) ∘ i₁-₂ ≈⟨ pushʳ +₁∘i₂ ⟨ - i ∘ (i₁-₁ +₁ i₁-₂) ∘ i₂ ≈⟨ pullˡ eq₁ ⟩ - h₁ ∘ i₂ ∎ - eq₂-₂ : (i ∘ i₂) ∘ i₂-₂ ≈ h₂ ∘ i₂ - eq₂-₂ = begin - (i ∘ i₂) ∘ i₂-₂ ≈⟨ pushʳ +₁∘i₂ ⟨ - i ∘ (i₂-₁ +₁ i₂-₂) ∘ i₂ ≈⟨ pullˡ eq₂ ⟩ - h₂ ∘ i₂ ∎ - - +-resp-coeq - : {(A₁ , A₂) (B₁ , B₂) (C₁ , C₂) : 𝒞×𝒞.Obj} - {(f₁ , f₂) (g₁ , g₂) : (A₁ ⇒ B₁) ×′ (A₂ ⇒ B₂)} - {(h₁ , h₂) : (B₁ ⇒ C₁) ×′ (B₂ ⇒ C₂)} - → IsCoequalizer 𝒞×𝒞.U (f₁ , f₂) (g₁ , g₂) (h₁ , h₂) - → IsCoequalizer 𝒞.U (f₁ +₁ f₂) (g₁ +₁ g₂) (h₁ +₁ h₂) - +-resp-coeq {A₁ , A₂} {B₁ , B₂} {C₁ , C₂} {f₁ , f₂} {g₁ , g₂} {h₁ , h₂} isCoeq = record - { equality = sym -+-.homomorphism ○ []-cong₂ (refl⟩∘⟨ Coeq₁.equality) (refl⟩∘⟨ Coeq₂.equality) ○ -+-.homomorphism - ; coequalize = coequalize - ; universal = universal _ - ; unique = uniq _ - } - where - open IsRightExact - open RightExactFunctor - module Coeq₁ = IsCoequalizer (F-resp-coeq (isRightExact (π₁ {𝒞} {𝒞})) isCoeq) - module Coeq₂ = IsCoequalizer (F-resp-coeq (isRightExact (π₂ {𝒞} {𝒞})) isCoeq) - open 𝒞 using ([]-cong₂; +₁∘i₁; +₁∘i₂; []∘+₁; +-g-η) - open 𝒞 using (Obj; _≈_; module HomReasoning; assoc; sym-assoc) - open 𝒞.HomReasoning - open ⇒-Reasoning 𝒞.U - - module _ {X : Obj} {k : B₁ + B₂ ⇒ X} (eq : k ∘ (f₁ +₁ f₂) ≈ k ∘ (g₁ +₁ g₂)) where - - eq₁ : (k ∘ i₁) ∘ f₁ ≈ (k ∘ i₁) ∘ g₁ - eq₁ = begin - (k ∘ i₁) ∘ f₁ ≈⟨ pushʳ +₁∘i₁ ⟨ - k ∘ (f₁ +₁ f₂) ∘ i₁ ≈⟨ extendʳ eq ⟩ - k ∘ (g₁ +₁ g₂) ∘ i₁ ≈⟨ pushʳ +₁∘i₁ ⟩ - (k ∘ i₁) ∘ g₁ ∎ - - eq₂ : (k ∘ i₂) ∘ f₂ ≈ (k ∘ i₂) ∘ g₂ - eq₂ = begin - (k ∘ i₂) ∘ f₂ ≈⟨ pushʳ +₁∘i₂ ⟨ - k ∘ (f₁ +₁ f₂) ∘ i₂ ≈⟨ extendʳ eq ⟩ - k ∘ (g₁ +₁ g₂) ∘ i₂ ≈⟨ pushʳ +₁∘i₂ ⟩ - (k ∘ i₂) ∘ g₂ ∎ - - coequalize : C₁ + C₂ ⇒ X - coequalize = [ Coeq₁.coequalize eq₁ , Coeq₂.coequalize eq₂ ] - - universal : k ≈ coequalize ∘ (h₁ +₁ h₂) - universal = begin - k ≈⟨ +-g-η ⟨ - [ k ∘ i₁ , k ∘ i₂ ] ≈⟨ []-cong₂ Coeq₁.universal Coeq₂.universal ⟩ - [ Coeq₁.coequalize eq₁ ∘ h₁ , Coeq₂.coequalize eq₂ ∘ h₂ ] ≈⟨ []∘+₁ ⟨ - coequalize ∘ (h₁ +₁ h₂) ∎ - - uniq : {i : C₁ + C₂ ⇒ X} → k ≈ i ∘ (h₁ +₁ h₂) → i ≈ coequalize - uniq {i} eq′ = begin - i ≈⟨ +-g-η ⟨ - [ i ∘ i₁ , i ∘ i₂ ] ≈⟨ []-cong₂ (Coeq₁.unique eq₁′) (Coeq₂.unique eq₂′) ⟩ - [ Coeq₁.coequalize eq₁ , Coeq₂.coequalize eq₂ ] ∎ - where - eq₁′ : k ∘ i₁ ≈ (i ∘ i₁) ∘ h₁ - eq₁′ = eq′ ⟩∘⟨refl ○ extendˡ +₁∘i₁ - eq₂′ : k ∘ i₂ ≈ (i ∘ i₂) ∘ h₂ - eq₂′ = eq′ ⟩∘⟨refl ○ extendˡ +₁∘i₂ - -module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} where - - open FinCoCom using (_⇒_; _∘_; id) - module 𝒞 = FinitelyCocompleteCategory 𝒞 - - -+- : 𝒞 × 𝒞 ⇒ 𝒞 - -+- = record - { F = 𝒞.-+- - ; isRightExact = record - { F-resp-⊥ = +-resp-⊥ 𝒞 - ; F-resp-+ = +-resp-+ 𝒞 - ; F-resp-coeq = +-resp-coeq 𝒞 - } - } - - [x+y]+z : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞 - [x+y]+z = -+- ∘ (-+- ×₁ id) - - x+[y+z] : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞 - x+[y+z] = -+- ∘ (id ×₁ -+-) ∘ assocˡ diff --git a/Category/Instance/Properties/SymMonCat.agda b/Category/Instance/Properties/SymMonCat.agda new file mode 100644 index 0000000..fa15295 --- /dev/null +++ b/Category/Instance/Properties/SymMonCat.agda @@ -0,0 +1,166 @@ +{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --lossy-unification #-} + +open import Level using (Level; suc; _⊔_) +module Category.Instance.Properties.SymMonCat {o ℓ e : Level} where + +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric as SMNI +import Categories.Functor.Monoidal.Symmetric {o} {o} {ℓ} {ℓ} {e} {e} as SMF + +open import Category.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat) + +open import Categories.Category using (Category; _[_≈_]; _[_∘_]) +open import Categories.Object.Product.Core SymMonCat using (Product) +open import Categories.Object.Terminal SymMonCat using (Terminal) +open import Categories.Category.Instance.One using (One) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Categories.Category.Cartesian SymMonCat using (Cartesian) +open import Categories.Category.Cartesian.Bundle using (CartesianCategory) +open import Categories.Functor.Monoidal.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal) +open import Categories.Category.BinaryProducts SymMonCat using (BinaryProducts) +open import Categories.Functor.Monoidal.Construction.Product + using () + renaming + ( πˡ-SymmetricMonoidalFunctor to πˡ-SMF + ; πʳ-SymmetricMonoidalFunctor to πʳ-SMF + ; ※-SymmetricMonoidalFunctor to ※-SMF + ) +open import Categories.Category.Monoidal.Construction.Product using (Product-SymmetricMonoidalCategory) +open import Categories.Category.Product.Properties using () renaming (project₁ to p₁; project₂ to p₂; unique to u) +open import Data.Product.Base using (_,_; proj₁; proj₂) + +open SMF.Lax using (SymmetricMonoidalFunctor) +open SMNI.Lax using (SymmetricMonoidalNaturalIsomorphism; id; isEquivalence) + +module Cone + {A B X : SymmetricMonoidalCategory o ℓ e} + {F : SymmetricMonoidalFunctor X A} + {G : SymmetricMonoidalFunctor X B} where + + module A = SymmetricMonoidalCategory A + module B = SymmetricMonoidalCategory B + module X = SymmetricMonoidalCategory X + module F = SymmetricMonoidalFunctor X A F + module G = SymmetricMonoidalFunctor X B G + + A×B : SymmetricMonoidalCategory o ℓ e + A×B = (Product-SymmetricMonoidalCategory A B) + + πˡ : SymmetricMonoidalFunctor A×B A + πˡ = πˡ-SMF {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} + + πʳ : SymmetricMonoidalFunctor A×B B + πʳ = πʳ-SMF {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} + + module _ where + open Category A.U + open Equiv + open ⇒-Reasoning A.U + open ⊗-Reasoning A.monoidal + project₁ : SymMonCat [ SymMonCat [ πˡ ∘ ※-SMF F G ] ≈ F ] + project₁ = record + { U = p₁ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {X.U} {F.F} {G.F} + ; F⇒G-isMonoidal = record + { ε-compat = identityˡ ○ identityʳ + ; ⊗-homo-compat = λ { {C} {D} → identityˡ ○ refl⟩∘⟨ sym A.⊗.identity } + } + } + module _ (H : SymmetricMonoidalFunctor X A×B) (eq₁ : SymMonCat [ SymMonCat [ πˡ ∘ H ] ≈ F ]) where + private + module H = SymmetricMonoidalFunctor X A×B H + open SymmetricMonoidalNaturalIsomorphism eq₁ + ε-compat₁ : ⇐.η X.unit A.∘ F.ε A.≈ H.ε .proj₁ + ε-compat₁ = refl⟩∘⟨ sym ε-compat ○ cancelˡ (iso.isoˡ X.unit) ○ identityʳ + ⊗-homo-compat₁ + : ∀ {C D} + → ⇐.η (X.⊗.₀ (C , D)) ∘ F.⊗-homo.η (C , D) + ≈ H.⊗-homo.η (C , D) .proj₁ ∘ A.⊗.₁ (⇐.η C , ⇐.η D) + ⊗-homo-compat₁ {C} {D} = + insertʳ + (sym ⊗-distrib-over-∘ + ○ iso.isoʳ C ⟩⊗⟨ iso.isoʳ D + ○ A.⊗.identity) + ○ (pullʳ (sym ⊗-homo-compat) + ○ cancelˡ (iso.isoˡ (X.⊗.₀ (C , D))) + ○ identityʳ) ⟩∘⟨refl + + module _ where + open Category B.U + open Equiv + open ⇒-Reasoning B.U + open ⊗-Reasoning B.monoidal + project₂ : SymMonCat [ SymMonCat [ πʳ ∘ ※-SMF F G ] ≈ G ] + project₂ = record + { U = p₂ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {X.U} {F.F} {G.F} + ; F⇒G-isMonoidal = record + { ε-compat = identityˡ ○ identityʳ + ; ⊗-homo-compat = λ { {C} {D} → identityˡ ○ refl⟩∘⟨ sym B.⊗.identity } + } + } + module _ (H : SymmetricMonoidalFunctor X A×B) (eq₂ : SymMonCat [ SymMonCat [ πʳ ∘ H ] ≈ G ]) where + private + module H = SymmetricMonoidalFunctor X A×B H + open SymmetricMonoidalNaturalIsomorphism eq₂ + ε-compat₂ : ⇐.η X.unit ∘ G.ε ≈ H.ε .proj₂ + ε-compat₂ = refl⟩∘⟨ sym ε-compat ○ cancelˡ (iso.isoˡ X.unit) ○ identityʳ + ⊗-homo-compat₂ + : ∀ {C D} + → ⇐.η (X.⊗.₀ (C , D)) ∘ G.⊗-homo.η (C , D) + ≈ H.⊗-homo.η (C , D) .proj₂ ∘ B.⊗.₁ (⇐.η C , ⇐.η D) + ⊗-homo-compat₂ {C} {D} = + insertʳ + (sym ⊗-distrib-over-∘ + ○ iso.isoʳ C ⟩⊗⟨ iso.isoʳ D + ○ B.⊗.identity) + ○ (pullʳ (sym ⊗-homo-compat) + ○ cancelˡ (iso.isoˡ (X.⊗.₀ (C , D))) + ○ identityʳ) ⟩∘⟨refl + + unique + : (H : SymmetricMonoidalFunctor X A×B) + → SymMonCat [ SymMonCat [ πˡ ∘ H ] ≈ F ] + → SymMonCat [ SymMonCat [ πʳ ∘ H ] ≈ G ] + → SymMonCat [ ※-SMF F G ≈ H ] + unique H eq₁ eq₂ = record + { U = u {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {X.U} {F.F} {G.F} {H.F} eq₁.U eq₂.U + ; F⇒G-isMonoidal = record + { ε-compat = ε-compat₁ H eq₁ , ε-compat₂ H eq₂ + ; ⊗-homo-compat = ⊗-homo-compat₁ H eq₁ , ⊗-homo-compat₂ H eq₂ + } + } + where + module H = SymmetricMonoidalFunctor X A×B H + module eq₁ = SymmetricMonoidalNaturalIsomorphism eq₁ + module eq₂ = SymmetricMonoidalNaturalIsomorphism eq₂ + +prod-SymMonCat : ∀ {A B} → Product A B +prod-SymMonCat {A} {B} = record + { A×B = Product-SymmetricMonoidalCategory A B + ; π₁ = πˡ-SMF {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} + ; π₂ = πʳ-SMF {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} + ; ⟨_,_⟩ = ※-SMF + ; project₁ = λ { {X} {f} {g} → Cone.project₁ {A} {B} {X} {f} {g} } + ; project₂ = λ { {X} {f} {g} → Cone.project₂ {A} {B} {X} {f} {g} } + ; unique = λ { {X} {h} {f} {g} eq₁ eq₂ → Cone.unique {A} {B} {X} {f} {g} h eq₁ eq₂ } + } + +SymMonCat-BinaryProducts : BinaryProducts +SymMonCat-BinaryProducts = record { product = prod-SymMonCat } + +SymMonCat-Terminal : Terminal +SymMonCat-Terminal = record + { ⊤ = record + { U = One + ; monoidal = _ + ; symmetric = _ + } + ; ⊤-is-terminal = _ + } + +SymMonCat-Cartesian : Cartesian +SymMonCat-Cartesian = record + { terminal = SymMonCat-Terminal + ; products = SymMonCat-BinaryProducts + } diff --git a/Category/Instance/SymMonCat.agda b/Category/Instance/SymMonCat.agda new file mode 100644 index 0000000..e4b136c --- /dev/null +++ b/Category/Instance/SymMonCat.agda @@ -0,0 +1,74 @@ +{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --lossy-unification #-} + +open import Level using (Level; suc; _⊔_) +module Category.Instance.SymMonCat {o ℓ e : Level} where + +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +import Categories.Functor.Monoidal.Symmetric as SMF +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Categories.Morphism as Morphism +import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric as SMNI +import Categories.Category.Monoidal.Utilities as MonoidalUtil +import Categories.Category.Monoidal.Braided.Properties as BraidedProperties +open import Relation.Binary.Core using (Rel) + +open import Categories.Category using (Category; _[_,_]; _[_∘_]) +open import Categories.Category.Helper using (categoryHelper) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Categories.Functor.Monoidal.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal) + +open SMF.Lax using (SymmetricMonoidalFunctor) +open SMNI.Lax using (SymmetricMonoidalNaturalIsomorphism; id; isEquivalence) + +assoc + : {A B C D : SymmetricMonoidalCategory o ℓ e} + {F : SymmetricMonoidalFunctor A B} + {G : SymmetricMonoidalFunctor B C} + {H : SymmetricMonoidalFunctor C D} + → SymmetricMonoidalNaturalIsomorphism + (∘-SymmetricMonoidal (∘-SymmetricMonoidal H G) F) + (∘-SymmetricMonoidal H (∘-SymmetricMonoidal G F)) +assoc {A} {B} {C} {D} {F} {G} {H} = SMNI.Lax.associator {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {D} {F} {G} {H} + +identityˡ + : {A B : SymmetricMonoidalCategory o ℓ e} + {F : SymmetricMonoidalFunctor A B} + → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal (idF-SymmetricMonoidal B) F) F +identityˡ {A} {B} {F} = SMNI.Lax.unitorˡ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F} + +identityʳ + : {A B : SymmetricMonoidalCategory o ℓ e} + {F : SymmetricMonoidalFunctor A B} + → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal F (idF-SymmetricMonoidal A)) F +identityʳ {A} {B} {F} = SMNI.Lax.unitorʳ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F} + +Compose + : {A B C : SymmetricMonoidalCategory o ℓ e} + → SymmetricMonoidalFunctor B C + → SymmetricMonoidalFunctor A B + → SymmetricMonoidalFunctor A C +Compose {A} {B} {C} F G = ∘-SymmetricMonoidal {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} F G + +∘-resp-≈ + : {A B C : SymmetricMonoidalCategory o ℓ e} + {f h : SymmetricMonoidalFunctor B C} + {g i : SymmetricMonoidalFunctor A B} + → SymmetricMonoidalNaturalIsomorphism f h + → SymmetricMonoidalNaturalIsomorphism g i + → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal f g) (∘-SymmetricMonoidal h i) +∘-resp-≈ {A} {B} {C} {F} {F′} {G} {G′} F≃F′ G≃G′ = SMNI.Lax._ⓘₕ_ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {G} {G′} {F} {F′} F≃F′ G≃G′ + +SymMonCat : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) +SymMonCat = categoryHelper record + { Obj = SymmetricMonoidalCategory o ℓ e + ; _⇒_ = SymmetricMonoidalFunctor {o} {o} {ℓ} {ℓ} {e} {e} + ; _≈_ = λ { {A} {B} → SymmetricMonoidalNaturalIsomorphism {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} } + ; id = λ { {X} → idF-SymmetricMonoidal X } + ; _∘_ = λ { {A} {B} {C} F G → Compose {A} {B} {C} F G } + ; assoc = λ { {A} {B} {C} {D} {F} {G} {H} → assoc {A} {B} {C} {D} {F} {G} {H} } + ; identityˡ = λ { {A} {B} {F} → identityˡ {A} {B} {F} } + ; identityʳ = λ { {A} {B} {F} → identityʳ {A} {B} {F} } + ; equiv = isEquivalence + ; ∘-resp-≈ = λ { {A} {B} {C} {f} {h} {g} {i} f≈h g≈i → ∘-resp-≈ {A} {B} {C} {f} {h} {g} {i} f≈h g≈i } + } |