diff options
Diffstat (limited to 'Category/Instance')
| -rw-r--r-- | Category/Instance/DecoratedCospans.agda | 36 | ||||
| -rw-r--r-- | Category/Instance/FinitelyCocompletes.agda | 24 | ||||
| -rw-r--r-- | Category/Instance/One/Properties.agda | 2 | ||||
| -rw-r--r-- | Category/Instance/Setoids/SymmetricMonoidal.agda | 4 |
4 files changed, 27 insertions, 39 deletions
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) |