diff options
Diffstat (limited to 'Functor')
| -rw-r--r-- | Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda | 12 | ||||
| -rw-r--r-- | Functor/Exact/Instance/Swap.agda | 10 | ||||
| -rw-r--r-- | Functor/Instance/CMonoidalize.agda | 2 | ||||
| -rw-r--r-- | Functor/Instance/Cospan/Stack.agda | 3 | ||||
| -rw-r--r-- | Functor/Instance/Decorate.agda | 9 | ||||
| -rw-r--r-- | Functor/Instance/DecoratedCospan/Embed.agda | 14 | ||||
| -rw-r--r-- | Functor/Instance/DecoratedCospan/Stack.agda | 35 | ||||
| -rw-r--r-- | Functor/Instance/Monoidalize.agda | 4 | ||||
| -rw-r--r-- | Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda | 90 | ||||
| -rw-r--r-- | Functor/Monoidal/Construction/CMonoidValued.agda | 2 | ||||
| -rw-r--r-- | Functor/Monoidal/Construction/MonoidValued.agda | 4 |
11 files changed, 87 insertions, 98 deletions
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 } |