aboutsummaryrefslogtreecommitdiff
path: root/Category
diff options
context:
space:
mode:
Diffstat (limited to 'Category')
-rw-r--r--Category/Cartesian/Instance/FinitelyCocompletes.agda17
-rw-r--r--Category/Cocomplete/Finitely/Product.agda20
-rw-r--r--Category/Cocomplete/Finitely/SymmetricMonoidal.agda4
-rw-r--r--Category/Dagger/Semiadditive.agda34
-rw-r--r--Category/Instance/DecoratedCospans.agda36
-rw-r--r--Category/Instance/FinitelyCocompletes.agda24
-rw-r--r--Category/Instance/One/Properties.agda2
-rw-r--r--Category/Instance/Setoids/SymmetricMonoidal.agda4
-rw-r--r--Category/Monoidal/Instance/Cospans.agda9
-rw-r--r--Category/Monoidal/Instance/DecoratedCospans/Products.agda10
-rw-r--r--Category/Monoidal/Instance/Nat.agda12
11 files changed, 73 insertions, 99 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
generated by cgit v1.2.3 (git 2.39.1) at 2026-07-21 20:43:24 +0000