From a408cbee9abbe2dbeee09bd36afc678efe7b6557 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Fri, 10 Jul 2026 17:21:14 -0700 Subject: Use latest agda-categories --- .../Cartesian/Instance/FinitelyCocompletes.agda | 17 ++-- Category/Cocomplete/Finitely/Product.agda | 20 +++-- .../Cocomplete/Finitely/SymmetricMonoidal.agda | 4 +- Category/Dagger/Semiadditive.agda | 34 ++++---- Category/Instance/DecoratedCospans.agda | 36 +++------ Category/Instance/FinitelyCocompletes.agda | 24 +++--- Category/Instance/One/Properties.agda | 2 +- Category/Instance/Setoids/SymmetricMonoidal.agda | 4 +- Category/Monoidal/Instance/Cospans.agda | 9 +-- .../Instance/DecoratedCospans/Products.agda | 10 +-- Category/Monoidal/Instance/Nat.agda | 12 +-- Data/Matrix/SemiadditiveDagger.agda | 8 +- .../SymmetricMonoidal/FinitelyCocomplete.agda | 12 +-- Functor/Exact/Instance/Swap.agda | 10 +-- Functor/Instance/CMonoidalize.agda | 2 +- Functor/Instance/Cospan/Stack.agda | 3 +- Functor/Instance/Decorate.agda | 9 ++- Functor/Instance/DecoratedCospan/Embed.agda | 14 ++-- Functor/Instance/DecoratedCospan/Stack.agda | 35 ++++----- Functor/Instance/Monoidalize.agda | 4 +- .../SymmetricMonoidal/FinitelyCocomplete.agda | 90 +++++++++++----------- Functor/Monoidal/Construction/CMonoidValued.agda | 2 +- Functor/Monoidal/Construction/MonoidValued.agda | 4 +- 23 files changed, 164 insertions(+), 201 deletions(-) diff --git a/Category/Cartesian/Instance/FinitelyCocompletes.agda b/Category/Cartesian/Instance/FinitelyCocompletes.agda index 8c779d5..c44388a 100644 --- a/Category/Cartesian/Instance/FinitelyCocompletes.agda +++ b/Category/Cartesian/Instance/FinitelyCocompletes.agda @@ -7,7 +7,6 @@ module Category.Cartesian.Instance.FinitelyCocompletes {o ℓ e : Level} where import Categories.Morphism as Morphism import Categories.Morphism.Reasoning as ⇒-Reasoning -open import Categories.Category.BinaryProducts using (BinaryProducts) open import Categories.Category.Cartesian.Bundle using (CartesianCategory) open import Categories.Diagram.Coequalizer using (IsCoequalizer) open import Categories.Functor.Bifunctor using (flip-bifunctor) @@ -30,7 +29,7 @@ FinitelyCocompletes-CC = record } module FinCoCom = CartesianCategory FinitelyCocompletes-CC -open BinaryProducts (FinCoCom.products) using (_×_; π₁; π₂; _⁂_; assocˡ) -- hiding (unique) +open FinCoCom using (_×_; π₁; π₂; assocˡ) module _ (𝒞 : FinitelyCocompleteCategory o ℓ e) where @@ -49,8 +48,8 @@ module _ (𝒞 : FinitelyCocompleteCategory o ℓ e) where → IsInitial 𝒞×𝒞.U (A , B) → IsInitial 𝒞×𝒞.U (B , A) flip-IsInitial isInitial = let open IsInitial isInitial in record - { ! = swap ! - ; !-unique = swap ∘′ !-unique ∘′ swap + { ¡ = swap ¡ + ; ¡-unique = swap ∘′ ¡-unique ∘′ swap } flip-IsCoproduct @@ -84,8 +83,8 @@ module _ (𝒞 : FinitelyCocompleteCategory o ℓ e) where → 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₂))) + { ¡ = [ A-isInitial.¡ , B-isInitial.¡ ] + ; ¡-unique = λ f → +-unique (sym (A-isInitial.¡-unique (f ∘ i₁))) (sym (B-isInitial.¡-unique (f ∘ i₂))) } where open IsRightExact @@ -269,10 +268,6 @@ module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} where module 𝒞×𝒞×𝒞 = FinitelyCocompleteCategory ((𝒞 × 𝒞) × 𝒞) open Morphism U using (_≅_; module ≅) module +-assoc {X} {Y} {Z} = _≅_ (≅.sym (+-assoc {X} {Y} {Z})) - open import Categories.Object.Duality 𝒞.U using (Coproduct⇒coProduct) - op-binaryProducts : BinaryProducts op - op-binaryProducts = record { product = Coproduct⇒coProduct coproduct } - open BinaryProducts op-binaryProducts using () renaming (assocʳ∘⁂ to +₁∘assocˡ) open Equiv commute : {((X , Y) , Z) : 𝒞×𝒞×𝒞.Obj} @@ -280,4 +275,4 @@ module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} where → (F : ((X , Y) , Z) 𝒞×𝒞×𝒞.⇒ ((X′ , Y′) , Z′)) → (+-assoc.from 𝒞.∘ [x+y]+z.₁ F) ≈ (x+[y+z].₁ F 𝒞.∘ +-assoc.from) - commute {(X , Y) , Z} {(X′ , Y′) , Z′} ((F , G) , H) = sym +₁∘assocˡ + commute {(X , Y) , Z} {(X′ , Y′) , Z′} ((F , G) , H) = sym +₁∘+-assocʳ diff --git a/Category/Cocomplete/Finitely/Product.agda b/Category/Cocomplete/Finitely/Product.agda index 25dc346..4b74171 100644 --- a/Category/Cocomplete/Finitely/Product.agda +++ b/Category/Cocomplete/Finitely/Product.agda @@ -6,20 +6,21 @@ open import Level using (Level) module Category.Cocomplete.Finitely.Product {o ℓ e : Level} {𝒞 𝒟 : Category o ℓ e} where open import Categories.Category using (_[_,_]) +open import Categories.Category.BinaryCoproducts using (BinaryCoproducts) +open import Categories.Category.Cocartesian using (Cocartesian) open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete) -open import Categories.Category.Cocartesian using (Cocartesian; BinaryCoproducts) open import Categories.Category.Product using (Product) open import Categories.Diagram.Coequalizer using (Coequalizer) open import Categories.Object.Coproduct using (Coproduct) open import Categories.Object.Initial using (IsInitial; Initial) -open import Data.Product.Base using (_,_; _×_; dmap; zip; map) +open import Data.Product using (_,_; _×_; dmap; zip; map) Initial-× : Initial 𝒞 → Initial 𝒟 → Initial (Product 𝒞 𝒟) Initial-× initial-𝒞 initial-𝒟 = record { ⊥ = 𝒞.⊥ , 𝒟.⊥ ; ⊥-is-initial = record - { ! = 𝒞.! , 𝒟.! - ; !-unique = dmap 𝒞.!-unique 𝒟.!-unique + { ¡ = 𝒞.¡ , 𝒟.¡ + ; ¡-unique = dmap 𝒞.¡-unique 𝒟.¡-unique } } where @@ -31,20 +32,17 @@ Coproducts-× coproducts-𝒞 coproducts-𝒟 = record { coproduct = coproduct } where coproduct : ∀ {(A₁ , B₁) (A₂ , B₂) : _ × _} → Coproduct (Product 𝒞 𝒟) (A₁ , B₁) (A₂ , B₂) coproduct = record - { A+B = 𝒞.A+B , 𝒟.A+B + { A+B = _ 𝒞.+ _ , _ 𝒟.+ _ ; i₁ = 𝒞.i₁ , 𝒟.i₁ ; i₂ = 𝒞.i₂ , 𝒟.i₂ ; [_,_] = zip 𝒞.[_,_] 𝒟.[_,_] ; inject₁ = 𝒞.inject₁ , 𝒟.inject₁ ; inject₂ = 𝒞.inject₂ , 𝒟.inject₂ - ; unique = zip 𝒞.unique 𝒟.unique + ; unique = zip 𝒞.+-unique 𝒟.+-unique } where - module Coprod {𝒞} (coprods : BinaryCoproducts 𝒞) where - open BinaryCoproducts coprods using (coproduct) - open coproduct public - module 𝒞 = Coprod coproducts-𝒞 - module 𝒟 = Coprod coproducts-𝒟 + module 𝒞 = BinaryCoproducts coproducts-𝒞 + module 𝒟 = BinaryCoproducts coproducts-𝒟 Coequalizer-× : (∀ {A} {B} (f g : 𝒞 [ A , B ]) → Coequalizer 𝒞 f g) diff --git a/Category/Cocomplete/Finitely/SymmetricMonoidal.agda b/Category/Cocomplete/Finitely/SymmetricMonoidal.agda index 2b66d19..bae9774 100644 --- a/Category/Cocomplete/Finitely/SymmetricMonoidal.agda +++ b/Category/Cocomplete/Finitely/SymmetricMonoidal.agda @@ -5,8 +5,8 @@ open import Categories.Category.Core using (Category) module Category.Cocomplete.Finitely.SymmetricMonoidal {o ℓ e} {𝒞 : Category o ℓ e} where open import Categories.Category.Cocomplete.Finitely 𝒞 using (FinitelyCocomplete) -open import Categories.Category.Cocartesian 𝒞 using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal) - +open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal) +open import Categories.Category.Cocartesian.SymmetricMonoidal 𝒞 using (module CocartesianSymmetricMonoidal) module FinitelyCocompleteSymmetricMonoidal (finCo : FinitelyCocomplete) where diff --git a/Category/Dagger/Semiadditive.agda b/Category/Dagger/Semiadditive.agda index 283f270..bf8c929 100644 --- a/Category/Dagger/Semiadditive.agda +++ b/Category/Dagger/Semiadditive.agda @@ -3,21 +3,20 @@ open import Level using (Level; suc; _⊔_) open import Categories.Category using (Category) -module Category.Dagger.Semiadditive - {o ℓ e : Level} - (𝒞 : Category o ℓ e) - where +module Category.Dagger.Semiadditive {o ℓ e : Level} (𝒞 : Category o ℓ e) where import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning import Categories.Morphism.Reasoning as ⇒-Reasoning -open import Categories.Category.BinaryProducts using (BinaryProducts) -open import Categories.Category.Cocartesian 𝒞 using (Cocartesian; module CocartesianMonoidal; module CocartesianSymmetricMonoidal) +open import Categories.Category.Cocartesian 𝒞 using (Cocartesian) +open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal) +open import Categories.Category.Cocartesian.SymmetricMonoidal using (module CocartesianSymmetricMonoidal) open import Categories.Category.Dagger using (HasDagger) open import Categories.Category.Monoidal using (Monoidal) open import Categories.Category.Monoidal.Symmetric using (module Symmetric) open import Categories.Category.Monoidal.Symmetric.Properties using () renaming (module Shorthands to σ-Shorthands) open import Categories.Category.Monoidal.Utilities using (module Shorthands) +open import Categories.Functor using (Functor) open import Categories.Object.Duality using (Coproduct⇒coProduct) open import Relation.Binary using (Rel) @@ -27,9 +26,9 @@ record DaggerCocartesianMonoidal : Set (suc (o ⊔ ℓ ⊔ e)) where cocartesian : Cocartesian dagger : HasDagger 𝒞 - open Cocartesian cocartesian using (i₁; i₂) - open CocartesianMonoidal cocartesian using (+-monoidal; _⊗₀_; _⊗₁_) - open CocartesianSymmetricMonoidal cocartesian using (+-symmetric) + open Cocartesian cocartesian using (i₁; i₂) renaming (_+₁_ to _⊗₁_) + open CocartesianMonoidal cocartesian using (+-monoidal) + open CocartesianSymmetricMonoidal 𝒞 cocartesian using (+-symmetric) open HasDagger dagger using (_†; isUnitary; isSelfAdjoint) open Shorthands +-monoidal using (λ⇒; λ⇐; ρ⇒; ρ⇐; α⇒; α⇐) open σ-Shorthands +-symmetric using (σ⇒) @@ -49,11 +48,11 @@ record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where daggerCocartesianMonoidal : DaggerCocartesianMonoidal open DaggerCocartesianMonoidal daggerCocartesianMonoidal public - open CocartesianMonoidal cocartesian using (+-monoidal) renaming (_⊗₀_ to _⊕₀_; _⊗₁_ to _⊕₁_; ⊗ to ⊕) public - + open Cocartesian cocartesian using ([]∘+-assocʳ; []∘+-swap) renaming (_+_ to _⊕₀_; _+₁_ to infixr 10 _⊕₁_; -+- to ⊕) public + open CocartesianMonoidal cocartesian using (+-monoidal) public open Cocartesian cocartesian using (i₁; i₂; ¡) public open Cocartesian cocartesian using (⊥; [_,_]; ∘[]; []∘+₁; []-cong₂; coproduct; ¡-unique; inject₁; inject₂; +-unique; +-g-η) - open CocartesianSymmetricMonoidal cocartesian using (+-symmetric) + open CocartesianSymmetricMonoidal 𝒞 cocartesian using (+-symmetric) open HasDagger dagger using (_†; †-involutive; ⟨_⟩†; †-identity; †-homomorphism) public open Monoidal +-monoidal using (unitorˡ-commute-from; unitorʳ-commute-from; assoc-commute-from; module unitorˡ; module unitorʳ; module associator) open σ-Shorthands +-symmetric using (σ⇒) @@ -61,6 +60,8 @@ record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where open Shorthands +-monoidal using (λ⇒; λ⇐; ρ⇒; ρ⇐; α⇒; α⇐) open Category 𝒞 + module ⊕ = Functor ⊕ + -- projection maps p₁ : {A B : Obj} → A ⊕₀ B ⇒ A p₁ = i₁ † @@ -76,11 +77,6 @@ record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where △ : {A : Obj} → A ⇒ A ⊕₀ A △ = ▽ † - private - op-binaryProducts : BinaryProducts op - op-binaryProducts = record { product = Coproduct⇒coProduct 𝒞 coproduct } - open BinaryProducts op-binaryProducts using () renaming (assocʳ∘⟨⟩ to []-assoc; swap∘⟨⟩ to []∘swap) - open ⊗-Reasoning +-monoidal open ⇒-Reasoning 𝒞 @@ -88,7 +84,7 @@ record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where ▽-assoc = begin [ id , id ] ∘ [ id , id ] ⊕₁ id ≈⟨ []∘+₁ ⟩ [ id ∘ [ id , id ] , id ∘ id ] ≈⟨ []-cong₂ identityˡ identityˡ ⟩ - [ [ id , id ] , id ] ≈⟨ []-assoc ⟨ + [ [ id , id ] , id ] ≈⟨ []∘+-assocʳ ⟨ [ id , [ id , id ] ] ∘ α⇒ ≈⟨ []-cong₂ identityˡ identityˡ ⟩∘⟨refl ⟨ [ id ∘ id , id ∘ [ id , id ] ] ∘ α⇒ ≈⟨ pushˡ (Equiv.sym []∘+₁) ⟩ [ id , id ] ∘ id ⊕₁ [ id , id ] ∘ α⇒ ∎ @@ -144,7 +140,7 @@ record SemiadditiveDagger : Set (suc (o ⊔ ℓ ⊔ e)) where ρ⇐  ∎ ▽-comm : {A : Obj} → ▽ {A} ∘ σ⇒ ≈ ▽ - ▽-comm = []∘swap + ▽-comm = []∘+-swap △-comm : {A : Obj} → σ⇒ ∘ △ {A} ≈ △ △-comm = begin diff --git a/Category/Instance/DecoratedCospans.agda b/Category/Instance/DecoratedCospans.agda index b527265..480803e 100644 --- a/Category/Instance/DecoratedCospans.agda +++ b/Category/Instance/DecoratedCospans.agda @@ -23,7 +23,7 @@ import Category.Instance.Cospans 𝒞 as Cospans import Category.Diagram.Cospan 𝒞 as Cospan open import Categories.Category using (Category; _[_∘_]) -open import Categories.Category.Cocartesian using (module CocartesianMonoidal) +open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal) open import Categories.Diagram.Pushout using (Pushout) open import Categories.Diagram.Pushout.Properties 𝒞.U using (up-to-iso) open import Categories.Functor.Properties using ([_]-resp-≅; [_]-resp-square) @@ -71,7 +71,7 @@ compose c₁ c₂ = record identity : DecoratedCospan A A identity = record { cospan = Cospan.identity - ; decoration = 𝒟.U [ F₁ 𝒞.initial.! ∘ ε ] + ; decoration = 𝒟.U [ F₁ 𝒞.¡ ∘ ε ] } record _≈_ (C₁ C₂ : DecoratedCospan A B) : Set (ℓ ⊔ e ⊔ e′) where @@ -222,10 +222,7 @@ compose-assoc {A} {B} {C} {D} {c₁} {c₂} {c₃} = record module _ where - open 𝒞 using (∘[]; []-congʳ; []-congˡ; []∘+₁) - open 𝒞.Dual.op-binaryProducts 𝒞.cocartesian - using () - renaming (⟨⟩-cong₂ to []-cong₂; assocˡ∘⟨⟩ to []∘assocˡ) + open 𝒞 using (∘[]; []-congʳ; []-congˡ; []∘+₁; []∘+-assocˡ; []-cong₂) open ⇒-Reasoning 𝒞.U open 𝒞 using (id; _∘_; _≈_; assoc; identityʳ) @@ -241,7 +238,7 @@ compose-assoc {A} {B} {C} {D} {c₁} {c₂} {c₃} = record [ (y ∘ f) ∘ id , (l ∘ k) ∘ [ h , i ] ] ≈⟨ []-cong₂ identityʳ ∘[] ⟩ [ y ∘ f , [ (l ∘ k) ∘ h , (l ∘ k) ∘ i ] ] ≈⟨ []-congˡ ([]-cong₂ (pullʳ (sym P₃.commute)) (assoc ○ P₂₃.universal∘i₂≈h₂)) ⟩ [ y ∘ f , [ l ∘ j ∘ g , z ] ] ≈⟨ []-congˡ ([]-congʳ (pullˡ P₂₃.universal∘i₁≈h₁)) ⟩ - [ y ∘ f , [ y ∘ g , z ] ] ≈⟨ []∘assocˡ ⟨ + [ y ∘ f , [ y ∘ g , z ] ] ≈⟨ []∘+-assocˡ ⟨ [ [ y ∘ f , y ∘ g ] , z ] ∘ +-assoc.from ≈⟨ []-cong₂ ∘[] identityʳ ⟩∘⟨refl ⟨ [ y ∘ [ f , g ] , z ∘ id ] ∘ +-assoc.from ≈⟨ pullˡ []∘+₁ ⟨ [ y , z ] ∘ ([ f , g ] +₁ id) ∘ +-assoc.from ∎ @@ -404,7 +401,7 @@ compose-idʳ {A} {_} {C} = record open 𝒞 using (cocartesian) renaming (id to id′; _∘_ to _∘′_) - open CocartesianMonoidal 𝒞.U cocartesian using (⊥+A≅A) + open CocartesianMonoidal cocartesian using (⊥+A≅A) module ⊥+A≅A {a} = _≅_ (⊥+A≅A {a}) module _ where open 𝒞 @@ -412,13 +409,10 @@ compose-idʳ {A} {_} {C} = record ( _⇒_ ; _∘_ ; _≈_ ; id ; U ; identity² ; cocartesian ; initial ; ¡-unique - ; ∘[] ; []∘+₁ ; inject₂ ; assoc - ; module HomReasoning ; module Dual ; module Equiv + ; ∘[] ; []∘+₁ ; inject₂ ; assoc ; []-cong₂ + ; module HomReasoning ; module Equiv ) open Equiv - open Dual.op-binaryProducts cocartesian - using () - renaming (⟨⟩-cong₂ to []-cong₂) open ⇒-Reasoning U open HomReasoning copairing-id : ((≅P.from ∘ [ i₁ , i₂ ]) ∘ (¡ +₁ id)) ∘ ⊥+A≅A.to 𝒞.≈ id @@ -502,7 +496,7 @@ compose-idˡ {_} {B} {C} = record using (cocartesian) renaming (id to id′; _∘_ to _∘′_) - open CocartesianMonoidal 𝒞.U cocartesian using (A+⊥≅A) + open CocartesianMonoidal cocartesian using (A+⊥≅A) module A+⊥≅A {a} = _≅_ (A+⊥≅A {a}) @@ -513,16 +507,12 @@ compose-idˡ {_} {B} {C} = record ( _⇒_ ; _∘_ ; _≈_ ; id ; U ; identity² ; cocartesian ; initial ; ¡-unique - ; ∘[] ; []∘+₁ ; inject₁ ; assoc - ; module HomReasoning ; module Dual ; module Equiv + ; ∘[] ; []∘+₁ ; inject₁ ; assoc ; []-cong₂ + ; module HomReasoning ; module Equiv ) open Equiv - open Dual.op-binaryProducts cocartesian - using () - renaming (⟨⟩-cong₂ to []-cong₂) - open ⇒-Reasoning U open HomReasoning @@ -652,11 +642,7 @@ compose-equiv {_} {_} {_} {c₂} {c₂′} {c₁} {c₁′} ≅C₂ ≅C₁ = re open ⊗-Util 𝒟.monoidal using (module Shorthands) open Shorthands using (ρ⇒; ρ⇐) - open 𝒞 using ([_,_]; ∘[]; _+_; _+₁_; []∘+₁) renaming (_∘_ to _∘′_) - open 𝒞.Dual.op-binaryProducts 𝒞.cocartesian - using () - renaming (⟨⟩-cong₂ to []-cong₂) - + open 𝒞 using ([_,_]; ∘[]; _+_; _+₁_; []∘+₁; []-cong₂) renaming (_∘_ to _∘′_) open 𝒟 φ[N,M] : F₀ N ⊗₀ F₀ M 𝒟.⇒ F₀ (N + M) diff --git a/Category/Instance/FinitelyCocompletes.agda b/Category/Instance/FinitelyCocompletes.agda index 9bee58e..ceb1d53 100644 --- a/Category/Instance/FinitelyCocompletes.agda +++ b/Category/Instance/FinitelyCocompletes.agda @@ -84,8 +84,8 @@ module _ (𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e) where → IsInitial 𝒞×𝒟.U (A , B) → IsInitial 𝒞.U A F-resp-⊥ {A , B} initial = record - { ! = λ { {C} → proj₁ (! {C , B}) } - ; !-unique = λ { f → proj₁ (!-unique (f , 𝒟.id)) } + { ¡ = λ { {C} → proj₁ (¡ {C , B}) } + ; ¡-unique = λ { f → proj₁ (¡-unique (f , 𝒟.id)) } } where open IsInitial initial @@ -130,8 +130,8 @@ module _ (𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e) where → IsInitial 𝒞×𝒟.U (A , B) → IsInitial 𝒟.U B F-resp-⊥ {A , B} initial = record - { ! = λ { {C} → proj₂ (! {A , C}) } - ; !-unique = λ { f → proj₂ (!-unique (𝒞.id , f)) } + { ¡ = λ { {C} → proj₂ (¡ {A , C}) } + ; ¡-unique = λ { f → proj₂ (¡-unique (𝒞.id , f)) } } where open IsInitial initial @@ -193,8 +193,8 @@ module _ where → IsInitial 𝒞.U A → IsInitial (ProductCat 𝒟.U ℰ.U) (F.₀ A , G.₀ A) F-resp-⊥′ A-isInitial = record - { ! = F[A]-isInitial.! , G[A]-isInitial.! - ; !-unique = dmap F[A]-isInitial.!-unique G[A]-isInitial.!-unique + { ¡ = F[A]-isInitial.¡ , G[A]-isInitial.¡ + ; ¡-unique = dmap F[A]-isInitial.¡-unique G[A]-isInitial.¡-unique } where module F[A]-isInitial = IsInitial (F-resp-⊥ A-isInitial) @@ -254,20 +254,20 @@ module _ where → IsInitial 𝒜×ℬ.U (A , B) → IsInitial 𝒞×𝒟.U (F.₀ A , G.₀ B) F-resp-⊥′ {A , B} A,B-isInitial = record - { ! = F[A]-isInitial.! , G[B]-isInitial.! - ; !-unique = dmap F[A]-isInitial.!-unique G[B]-isInitial.!-unique + { ¡ = F[A]-isInitial.¡ , G[B]-isInitial.¡ + ; ¡-unique = dmap F[A]-isInitial.¡-unique G[B]-isInitial.¡-unique } where module A,B-isInitial = IsInitial A,B-isInitial A-isInitial : IsInitial 𝒜.U A A-isInitial = record - { ! = λ { {X} → proj₁ (A,B-isInitial.! {X , B}) } - ; !-unique = λ { f → proj₁ (A,B-isInitial.!-unique (f , ℬ.id)) } + { ¡ = λ { {X} → proj₁ (A,B-isInitial.¡ {X , B}) } + ; ¡-unique = λ { f → proj₁ (A,B-isInitial.¡-unique (f , ℬ.id)) } } B-isInitial : IsInitial ℬ.U B B-isInitial = record - { ! = λ { {X} → proj₂ (A,B-isInitial.! {A , X}) } - ; !-unique = λ { f → proj₂ (A,B-isInitial.!-unique (𝒜.id , f)) } + { ¡ = λ { {X} → proj₂ (A,B-isInitial.¡ {A , X}) } + ; ¡-unique = λ { f → proj₂ (A,B-isInitial.¡-unique (𝒜.id , f)) } } module F[A]-isInitial = IsInitial (F-resp-⊥ A-isInitial) module G[B]-isInitial = IsInitial (G-resp-⊥ B-isInitial) diff --git a/Category/Instance/One/Properties.agda b/Category/Instance/One/Properties.agda index c6261bb..2d75139 100644 --- a/Category/Instance/One/Properties.agda +++ b/Category/Instance/One/Properties.agda @@ -13,7 +13,7 @@ One = One′ {o} {ℓ} {e} open import Categories.Category.Cocartesian One using (Cocartesian) open import Categories.Category.Cocomplete.Finitely One using (FinitelyCocomplete) open import Categories.Object.Initial One using (Initial) -open import Categories.Category.Cocartesian One using (BinaryCoproducts) +open import Categories.Category.BinaryCoproducts One using (BinaryCoproducts) initial : Initial diff --git a/Category/Instance/Setoids/SymmetricMonoidal.agda b/Category/Instance/Setoids/SymmetricMonoidal.agda index 995ddf3..e6c04d5 100644 --- a/Category/Instance/Setoids/SymmetricMonoidal.agda +++ b/Category/Instance/Setoids/SymmetricMonoidal.agda @@ -12,7 +12,9 @@ open import Categories.Category.Cartesian.SymmetricMonoidal (Setoids c ℓ) Seto using () renaming (symmetric to ×-symmetric) open import Categories.Category.Cocartesian (Setoids c (c ⊔ ℓ)) - using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal) +open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal) +open import Categories.Category.Cocartesian.SymmetricMonoidal (Setoids c (c ⊔ ℓ)) + using (module CocartesianSymmetricMonoidal) open CocartesianMonoidal (Setoids-Cocartesian {c} {ℓ}) using (+-monoidal) open CocartesianSymmetricMonoidal (Setoids-Cocartesian {c} {ℓ}) using (+-symmetric) diff --git a/Category/Monoidal/Instance/Cospans.agda b/Category/Monoidal/Instance/Cospans.agda index a1648db..187eaca 100644 --- a/Category/Monoidal/Instance/Cospans.agda +++ b/Category/Monoidal/Instance/Cospans.agda @@ -9,9 +9,9 @@ import Categories.Morphism as Morphism import Categories.Morphism.Reasoning.Iso as IsoReasoning open import Categories.Category using (_[_,_]; _[_≈_]; _[_∘_]; Category) -open import Categories.Category.BinaryProducts using (BinaryProducts) open import Categories.Category.Cartesian.Bundle using (CartesianCategory) -open import Categories.Category.Cocartesian using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal) +open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal) +open import Categories.Category.Cocartesian.SymmetricMonoidal using (module CocartesianSymmetricMonoidal) open import Categories.Category.Monoidal.Symmetric using (Symmetric) open import Categories.Category.Monoidal.Braided using (Braided) open import Categories.Category.Monoidal.Core using (Monoidal) @@ -27,7 +27,7 @@ open import Functor.Instance.Cospan.Stack 𝒞 using (⊗) open import Functor.Instance.Cospan.Embed 𝒞 using (L; L-resp-⊗) module 𝒞 = FinitelyCocompleteCategory 𝒞 -open CocartesianMonoidal 𝒞.U 𝒞.cocartesian using (⊥+--id; -+⊥-id; ⊥+A≅A; A+⊥≅A; +-monoidal) +open CocartesianMonoidal 𝒞.cocartesian using (⊥+--id; -+⊥-id; ⊥+A≅A; A+⊥≅A; +-monoidal) open CocartesianSymmetricMonoidal 𝒞.U 𝒞.cocartesian using (+-symmetric) open Monoidal +-monoidal using () renaming (triangle to tri; pentagon to pent) @@ -36,8 +36,7 @@ open import Categories.Category.Monoidal.Utilities +-monoidal using (associator- module _ where - open CartesianCategory FinitelyCocompletes-CC using (products) - open BinaryProducts products using (_×_) + open CartesianCategory FinitelyCocompletes-CC using (_×_) 𝒞×𝒞 : FinitelyCocompleteCategory o ℓ e 𝒞×𝒞 = 𝒞 × 𝒞 diff --git a/Category/Monoidal/Instance/DecoratedCospans/Products.agda b/Category/Monoidal/Instance/DecoratedCospans/Products.agda index 647f887..4fd323e 100644 --- a/Category/Monoidal/Instance/DecoratedCospans/Products.agda +++ b/Category/Monoidal/Instance/DecoratedCospans/Products.agda @@ -21,7 +21,6 @@ import Categories.Morphism.Reasoning as ⇒-Reasoning open import Categories.Category using (_[_,_]; _[_≈_]; _[_∘_]; Category) open import Categories.Category.Core using (Category) -open import Categories.Category.BinaryProducts using (BinaryProducts) open import Categories.Category.Cartesian using (Cartesian) open import Categories.Category.Cartesian.Bundle using (CartesianCategory) open import Categories.Functor using (Functor; _∘F_) renaming (id to idF) @@ -44,8 +43,7 @@ module 𝒟 = SymmetricMonoidalCategory 𝒟 module _ where - open CartesianCategory FinitelyCocompletes-CC using (products) - open BinaryProducts products using (_×_) + open CartesianCategory FinitelyCocompletes-CC using (_×_) 𝒞×𝒞 : FinitelyCocompleteCategory o ℓ e 𝒞×𝒞 = 𝒞 × 𝒞 @@ -57,8 +55,7 @@ module _ where module _ where - open Cartesian SymMonCat-Cartesian′ using (products) - open BinaryProducts products using (_×_; _⁂_) + open Cartesian SymMonCat-Cartesian′ using (_×_) 𝒟×𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′ 𝒟×𝒟 = 𝒟 × 𝒟 @@ -70,8 +67,7 @@ module _ where module _ where - open Cartesian SymMonCat-Cartesian using (products) - open BinaryProducts products using (_×_; _⁂_) + open Cartesian SymMonCat-Cartesian using (_×_) smc𝒞×𝒞 : SymmetricMonoidalCategory o ℓ e smc𝒞×𝒞 = smc 𝒞 × smc 𝒞 diff --git a/Category/Monoidal/Instance/Nat.agda b/Category/Monoidal/Instance/Nat.agda index 24b30a6..23ee39d 100644 --- a/Category/Monoidal/Instance/Nat.agda +++ b/Category/Monoidal/Instance/Nat.agda @@ -6,7 +6,9 @@ open import Level using (0ℓ) open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) open import Categories.Category.Instance.Nat using (Nat; Nat-Cartesian; Nat-Cocartesian; Natop) open import Categories.Category.Cartesian using (Cartesian) -open import Categories.Category.Cocartesian using (Cocartesian; module CocartesianMonoidal; module CocartesianSymmetricMonoidal) +open import Categories.Category.Cocartesian using (Cocartesian) +open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal) +open import Categories.Category.Cocartesian.SymmetricMonoidal using (module CocartesianSymmetricMonoidal) open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal) open import Categories.Category.Duality using (coCartesian⇒Cocartesian; Cocartesian⇒coCartesian) @@ -26,7 +28,7 @@ module Monoidal where Nat,+,0 : MonoidalCategory 0ℓ 0ℓ 0ℓ Nat,+,0 .U = Nat - Nat,+,0 .monoidal = +-monoidal Nat Nat-Cocartesian + Nat,+,0 .monoidal = +-monoidal Nat-Cocartesian Nat,×,1 : MonoidalCategory 0ℓ 0ℓ 0ℓ Nat,×,1 .U = Nat @@ -38,7 +40,7 @@ module Monoidal where Natop,×,1 : MonoidalCategory 0ℓ 0ℓ 0ℓ Natop,×,1 .U = Natop - Natop,×,1 .monoidal = +-monoidal Natop Natop-Cocartesian + Natop,×,1 .monoidal = +-monoidal Natop-Cocartesian module Symmetric where @@ -50,7 +52,7 @@ module Symmetric where Nat,+,0 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ Nat,+,0 .U = Nat - Nat,+,0 .monoidal = +-monoidal Nat Nat-Cocartesian + Nat,+,0 .monoidal = +-monoidal Nat-Cocartesian Nat,+,0 .symmetric = +-symmetric Nat Nat-Cocartesian Nat,×,1 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ @@ -65,7 +67,7 @@ module Symmetric where Natop,×,1 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ Natop,×,1 .U = Natop - Natop,×,1 .monoidal = +-monoidal Natop Natop-Cocartesian + Natop,×,1 .monoidal = +-monoidal Natop-Cocartesian Natop,×,1 .symmetric = +-symmetric Natop Natop-Cocartesian open Symmetric public diff --git a/Data/Matrix/SemiadditiveDagger.agda b/Data/Matrix/SemiadditiveDagger.agda index ebc6592..1415c7e 100644 --- a/Data/Matrix/SemiadditiveDagger.agda +++ b/Data/Matrix/SemiadditiveDagger.agda @@ -286,15 +286,15 @@ coproduct {A} {B} = record opaque unfolding _≋_ - !-unique : (E : Matrix 0 B) → []ᵥ ≋ E - !-unique E = ≋.reflexive (≡.sym ([]ᵥ-! E)) + ¡-unique : (E : Matrix 0 B) → []ᵥ ≋ E + ¡-unique E = ≋.reflexive (≡.sym ([]ᵥ-! E)) initial : Initial Mat initial = record { ⊥ = 0 ; ⊥-is-initial = record - { ! = []ᵥ - ; !-unique = !-unique + { ¡ = []ᵥ + ; ¡-unique = ¡-unique } } diff --git a/Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda b/Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda index 346999b..537ac38 100644 --- a/Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda +++ b/Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda @@ -26,16 +26,8 @@ open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategor open import Category.Cartesian.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat-CC) open import Functor.Instance.Underlying.SymmetricMonoidal.FinitelyCocomplete {o} {ℓ} {e} using () renaming (Underlying to U) -module CartesianCategory′ {o ℓ e : Level} (C : CartesianCategory o ℓ e) where - module CC = CartesianCategory C - open import Categories.Object.Terminal using (Terminal) - open Terminal CC.terminal public - open import Categories.Category.BinaryProducts using (BinaryProducts) - open BinaryProducts CC.products public - open CC public - -module FC = CartesianCategory′ FinitelyCocompletes-CC -module SMC = CartesianCategory′ SymMonCat-CC +module FC = CartesianCategory FinitelyCocompletes-CC +module SMC = CartesianCategory SymMonCat-CC module U = Functor U F-resp-⊤ : IsTerminal SMC.U (U.₀ FC.⊤) diff --git a/Functor/Exact/Instance/Swap.agda b/Functor/Exact/Instance/Swap.agda index 99a27c5..98ca0f4 100644 --- a/Functor/Exact/Instance/Swap.agda +++ b/Functor/Exact/Instance/Swap.agda @@ -6,28 +6,26 @@ open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategor module Functor.Exact.Instance.Swap {o ℓ e : Level} (𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e) where open import Categories.Category using (_[_,_]) -open import Categories.Category.BinaryProducts using (BinaryProducts) open import Categories.Category.Product using (Product) renaming (Swap to Swap′) open import Categories.Category.Cartesian using (Cartesian) open import Categories.Diagram.Coequalizer using (IsCoequalizer) open import Categories.Object.Initial using (IsInitial) open import Categories.Object.Coproduct using (IsCoproduct) -open import Data.Product.Base using (_,_; proj₁; proj₂; swap) +open import Data.Product using (_,_; proj₁; proj₂; swap) open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes-Cartesian) open import Functor.Exact using (RightExactFunctor) module FCC = Cartesian FinitelyCocompletes-Cartesian -open BinaryProducts (FCC.products) using (_×_) -- ; π₁; π₂; _⁂_; assocˡ) - +open FCC using (_×_) module 𝒞 = FinitelyCocompleteCategory 𝒞 module 𝒟 = FinitelyCocompleteCategory 𝒟 swap-resp-⊥ : {A : 𝒞.Obj} {B : 𝒟.Obj} → IsInitial (Product 𝒞.U 𝒟.U) (A , B) → IsInitial (Product 𝒟.U 𝒞.U) (B , A) swap-resp-⊥ {A} {B} isInitial = record - { ! = swap ! - ; !-unique = λ { (f , g) → swap (!-unique (g , f)) } + { ¡ = swap ¡ + ; ¡-unique = λ { (f , g) → swap (¡-unique (g , f)) } } where open IsInitial isInitial diff --git a/Functor/Instance/CMonoidalize.agda b/Functor/Instance/CMonoidalize.agda index ad9b266..eef2bc8 100644 --- a/Functor/Instance/CMonoidalize.agda +++ b/Functor/Instance/CMonoidalize.agda @@ -12,7 +12,7 @@ module Functor.Instance.CMonoidalize (D : SymmetricMonoidalCategory o′ ℓ′ e′) where -open import Categories.Category.Cocartesian using (module CocartesianSymmetricMonoidal) +open import Categories.Category.Cocartesian.SymmetricMonoidal using (module CocartesianSymmetricMonoidal) open import Categories.Functor using (Functor) open import Category.Construction.CMonoids using (CMonoids) open import Categories.Category.Construction.Functors using (Functors) diff --git a/Functor/Instance/Cospan/Stack.agda b/Functor/Instance/Cospan/Stack.agda index b72219b..568b99d 100644 --- a/Functor/Instance/Cospan/Stack.agda +++ b/Functor/Instance/Cospan/Stack.agda @@ -43,8 +43,7 @@ id⊗id≈id {A} {B} = record where open Morphism U using (module ≅) open HomReasoning - open 𝒞 using (+-η; []-cong₂) - open coproduct {A} {B} using (i₁; i₂) + open 𝒞 using (i₁; i₂; +-η; []-cong₂) from∘f≈f : id ∘ [ i₁ ∘ id , i₂ ∘ id ] 𝒞.≈ id from∘f≈f = begin id ∘ [ i₁ ∘ id , i₂ ∘ id ] ≈⟨ identityˡ ⟩ diff --git a/Functor/Instance/Decorate.agda b/Functor/Instance/Decorate.agda index fedddba..8d5aefb 100644 --- a/Functor/Instance/Decorate.agda +++ b/Functor/Instance/Decorate.agda @@ -23,7 +23,8 @@ import Categories.Morphism.Reasoning as ⇒-Reasoning import Category.Diagram.Cospan 𝒞 as Cospan open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_]) -open import Categories.Category.Cocartesian using (module CocartesianMonoidal) +open import Categories.Category.Monoidal using (module Monoidal) +open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal) open import Categories.Category.Monoidal.Properties using (coherence-inv₃) open import Categories.Category.Monoidal.Utilities using (module Shorthands) open import Categories.Functor.Core using (Functor) @@ -39,7 +40,7 @@ module 𝒟 = SymmetricMonoidalCategory 𝒟 module F = SymmetricMonoidalFunctor F module Cospans = Category Cospans module DecoratedCospans = Category DecoratedCospans -module mc𝒞 = CocartesianMonoidal 𝒞.U 𝒞.cocartesian +module mc𝒞 = CocartesianMonoidal 𝒞.cocartesian -- For every cospan there exists a free decorated cospan -- i.e. the original cospan with the discrete decoration @@ -90,7 +91,7 @@ homomorphism {g} {f} = record open DiagramPushout 𝒞.U using (Pushout) open Pushout (pushout f₂ g₁) using (i₁; i₂) - open mc𝒞 using (unitorˡ) + open Monoidal mc𝒞.+-monoidal using (unitorˡ) open unitorˡ using () renaming (to to λ⇐′) same-deco : F₁ 𝒞.id ∘ F₁ ¡ ∘ F.ε ≈ F₁ [ i₁ , i₂ ]′ ∘ φ (N , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ @@ -147,7 +148,7 @@ Decorate-resp-⊗ {f} {g} = record open F.⊗-homo using () renaming (η to φ; commute to φ-commute) open F using (F₁; ε) open Shorthands monoidal - open mc𝒞 using (unitorˡ) + open Monoidal mc𝒞.+-monoidal using (unitorˡ) open unitorˡ using () renaming (to to λ⇐′) same-deco : F₁ 𝒞.id ∘ F₁ ¡ ∘ ε ≈ φ (N , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ diff --git a/Functor/Instance/DecoratedCospan/Embed.agda b/Functor/Instance/DecoratedCospan/Embed.agda index 77b16fa..15f3b57 100644 --- a/Functor/Instance/DecoratedCospan/Embed.agda +++ b/Functor/Instance/DecoratedCospan/Embed.agda @@ -32,7 +32,8 @@ import Categories.Diagram.Pushout as DiagramPushout import Categories.Diagram.Pushout.Properties as PushoutProperties import Categories.Morphism as Morphism -open import Categories.Category.Cocartesian using (module CocartesianMonoidal) +open import Categories.Category.Monoidal using (module Monoidal) +open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal) open import Categories.Category.Monoidal.Utilities using (module Shorthands) open import Categories.Functor using (Functor; _∘F_) open import Data.Product using (_,_) @@ -44,7 +45,7 @@ module 𝒟 = SymmetricMonoidalCategory 𝒟 module F = SymmetricMonoidalFunctor F module Cospans = Category Cospans module DecoratedCospans = Category DecoratedCospans -module mc𝒞 = CocartesianMonoidal 𝒞.U 𝒞.cocartesian +module mc𝒞 = CocartesianMonoidal 𝒞.cocartesian open import Functor.Instance.Decorate 𝒞 F using (Decorate; Decorate-resp-⊗) @@ -74,7 +75,8 @@ module _ where module Codiagonal where - open mc𝒞 using (unitorˡ; unitorʳ; +-monoidal) public + open mc𝒞 using (+-monoidal) public + open Monoidal +-monoidal using (unitorˡ; unitorʳ) public open unitorˡ using () renaming (to to λ⇐′) public open unitorʳ using () renaming (to to ρ⇐′) public open 𝒞 using (U; _+_; []-cong₂; []∘+₁; ∘-distribˡ-[]; inject₁; inject₂; ¡) @@ -122,7 +124,8 @@ module _ where open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ ) open 𝒞 using (U) open Category U - open mc𝒞 using (unitorˡ; unitorˡ-commute-to; +-monoidal) public + open mc𝒞 using (+-monoidal) public + open Monoidal +-monoidal using (unitorˡ; unitorˡ-commute-to) public open unitorˡ using () renaming (to to λ⇐′) public open ⊗-Reasoning +-monoidal open ⇒-Reasoning 𝒞.U @@ -198,7 +201,8 @@ module _ where open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ ) open 𝒞 using (U) open Category U - open mc𝒞 using (unitorʳ; unitorˡ; unitorˡ-commute-to; +-monoidal) public + open mc𝒞 using (+-monoidal) public + open Monoidal +-monoidal using (unitorʳ; unitorˡ; unitorˡ-commute-to) public open unitorˡ using () renaming (to to λ⇐′) public open unitorʳ using () renaming (to to ρ⇐′) public open ⊗-Reasoning +-monoidal diff --git a/Functor/Instance/DecoratedCospan/Stack.agda b/Functor/Instance/DecoratedCospan/Stack.agda index 381ee06..e3eca81 100644 --- a/Functor/Instance/DecoratedCospan/Stack.agda +++ b/Functor/Instance/DecoratedCospan/Stack.agda @@ -23,16 +23,17 @@ import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning import Functor.Instance.Cospan.Stack 𝒞 as Stack open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_]) -open import Categories.Category.BinaryProducts using (BinaryProducts) -open import Categories.Category.Monoidal.Utilities using (module Shorthands) -open import Categories.Category.Monoidal.Properties using (coherence-inv₃) +open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal) +open import Categories.Category.Cocartesian.SymmetricMonoidal using (module CocartesianSymmetricMonoidal) +open import Categories.Category.Monoidal using (module Monoidal) open import Categories.Category.Monoidal.Braided.Properties using (braiding-coherence-inv) +open import Categories.Category.Monoidal.Properties using (coherence-inv₃) +open import Categories.Category.Monoidal.Utilities using (module Shorthands) open import Categories.Functor using (Functor) open import Categories.Functor.Bifunctor using (Bifunctor) open import Categories.Functor.Properties using ([_]-resp-≅) -open import Categories.Category.Cocartesian using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal) -open import Categories.Object.Initial using (Initial) open import Categories.Object.Duality using (Coproduct⇒coProduct) +open import Categories.Object.Initial using (Initial) open import Category.Instance.DecoratedCospans 𝒞 F using () renaming (DecoratedCospans to Cospans; _≈_ to _≈_′) import Category.Diagram.Cospan 𝒞 as Cospan @@ -47,7 +48,7 @@ module Cospans = Category Cospans open 𝒞 using (Obj; _+_; cocartesian) -module mc𝒞 = CocartesianMonoidal 𝒞.U cocartesian +module mc𝒞 = CocartesianMonoidal cocartesian module smc𝒞 = CocartesianSymmetricMonoidal 𝒞.U cocartesian open DiagramPushout 𝒞.U using (Pushout) @@ -73,9 +74,9 @@ id⊗id≈id {A} {B} = record ; same-deco = F.identity ⟩∘⟨refl ○ identityˡ ○ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩∘⟨refl - ○ extendʳ (extendʳ (⊗-homo.commute (! , !))) + ○ extendʳ (extendʳ (⊗-homo.commute (¡ , ¡))) ○ refl⟩∘⟨ pullʳ (pushˡ serialize₂₁ ○ refl⟩∘⟨ sym unitorʳ-commute-to) - ○ pushˡ (F-resp-≈ !+!≈! ○ homomorphism) + ○ pushˡ (F-resp-≈ ¡+¡≈¡ ○ homomorphism) ○ refl⟩∘⟨ (refl⟩∘⟨ sym-assoc ○ pullˡ unitaryʳ ○ cancelˡ unitorʳ.isoʳ) } where @@ -87,12 +88,12 @@ id⊗id≈id {A} {B} = record open ⊗-Reasoning monoidal open F using (module ⊗-homo; F-resp-≈; homomorphism; unitaryʳ) open 𝒞 using (initial) - open Initial initial using (!; !-unique₂) + open Initial initial using (¡; ¡-unique₂) open Morphism using (_≅_; module ≅) open mc𝒞 using (A+⊥≅A) module A+⊥≅A = _≅_ A+⊥≅A - !+!≈! : 𝒞.U [ (! {A} +₁ ! {B}) ≈ ! {A + B} 𝒞.∘ A+⊥≅A.from ] - !+!≈! = 𝒞.Equiv.sym (flip-iso′ (≅.sym 𝒞.U A+⊥≅A) (¡-unique ((! +₁ !) 𝒞.∘ A+⊥≅A.to))) + ¡+¡≈¡ : 𝒞.U [ (¡ {A} +₁ ¡ {B}) ≈ ¡ {A + B} 𝒞.∘ A+⊥≅A.from ] + ¡+¡≈¡ = 𝒞.Equiv.sym (flip-iso′ (≅.sym 𝒞.U A+⊥≅A) (¡-unique ((¡ +₁ ¡) 𝒞.∘ A+⊥≅A.to))) homomorphism : (A⇒B : Cospans [ A , B ]) @@ -148,12 +149,12 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record open Shorthands mc𝒞.+-monoidal open ⊗-Reasoning mc𝒞.+-monoidal open ⇒-Reasoning U - open mc𝒞 using (assoc-commute-from; assoc-commute-to; module ⊗; associator) + open Monoidal mc𝒞.+-monoidal using (assoc-commute-from; assoc-commute-to; module ⊗; associator) open smc𝒞 using () renaming (module braiding to σ) module Codiagonal where - open 𝒞 using (coproduct; +-unique; []-cong₂; []∘+₁; ∘-distribˡ-[]) + open 𝒞 using (coproduct; +-unique; []-cong₂; []∘+₁; ∘-distribˡ-[]; []∘+-assocʳ) μ : {X : Obj} → X + X ⇒ X μ = [ id , id ]′ @@ -163,16 +164,10 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record μ∘σ : {X : Obj} → μ ∘ +-swap ≈ μ {X} μ∘σ = sym (+-unique (pullʳ inject₁ ○ inject₂) (pullʳ inject₂ ○ inject₁) ) - op-binaryProducts : BinaryProducts op - op-binaryProducts = record { product = Coproduct⇒coProduct U coproduct } - - module op-binaryProducts = BinaryProducts op-binaryProducts - open op-binaryProducts using () renaming (assocʳ∘⟨⟩ to []∘assocˡ) - μ-assoc : {X : Obj} → μ {X} ∘ μ +₁ (id {X}) ≈ μ ∘ (id {X}) +₁ μ ∘ α⇒ μ-assoc = begin μ ∘ μ +₁ id ≈⟨ μ∘+ ⟨ - [ [ id , id ]′ , id ]′ ≈⟨ []∘assocˡ ⟨ + [ [ id , id ]′ , id ]′ ≈⟨ []∘+-assocʳ ⟨ [ id , [ id , id ]′ ]′ ∘ α⇒ ≈⟨ pushˡ μ∘+ ⟩ μ ∘ id +₁ μ ∘ α⇒ ∎ diff --git a/Functor/Instance/Monoidalize.agda b/Functor/Instance/Monoidalize.agda index b856f82..b52c5fb 100644 --- a/Functor/Instance/Monoidalize.agda +++ b/Functor/Instance/Monoidalize.agda @@ -12,7 +12,7 @@ module Functor.Instance.Monoidalize (D : MonoidalCategory o′ ℓ′ e′) where -open import Categories.Category.Cocartesian using (module CocartesianMonoidal) +open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal) open import Categories.Functor using (Functor) open import Categories.Functor.Monoidal using (MonoidalFunctor) @@ -25,7 +25,7 @@ open import NaturalTransformation.Monoidal.Construction.MonoidValued cocartesian C-MC : MonoidalCategory o ℓ e C-MC = record { monoidal = +-monoidal } where - open CocartesianMonoidal C cocartesian + open CocartesianMonoidal cocartesian module C = MonoidalCategory C-MC module D = MonoidalCategory D diff --git a/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda b/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda index 8fabddd..456fe87 100644 --- a/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda +++ b/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda @@ -74,17 +74,17 @@ F₁ {A} {B} F = record open B.HomReasoning open B.Equiv open B using (_∘_; _≈_) - open B′ using (_+₁_; []-congˡ; []-congʳ; []-cong₂) + open B′ using (_+₁_; []-congˡ; []-congʳ; []-cong₂; ∘-distribˡ-[]) open A′ using (_+_; i₁; i₂) ⊗-homo : NaturalTransformation (B.⊗ ∘F (F.F ⁂ F.F)) (F.F ∘F A.⊗) ⊗-homo = ntHelper record { η = λ { (X , Y) → +-iso.from {X} {Y} } ; commute = λ { {X , Y} {X′ , Y′} (f , g) → - B′.coproduct.∘-distribˡ-[] - ○ B′.coproduct.[]-cong₂ - (pullˡ B′.coproduct.inject₁ ○ [ F.F ]-resp-square (A.Equiv.sym A′.coproduct.inject₁)) - (pullˡ B′.coproduct.inject₂ ○ [ F.F ]-resp-square (A.Equiv.sym A′.coproduct.inject₂)) - ○ sym B′.coproduct.∘-distribˡ-[] } + ∘-distribˡ-[] + ○ []-cong₂ + (pullˡ B′.inject₁ ○ [ F.F ]-resp-square (A.Equiv.sym A′.inject₁)) + (pullˡ B′.inject₂ ○ [ F.F ]-resp-square (A.Equiv.sym A′.inject₂)) + ○ sym ∘-distribˡ-[] } } assoc : {X Y Z : A.Obj} @@ -96,59 +96,59 @@ F₁ {A} {B} F = record ∘ B′.+-assocˡ assoc {X} {Y} {Z} = begin F.₁ A′.+-assocˡ ∘ +-iso.from ∘ (+-iso.from +₁ B.id) ≈⟨ refl⟩∘⟨ B′.[]∘+₁ ⟩ - F.₁ A′.+-assocˡ ∘ B′.[ F.₁ i₁ ∘ +-iso.from , F.₁ i₂ ∘ B.id ] ≈⟨ refl⟩∘⟨ []-congʳ B′.coproduct.∘-distribˡ-[] ⟩ - F.₁ A′.+-assocˡ ∘ B′.[ B′.[ F.₁ i₁ ∘ F.₁ i₁ , F.₁ i₁ ∘ F.₁ i₂ ] , F.₁ i₂ ∘ B.id ] ≈⟨ B′.coproduct.∘-distribˡ-[] ⟩ - B′.[ F.₁ A′.+-assocˡ ∘ B′.[ F.₁ i₁ ∘ F.₁ i₁ , F.₁ i₁ ∘ F.₁ i₂ ] , _ ] ≈⟨ []-congʳ B′.coproduct.∘-distribˡ-[] ⟩ - B′.[ B′.[ F.₁ A′.+-assocˡ ∘ F.₁ i₁ ∘ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ _ ] , _ ] ≈⟨ []-congʳ ([]-congʳ (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₁))) ⟩ - B′.[ B′.[ F.₁ A′.[ i₁ , i₂ A′.∘ i₁ ] ∘ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ _ ] , _ ] ≈⟨ []-congʳ ([]-congʳ ([ F.F ]-resp-∘ A′.coproduct.inject₁)) ⟩ - B′.[ B′.[ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ F.₁ i₁ ∘ F.₁ i₂ ] , _ ] ≈⟨ []-congʳ ([]-congˡ (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₁))) ⟩ - B′.[ B′.[ F.₁ i₁ , F.₁ A′.[ i₁ , i₂ A′.∘ i₁ ] ∘ F.₁ i₂ ] , _ ] ≈⟨ []-congʳ ([]-congˡ ([ F.F ]-resp-∘ A′.coproduct.inject₂)) ⟩ - B′.[ B′.[ F.₁ i₁ , F.₁ (i₂ A′.∘ i₁) ] , F.₁ A′.+-assocˡ ∘ F.₁ i₂ ∘ B.id ] ≈⟨ []-congˡ (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₂)) ⟩ + F.₁ A′.+-assocˡ ∘ B′.[ F.₁ i₁ ∘ +-iso.from , F.₁ i₂ ∘ B.id ] ≈⟨ refl⟩∘⟨ []-congʳ ∘-distribˡ-[] ⟩ + F.₁ A′.+-assocˡ ∘ B′.[ B′.[ F.₁ i₁ ∘ F.₁ i₁ , F.₁ i₁ ∘ F.₁ i₂ ] , F.₁ i₂ ∘ B.id ] ≈⟨ ∘-distribˡ-[] ⟩ + B′.[ F.₁ A′.+-assocˡ ∘ B′.[ F.₁ i₁ ∘ F.₁ i₁ , F.₁ i₁ ∘ F.₁ i₂ ] , _ ] ≈⟨ []-congʳ ∘-distribˡ-[] ⟩ + B′.[ B′.[ F.₁ A′.+-assocˡ ∘ F.₁ i₁ ∘ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ _ ] , _ ] ≈⟨ []-congʳ ([]-congʳ (pullˡ ([ F.F ]-resp-∘ A′.inject₁))) ⟩ + B′.[ B′.[ F.₁ A′.[ i₁ , i₂ A′.∘ i₁ ] ∘ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ _ ] , _ ] ≈⟨ []-congʳ ([]-congʳ ([ F.F ]-resp-∘ A′.inject₁)) ⟩ + B′.[ B′.[ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ F.₁ i₁ ∘ F.₁ i₂ ] , _ ] ≈⟨ []-congʳ ([]-congˡ (pullˡ ([ F.F ]-resp-∘ A′.inject₁))) ⟩ + B′.[ B′.[ F.₁ i₁ , F.₁ A′.[ i₁ , i₂ A′.∘ i₁ ] ∘ F.₁ i₂ ] , _ ] ≈⟨ []-congʳ ([]-congˡ ([ F.F ]-resp-∘ A′.inject₂)) ⟩ + B′.[ B′.[ F.₁ i₁ , F.₁ (i₂ A′.∘ i₁) ] , F.₁ A′.+-assocˡ ∘ F.₁ i₂ ∘ B.id ] ≈⟨ []-congˡ (pullˡ ([ F.F ]-resp-∘ A′.inject₂)) ⟩ B′.[ B′.[ F.₁ i₁ , F.₁ (i₂ A′.∘ i₁) ] , F.₁ (i₂ A′.∘ i₂) ∘ B.id ] ≈⟨ []-cong₂ ([]-congˡ F.homomorphism) (B.identityʳ ○ F.homomorphism) ⟩ - B′.[ B′.[ F.₁ i₁ , F.₁ i₂ B′.∘ F.₁ i₁ ] , F.₁ i₂ ∘ F.₁ i₂ ] ≈⟨ []-congʳ ([]-congˡ B′.coproduct.inject₁) ⟨ - B′.[ B′.[ F.₁ i₁ , B′.[ F.₁ i₂ B′.∘ F.₁ i₁  , _ ] ∘ B′.i₁ ] , _ ] ≈⟨ []-congʳ ([]-cong₂ (sym B′.coproduct.inject₁) (pushˡ (sym B′.coproduct.inject₂))) ⟩ - B′.[ B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.i₁ , B′.[ F.₁ i₁ , _ ] ∘ B′.i₂ ∘ B′.i₁ ] , _ ] ≈⟨ []-congʳ B′.coproduct.∘-distribˡ-[] ⟨ - B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ B′.i₁ , B′.i₂ ∘ B′.i₁ ] , F.₁ i₂ ∘ F.₁ i₂ ] ≈⟨ []-congˡ B′.coproduct.inject₂ ⟨ - B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ _ , _ ] , B′.[ _ , F.₁ i₂ ∘ F.₁ i₂ ] ∘ B′.i₂ ] ≈⟨ []-congˡ (pushˡ (sym B′.coproduct.inject₂)) ⟩ - B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ _ , _ ] , B′.[ F.₁ i₁ , _ ] ∘ B′.i₂ ∘ B′.i₂ ] ≈⟨ B′.coproduct.∘-distribˡ-[] ⟨ - B′.[ F.₁ i₁ , B′.[ F.₁ i₂ ∘ F.₁ i₁ , F.₁ i₂ ∘ F.₁ i₂ ] ] ∘ B′.+-assocˡ ≈⟨ []-cong₂ B.identityʳ (B′.coproduct.∘-distribˡ-[]) ⟩∘⟨refl ⟨ + B′.[ B′.[ F.₁ i₁ , F.₁ i₂ B′.∘ F.₁ i₁ ] , F.₁ i₂ ∘ F.₁ i₂ ] ≈⟨ []-congʳ ([]-congˡ B′.inject₁) ⟨ + B′.[ B′.[ F.₁ i₁ , B′.[ F.₁ i₂ B′.∘ F.₁ i₁  , _ ] ∘ B′.i₁ ] , _ ] ≈⟨ []-congʳ ([]-cong₂ (sym B′.inject₁) (pushˡ (sym B′.inject₂))) ⟩ + B′.[ B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.i₁ , B′.[ F.₁ i₁ , _ ] ∘ B′.i₂ ∘ B′.i₁ ] , _ ] ≈⟨ []-congʳ ∘-distribˡ-[] ⟨ + B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ B′.i₁ , B′.i₂ ∘ B′.i₁ ] , F.₁ i₂ ∘ F.₁ i₂ ] ≈⟨ []-congˡ B′.inject₂ ⟨ + B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ _ , _ ] , B′.[ _ , F.₁ i₂ ∘ F.₁ i₂ ] ∘ B′.i₂ ] ≈⟨ []-congˡ (pushˡ (sym B′.inject₂)) ⟩ + B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ _ , _ ] , B′.[ F.₁ i₁ , _ ] ∘ B′.i₂ ∘ B′.i₂ ] ≈⟨ ∘-distribˡ-[] ⟨ + B′.[ F.₁ i₁ , B′.[ F.₁ i₂ ∘ F.₁ i₁ , F.₁ i₂ ∘ F.₁ i₂ ] ] ∘ B′.+-assocˡ ≈⟨ []-cong₂ B.identityʳ (∘-distribˡ-[]) ⟩∘⟨refl ⟨ B′.[ F.₁ i₁ B′.∘ B′.id , F.₁ i₂ ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ] ∘ B′.+-assocˡ ≈⟨ pushˡ (sym B′.[]∘+₁) ⟩ +-iso.from ∘ (B.id +₁ +-iso.from) ∘ B′.+-assocˡ ∎ unitaryˡ : {X : A.Obj} - → F.₁ A′.[ A′.initial.! , A.id {X} ] + → F.₁ A′.[ A′.¡ , A.id {X} ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] - ∘ B′.[ B′.i₁ ∘ B′.initial.! , B′.i₂ ∘ B.id ] - ≈ B′.[ B′.initial.! , B.id ] + ∘ B′.[ B′.i₁ ∘ B′.¡ , B′.i₂ ∘ B.id ] + ≈ B′.[ B′.¡ , B.id ] unitaryˡ {X} = begin - F.₁ A′.[ A′.initial.! , A.id ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.[ _ , B′.i₂ ∘ B.id ] ≈⟨ refl⟩∘⟨ B′.coproduct.∘-distribˡ-[] ⟩ - _ ∘ B′.[ _ ∘ B′.i₁ ∘ B′.initial.! , B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₂ ∘ B.id ] ≈⟨ refl⟩∘⟨ []-cong₂ (sym (B′.¡-unique _)) (pullˡ B′.coproduct.inject₂) ⟩ - F.₁ A′.[ A′.initial.! , A.id ] ∘ B′.[ B′.initial.! , F.₁ i₂ ∘ B.id ] ≈⟨ B′.coproduct.∘-distribˡ-[] ⟩ - B′.[ _ ∘ B′.initial.! , F.₁ A′.[ A′.initial.! , A.id ] ∘ F.₁ i₂ ∘ B.id ] ≈⟨ []-cong₂ (sym (B′.¡-unique _)) (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₂)) ⟩ - B′.[ B′.initial.! , F.₁ A.id ∘ B.id ] ≈⟨ []-congˡ (elimˡ F.identity) ⟩ - B′.[ B′.initial.! , B.id ] ∎ + F.₁ A′.[ A′.¡ , A.id ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.[ _ , B′.i₂ ∘ B.id ] ≈⟨ refl⟩∘⟨ ∘-distribˡ-[] ⟩ + _ ∘ B′.[ _ ∘ B′.i₁ ∘ B′.¡ , B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₂ ∘ B.id ] ≈⟨ refl⟩∘⟨ []-cong₂ (sym (B′.¡-unique _)) (pullˡ B′.inject₂) ⟩ + F.₁ A′.[ A′.¡ , A.id ] ∘ B′.[ B′.¡ , F.₁ i₂ ∘ B.id ] ≈⟨ ∘-distribˡ-[] ⟩ + B′.[ _ ∘ B′.¡ , F.₁ A′.[ A′.¡ , A.id ] ∘ F.₁ i₂ ∘ B.id ] ≈⟨ []-cong₂ (sym (B′.¡-unique _)) (pullˡ ([ F.F ]-resp-∘ A′.inject₂)) ⟩ + B′.[ B′.¡ , F.₁ A.id ∘ B.id ] ≈⟨ []-congˡ (elimˡ F.identity) ⟩ + B′.[ B′.¡ , B.id ] ∎ unitaryʳ : {X : A.Obj} - → F.₁ A′.[ A′.id {X} , A′.initial.! ] + → F.₁ A′.[ A′.id {X} , A′.¡ ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] - ∘ B′.[ B′.i₁ ∘ B.id , B′.i₂ ∘ B′.initial.! ] - ≈ B′.[ B.id , B′.initial.! ] + ∘ B′.[ B′.i₁ ∘ B.id , B′.i₂ ∘ B′.¡ ] + ≈ B′.[ B.id , B′.¡ ] unitaryʳ {X} = begin - F.₁ A′.[ A.id , A′.initial.! ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.[ B′.i₁ ∘ B.id , _ ] ≈⟨ refl⟩∘⟨ B′.coproduct.∘-distribˡ-[] ⟩ - _ ∘ B′.[ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₁ ∘ B.id , _ ∘ B′.i₂ ∘ B′.initial.! ] ≈⟨ refl⟩∘⟨ []-cong₂ (pullˡ B′.coproduct.inject₁) (sym (B′.¡-unique _)) ⟩ - F.₁ A′.[ A.id , A′.initial.! ] ∘ B′.[ F.₁ i₁ ∘ B.id , B′.initial.! ] ≈⟨ B′.coproduct.∘-distribˡ-[] ⟩ - B′.[ F.₁ A′.[ A.id , A′.initial.! ] ∘ F.₁ i₁ ∘ B.id , _ ∘ B′.initial.! ] ≈⟨ []-cong₂ (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₁)) (sym (B′.¡-unique _)) ⟩ - B′.[ F.₁ A.id ∘ B.id , B′.initial.! ] ≈⟨ []-congʳ (elimˡ F.identity) ⟩ - B′.[ B.id , B′.initial.! ] ∎ + F.₁ A′.[ A.id , A′.¡ ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.[ B′.i₁ ∘ B.id , _ ] ≈⟨ refl⟩∘⟨ ∘-distribˡ-[] ⟩ + _ ∘ B′.[ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₁ ∘ B.id , _ ∘ B′.i₂ ∘ B′.¡ ] ≈⟨ refl⟩∘⟨ []-cong₂ (pullˡ B′.inject₁) (sym (B′.¡-unique _)) ⟩ + F.₁ A′.[ A.id , A′.¡ ] ∘ B′.[ F.₁ i₁ ∘ B.id , B′.¡ ] ≈⟨ ∘-distribˡ-[] ⟩ + B′.[ F.₁ A′.[ A.id , A′.¡ ] ∘ F.₁ i₁ ∘ B.id , _ ∘ B′.¡ ] ≈⟨ []-cong₂ (pullˡ ([ F.F ]-resp-∘ A′.inject₁)) (sym (B′.¡-unique _)) ⟩ + B′.[ F.₁ A.id ∘ B.id , B′.¡ ] ≈⟨ []-congʳ (elimˡ F.identity) ⟩ + B′.[ B.id , B′.¡ ] ∎ braiding-compat : {X Y : A.Obj} → F.₁ A′.[ i₂ {X} {Y} , i₁ ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ≈ B′.[ F.F₁ i₁ , F.F₁ i₂ ] ∘ B′.[ B′.i₂ , B′.i₁ ] braiding-compat = begin - F.₁ A′.[ i₂ , i₁ ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ≈⟨ B′.coproduct.∘-distribˡ-[] ⟩ - B′.[ F.₁ A′.[ i₂ , i₁ ] ∘ F.₁ i₁ , F.₁ A′.[ i₂ , i₁ ] ∘ F.₁ i₂ ] ≈⟨ []-cong₂ ([ F.F ]-resp-∘ A′.coproduct.inject₁) ([ F.F ]-resp-∘ A′.coproduct.inject₂) ⟩ - B′.[ F.₁ i₂ , F.₁ i₁ ] ≈⟨ []-cong₂ B′.coproduct.inject₂ B′.coproduct.inject₁ ⟨ - B′.[ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₂ , B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₁ ] ≈⟨ B′.coproduct.∘-distribˡ-[] ⟨ + F.₁ A′.[ i₂ , i₁ ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ≈⟨ ∘-distribˡ-[] ⟩ + B′.[ F.₁ A′.[ i₂ , i₁ ] ∘ F.₁ i₁ , F.₁ A′.[ i₂ , i₁ ] ∘ F.₁ i₂ ] ≈⟨ []-cong₂ ([ F.F ]-resp-∘ A′.inject₁) ([ F.F ]-resp-∘ A′.inject₂) ⟩ + B′.[ F.₁ i₂ , F.₁ i₁ ] ≈⟨ []-cong₂ B′.inject₂ B′.inject₁ ⟨ + B′.[ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₂ , B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₁ ] ≈⟨ ∘-distribˡ-[] ⟨ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.[ B′.i₂ , B′.i₁ ] ∎ open B-proofs @@ -179,8 +179,8 @@ homomorphism {A} {B} {C} {F} {G} = record identityˡ ○ sym ([]-cong₂ - ([ G.F ]-resp-∘ B.coproducts.inject₁) - ([ G.F ]-resp-∘ B.coproducts.inject₂)) + ([ G.F ]-resp-∘ B.inject₁) + ([ G.F ]-resp-∘ B.inject₂)) ○ sym ∘-distribˡ-[] ○ pushʳ (introʳ C.⊗.identity) } diff --git a/Functor/Monoidal/Construction/CMonoidValued.agda b/Functor/Monoidal/Construction/CMonoidValued.agda index 2ac8be2..eb5c965 100644 --- a/Functor/Monoidal/Construction/CMonoidValued.agda +++ b/Functor/Monoidal/Construction/CMonoidValued.agda @@ -24,7 +24,7 @@ import Categories.Morphism.Reasoning as ⇒-Reasoning import Object.Monoid.Commutative as CommutativeMonoidObject import Functor.Monoidal.Construction.MonoidValued as MonoidValued -open import Categories.Category.Cocartesian using (module CocartesianSymmetricMonoidal) +open import Categories.Category.Cocartesian.SymmetricMonoidal using (module CocartesianSymmetricMonoidal) open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory) open import Categories.Category.Construction.Monoids using (Monoids) open import Categories.Category.Monoidal.Symmetric.Properties using (module Shorthands) diff --git a/Functor/Monoidal/Construction/MonoidValued.agda b/Functor/Monoidal/Construction/MonoidValued.agda index 937714d..f8cd11f 100644 --- a/Functor/Monoidal/Construction/MonoidValued.agda +++ b/Functor/Monoidal/Construction/MonoidValued.agda @@ -26,7 +26,7 @@ import Categories.Morphism.Reasoning as ⇒-Reasoning import Categories.Object.Monoid as MonoidObject open import Categories.Category using (module Definitions) -open import Categories.Category.Cocartesian using (module CocartesianMonoidal) +open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal) open import Categories.Category.Product using (_⁂_) open import Categories.Functor.Monoidal using (MonoidalFunctor; IsMonoidalFunctor) open import Categories.Functor.Properties using ([_]-resp-square; [_]-resp-∘) @@ -41,7 +41,7 @@ private G = Forget ∙ M module 𝒞 = CocartesianCategory (record { cocartesian = 𝒞-+ }) - module 𝒞-M = CocartesianMonoidal 𝒞 𝒞-+ + module 𝒞-M = CocartesianMonoidal 𝒞-+ 𝒞-MC : MonoidalCategory o ℓ e 𝒞-MC = record { monoidal = 𝒞-M.+-monoidal } -- cgit v1.2.3