diff options
| -rw-r--r-- | Category/Instance/Cospans.agda | 1 | ||||
| -rw-r--r-- | Category/Instance/DecoratedCospans.agda | 270 | ||||
| -rw-r--r-- | Category/Monoidal/Coherence.agda | 132 |
3 files changed, 377 insertions, 26 deletions
diff --git a/Category/Instance/Cospans.agda b/Category/Instance/Cospans.agda index a3f8fb0..ccefcf5 100644 --- a/Category/Instance/Cospans.agda +++ b/Category/Instance/Cospans.agda @@ -70,6 +70,7 @@ record Same (C C′ : Cospan A B) : Set (ℓ ⊔ e) where ≅N : C.N ≅ C′.N open _≅_ ≅N public + module ≅N = _≅_ ≅N field from∘f₁≈f₁′ : from ∘ C.f₁ ≈ C′.f₁ diff --git a/Category/Instance/DecoratedCospans.agda b/Category/Instance/DecoratedCospans.agda index a952906..8d67536 100644 --- a/Category/Instance/DecoratedCospans.agda +++ b/Category/Instance/DecoratedCospans.agda @@ -19,28 +19,31 @@ import Category.Instance.Cospans 𝒞 as Cospans open import Categories.Category using (Category; _[_∘_]; _[_≈_]) +open import Categories.Diagram.Pushout using (Pushout) +open import Categories.Functor.Properties using ([_]-resp-≅) open import Categories.Morphism.Reasoning using (switch-fromtoˡ; glueTrianglesˡ) open import Cospan.Decorated 𝒞 F using (DecoratedCospan) open import Data.Product using (_,_) open import Level using (_⊔_) -open import Categories.Functor.Properties using ([_]-resp-≅) + +import Category.Monoidal.Coherence as Coherence import Categories.Morphism as Morphism +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning module 𝒞 = FinitelyCocompleteCategory 𝒞 module 𝒟 = SymmetricMonoidalCategory 𝒟 -open Morphism 𝒞.U using (module ≅) -open Morphism using () renaming (_≅_ to _[_≅_]) open SymmetricMonoidalFunctor F - using (F₀; F₁; ⊗-homo; ε; homomorphism) + -- using (F₀; F₁; ⊗-homo; ε; homomorphism) renaming (identity to F-identity; F to F′) private variable - A B C : 𝒞.Obj + A B C D : 𝒞.Obj compose : DecoratedCospan A B → DecoratedCospan B C → DecoratedCospan A C compose c₁ c₂ = record @@ -51,13 +54,13 @@ compose c₁ c₂ = record module C₁ = DecoratedCospan c₁ module C₂ = DecoratedCospan c₂ open 𝒞 using ([_,_]; _+_) - open 𝒟 using (_⊗₀_; _⊗₁_; _∘_; unitorˡ; _⇒_; unit) + open 𝒟 using (_⊗₀_; _⊗₁_; _∘_; unitorʳ; _⇒_; unit) module p = 𝒞.pushout C₁.f₂ C₂.f₁ open p using (i₁; i₂) φ : F₀ C₁.N ⊗₀ F₀ C₂.N ⇒ F₀ (C₁.N + C₂.N) φ = ⊗-homo.⇒.η (C₁.N , C₂.N) s⊗t : unit ⇒ F₀ C₁.N ⊗₀ F₀ C₂.N - s⊗t = C₁.decoration ⊗₁ C₂.decoration ∘ unitorˡ.to + s⊗t = C₁.decoration ⊗₁ C₂.decoration ∘ unitorʳ.to identity : DecoratedCospan A A identity = record @@ -71,46 +74,261 @@ record Same (C₁ C₂ : DecoratedCospan A B) : Set (ℓ ⊔ e) where module C₂ = DecoratedCospan C₂ field - ≅N : 𝒞.U [ C₁.N ≅ C₂.N ] + cospans-≈ : Cospans.Same C₁.cospan C₂.cospan - module ≅N = _[_≅_] ≅N + open Cospans.Same cospans-≈ + open 𝒟 + open Morphism U using (_≅_) field - from∘f₁≈f₁′ : 𝒞.U [ 𝒞.U [ ≅N.from ∘ C₁.f₁ ] ≈ C₂.f₁ ] - from∘f₂≈f₂′ : 𝒞.U [ 𝒞.U [ ≅N.from ∘ C₁.f₂ ] ≈ C₂.f₂ ] - same-deco : 𝒟.U [ 𝒟.U [ F₁ ≅N.from ∘ C₁.decoration ] ≈ C₂.decoration ] + same-deco : F₁ ≅N.from ∘ C₁.decoration ≈ C₂.decoration - ≅F[N] : 𝒟.U [ F₀ C₁.N ≅ F₀ C₂.N ] + ≅F[N] : F₀ C₁.N ≅ F₀ C₂.N ≅F[N] = [ F′ ]-resp-≅ ≅N same-refl : {C : DecoratedCospan A B} → Same C C same-refl = record - { ≅N = ≅.refl - ; from∘f₁≈f₁′ = 𝒞.identityˡ - ; from∘f₂≈f₂′ = 𝒞.identityˡ - ; same-deco = F-identity ⟩∘⟨refl ○ 𝒟.identityˡ + { cospans-≈ = Cospans.same-refl + ; same-deco = F-identity ⟩∘⟨refl ○ identityˡ } where - open 𝒟.HomReasoning + open 𝒟 + open HomReasoning same-sym : {C C′ : DecoratedCospan A B} → Same C C′ → Same C′ C same-sym C≅C′ = record - { ≅N = ≅.sym ≅N - ; from∘f₁≈f₁′ = 𝒞.Equiv.sym (switch-fromtoˡ 𝒞.U ≅N from∘f₁≈f₁′) - ; from∘f₂≈f₂′ = 𝒞.Equiv.sym (switch-fromtoˡ 𝒞.U ≅N from∘f₂≈f₂′) - ; same-deco = 𝒟.Equiv.sym (switch-fromtoˡ 𝒟.U ≅F[N] same-deco) + { cospans-≈ = Cospans.same-sym cospans-≈ + ; same-deco = sym (switch-fromtoˡ 𝒟.U ≅F[N] same-deco) } where open Same C≅C′ + open 𝒟.Equiv same-trans : {C C′ C″ : DecoratedCospan A B} → Same C C′ → Same C′ C″ → Same C C″ same-trans C≈C′ C′≈C″ = record - { ≅N = ≅.trans C≈C′.≅N C′≈C″.≅N - ; from∘f₁≈f₁′ = glueTrianglesˡ 𝒞.U C′≈C″.from∘f₁≈f₁′ C≈C′.from∘f₁≈f₁′ - ; from∘f₂≈f₂′ = glueTrianglesˡ 𝒞.U C′≈C″.from∘f₂≈f₂′ C≈C′.from∘f₂≈f₂′ - ; same-deco = homomorphism ⟩∘⟨refl ○ glueTrianglesˡ 𝒟.U C′≈C″.same-deco C≈C′.same-deco + { cospans-≈ = Cospans.same-trans C≈C′.cospans-≈ C′≈C″.cospans-≈ + ; same-deco = + homomorphism ⟩∘⟨refl ○ + glueTrianglesˡ 𝒟.U C′≈C″.same-deco C≈C′.same-deco } where module C≈C′ = Same C≈C′ module C′≈C″ = Same C′≈C″ open 𝒟.HomReasoning + +compose-assoc + : {c₁ : DecoratedCospan A B} + {c₂ : DecoratedCospan B C} + {c₃ : DecoratedCospan C D} + → Same (compose c₁ (compose c₂ c₃)) (compose (compose c₁ c₂) c₃) +compose-assoc {_} {_} {_} {_} {c₁} {c₂} {c₃} = record + { cospans-≈ = Cospans.compose-assoc + ; same-deco = deco-assoc + } + where + module C₁ = DecoratedCospan c₁ + module C₂ = DecoratedCospan c₂ + module C₃ = DecoratedCospan c₃ + open 𝒞 using (+-assoc; pushout; [_,_]; _+₁_; _+_) renaming (_∘_ to _∘′_; id to id′) + p₁ = pushout C₁.f₂ C₂.f₁ + p₂ = pushout C₂.f₂ C₃.f₁ + module P₁ = Pushout p₁ + module P₂ = Pushout p₂ + p₃ = pushout P₁.i₂ P₂.i₁ + p₁₃ = Cospans.glue-i₂ p₁ p₃ + p₂₃ = Cospans.glue-i₁ p₂ p₃ + p₄ = pushout C₁.f₂ (P₂.i₁ ∘′ C₂.f₁) + p₅ = pushout (P₁.i₂ ∘′ C₂.f₂) C₃.f₁ + module P₃ = Pushout p₃ + module P₄ = Pushout p₄ + module P₅ = Pushout p₅ + module P₁₃ = Pushout p₁₃ + module P₂₃ = Pushout p₂₃ + open Morphism 𝒞.U using (_≅_) + module P₄≅P₁₃ = _≅_ (Cospans.up-to-iso p₄ p₁₃) + module P₅≅P₂₃ = _≅_ (Cospans.up-to-iso p₅ p₂₃) + + N = C₁.N + M = C₂.N + P = C₃.N + Q = P₁.Q + R = P₂.Q + φ = ⊗-homo.⇒.η + φ-commute = ⊗-homo.⇒.commute + + a = C₁.f₂ + b = C₂.f₁ + c = C₂.f₂ + d = C₂.f₁ + + f = P₁.i₁ + g = P₁.i₂ + h = P₂.i₁ + i = P₂.i₂ + + j = P₃.i₁ + k = P₃.i₂ + + w = P₄.i₁ + x = P₄.i₂ + y = P₅.i₁ + z = P₅.i₂ + + l = P₅≅P₂₃.to + m = P₄≅P₁₃.from + + module +-assoc = _≅_ +-assoc + + module _ where + + open 𝒞 using (∘[]; []-congʳ; []-congˡ; []∘+₁) + open 𝒞.Dual.op-binaryProducts 𝒞.cocartesian + using () + renaming (⟨⟩-cong₂ to []-cong₂; assocˡ∘⟨⟩ to []∘assocˡ) + + open ⇒-Reasoning 𝒞.U + open 𝒞 using (id; _∘_; _≈_; assoc; identityʳ) + open 𝒞.HomReasoning + open 𝒞.Equiv + + copairings : ((l ∘ m) ∘ [ w , x ]) ∘ (id +₁ [ h , i ]) ≈ [ y , z ] ∘ ([ f , g ] +₁ id) ∘ +-assoc.from + copairings = begin + ((l ∘ m) ∘ [ w , x ]) ∘ (id +₁ [ h , i ]) ≈⟨ pushˡ assoc ⟩ + l ∘ (m ∘ [ w , x ]) ∘ (id +₁ [ h , i ]) ≈⟨ refl⟩∘⟨ ∘[] ⟩∘⟨refl ⟩ + l ∘ [ m ∘ w , m ∘ x ] ∘ (id +₁ [ h , i ]) ≈⟨ refl⟩∘⟨ []-cong₂ (P₄.universal∘i₁≈h₁) (P₄.universal∘i₂≈h₂) ⟩∘⟨refl ⟩ + l ∘ [ j ∘ f , k ] ∘ (id +₁ [ h , i ]) ≈⟨ pullˡ ∘[] ⟩ + [ l ∘ j ∘ f , l ∘ k ] ∘ (id +₁ [ h , i ]) ≈⟨ []-congʳ (pullˡ P₂₃.universal∘i₁≈h₁) ⟩∘⟨refl ⟩ + [ y ∘ f , l ∘ k ] ∘ (id +₁ [ h , i ]) ≈⟨ []∘+₁ ⟩ + [ (y ∘ f) ∘ id , (l ∘ k) ∘ [ h , i ] ] ≈⟨ []-cong₂ identityʳ (pullʳ ∘[]) ⟩ + [ y ∘ f , l ∘ [ k ∘ h , k ∘ i ] ] ≈⟨ []-congˡ (refl⟩∘⟨ []-congʳ P₃.commute) ⟨ + [ y ∘ f , l ∘ [ j ∘ g , k ∘ i ] ] ≈⟨ []-congˡ ∘[] ⟩ + [ y ∘ f , [ l ∘ j ∘ g , l ∘ k ∘ i ] ] ≈⟨ []-congˡ ([]-congˡ 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.from ≈⟨ []-cong₂ ∘[] identityʳ ⟩∘⟨refl ⟨ + [ y ∘ [ f , g ] , z ∘ id ] ∘ +-assoc.from ≈⟨ pullˡ []∘+₁ ⟨ + [ y , z ] ∘ ([ f , g ] +₁ id) ∘ +-assoc.from ∎ + + module _ where + + open ⊗-Reasoning 𝒟.monoidal + open ⇒-Reasoning 𝒟.U + open 𝒟 using (_⊗₀_; _⊗₁_; id; _∘_; _≈_; assoc; sym-assoc; identityʳ; ⊗; identityˡ; triangle; assoc-commute-to; assoc-commute-from) + open 𝒟 using (_⇒_; unit) + + α⇒ = 𝒟.associator.from + α⇐ = 𝒟.associator.to + + λ⇒ = 𝒟.unitorˡ.from + λ⇐ = 𝒟.unitorˡ.to + + ρ⇒ = 𝒟.unitorʳ.from + ρ⇐ = 𝒟.unitorʳ.to + + module α≅ = 𝒟.associator + module λ≅ = 𝒟.unitorˡ + module ρ≅ = 𝒟.unitorʳ + + open Coherence 𝒟.monoidal using (λ₁≅ρ₁⇐) + open 𝒟.Equiv + + +-α⇒ = +-assoc.from + +-α⇐ = +-assoc.to + + s : unit ⇒ F₀ C₁.N + s = C₁.decoration + + t : unit ⇒ F₀ C₂.N + t = C₂.decoration + + u : unit ⇒ F₀ C₃.N + u = C₃.decoration + + F-copairings : F₁ (l ∘′ m) ∘ F₁ [ w , x ] ∘ F₁ (id′ +₁ [ h , i ]) ≈ F₁ [ y , z ] ∘ F₁ ([ f , g ] +₁ id′) ∘ F₁ (+-assoc.from) + F-copairings = begin + F₁ (l ∘′ m) ∘ F₁ [ w , x ] ∘ F₁ (id′ +₁ [ h , i ]) ≈⟨ pushˡ homomorphism ⟨ + F₁ ((l ∘′ m) ∘′ [ w , x ]) ∘ F₁ (id′ +₁ [ h , i ]) ≈⟨ homomorphism ⟨ + F₁ (((l ∘′ m) ∘′ [ w , x ]) ∘′ (id′ +₁ [ h , i ])) ≈⟨ F-resp-≈ copairings ⟩ + F₁ ([ y , z ] ∘′ ([ f , g ] +₁ id′) ∘′ +-assoc.from) ≈⟨ homomorphism ⟩ + F₁ [ y , z ] ∘ F₁ (([ f , g ] +₁ id′) ∘′ +-assoc.from) ≈⟨ refl⟩∘⟨ homomorphism ⟩ + F₁ [ y , z ] ∘ F₁ ([ f , g ] +₁ id′) ∘ F₁ +-assoc.from ∎ + + coherences : φ (N , M + P) ∘ id ⊗₁ φ (M , P) ≈ F₁ +-assoc.to ∘ φ (N + M , P) ∘ φ (N , M) ⊗₁ id ∘ α⇐ + coherences = begin + φ (N , M + P) ∘ id ⊗₁ φ (M , P) ≈⟨ insertʳ α≅.isoʳ ⟩ + ((φ (N , M + P) ∘ id ⊗₁ φ (M , P)) ∘ α⇒) ∘ α⇐ ≈⟨ assoc ⟩∘⟨refl ⟩ + (φ (N , M + P) ∘ id ⊗₁ φ (M , P) ∘ α⇒) ∘ α⇐ ≈⟨ assoc ⟩ + φ (N , M + P) ∘ (id ⊗₁ φ (M , P) ∘ α⇒) ∘ α⇐ ≈⟨ extendʳ associativity ⟨ + F₁ +-assoc.to ∘ (φ (N + M , P) ∘ φ (N , M) ⊗₁ id) ∘ α⇐ ≈⟨ refl⟩∘⟨ assoc ⟩ + F₁ +-assoc.to ∘ φ (N + M , P) ∘ φ (N , M) ⊗₁ id ∘ α⇐ ∎ + + triangle-to : α⇒ ∘ ρ⇐ ⊗₁ id ≈ id ⊗₁ λ⇐ + triangle-to = begin + α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ pullˡ identityˡ ⟨ + id ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ ⊗.identity ⟩∘⟨refl ⟨ + id ⊗₁ id ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ refl⟩⊗⟨ λ≅.isoˡ ⟩∘⟨refl ⟨ + id ⊗₁ (λ⇐ ∘ λ⇒) ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ identityʳ ⟩⊗⟨refl ⟩∘⟨refl ⟨ + (id ∘ id) ⊗₁ (λ⇐ ∘ λ⇒) ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ pushˡ ⊗-distrib-over-∘ ⟩ + id ⊗₁ λ⇐ ∘ id ⊗₁ λ⇒ ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ pullˡ triangle ⟩ + id ⊗₁ λ⇐ ∘ ρ⇒ ⊗₁ id ∘ ρ⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟨ + id ⊗₁ λ⇐ ∘ (ρ⇒ ∘ ρ⇐) ⊗₁ (id ∘ id) ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ identityˡ ⟩ + id ⊗₁ λ⇐ ∘ (ρ⇒ ∘ ρ⇐) ⊗₁ id ≈⟨ refl⟩∘⟨ ρ≅.isoʳ ⟩⊗⟨refl ⟩ + id ⊗₁ λ⇐ ∘ id ⊗₁ id ≈⟨ refl⟩∘⟨ ⊗.identity ⟩ + id ⊗₁ λ⇐ ∘ id ≈⟨ identityʳ ⟩ + id ⊗₁ λ⇐ ∎ + + unitors : s ⊗₁ (t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ ≈ α⇒ ∘ (s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ + unitors = begin + s ⊗₁ (t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ ≈⟨ pushˡ split₂ʳ ⟩ + s ⊗₁ t ⊗₁ u ∘ id ⊗₁ ρ⇐ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ λ₁≅ρ₁⇐ ⟩∘⟨refl ⟨ + s ⊗₁ t ⊗₁ u ∘ id ⊗₁ λ⇐ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pullˡ triangle-to ⟨ + s ⊗₁ t ⊗₁ u ∘ α⇒ ∘ ρ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ extendʳ assoc-commute-from ⟨ + α⇒ ∘ (s ⊗₁ t) ⊗₁ u ∘ ρ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pushˡ split₁ʳ ⟨ + α⇒ ∘ (s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ∎ + + F-l∘m = F₁ (l ∘′ m) + F[w,x] = F₁ [ w , x ] + F[h,i] = F₁ [ h , i ] + F[y,z] = F₁ [ y , z ] + F[f,g] = F₁ [ f , g ] + F-[f,g]+id = F₁ ([ f , g ] +₁ id′) + F-id+[h,i] = F₁ (id′ +₁ [ h , i ]) + φ-N,R = φ (N , R) + φ-M,P = φ (M , P) + φ-N+M,P = φ (N + M , P) + φ-N+M = φ (N , M) + φ-N,M+P = φ (N , M + P) + φ-N,M = φ (N , M) + φ-Q,P = φ (Q , P) + s⊗[t⊗u] = s ⊗₁ (t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ + [s⊗t]⊗u = (s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ + + deco-assoc + : F-l∘m ∘ F[w,x] ∘ φ-N,R ∘ s ⊗₁ (F[h,i] ∘ φ-M,P ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ + ≈ F[y,z] ∘ φ-Q,P ∘ (F[f,g] ∘ φ-N,M ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ + deco-assoc = begin + F-l∘m ∘ F[w,x] ∘ φ-N,R ∘ s ⊗₁ (F[h,i] ∘ φ-M,P ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ ≈⟨ pullˡ refl ⟩ + (F-l∘m ∘ F[w,x]) ∘ φ-N,R ∘ s ⊗₁ (F[h,i] ∘ φ-M,P ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ split₂ˡ ⟩∘⟨refl ⟩ + (F-l∘m ∘ F[w,x]) ∘ φ-N,R ∘ (id ⊗₁ F[h,i] ∘ s ⊗₁ (φ-M,P ∘ t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ split₂ˡ) ⟩∘⟨refl ⟩ + (F-l∘m ∘ F[w,x]) ∘ φ-N,R ∘ (id ⊗₁ F[h,i] ∘ id ⊗₁ φ-M,P ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩ + (F-l∘m ∘ F[w,x]) ∘ φ-N,R ∘ id ⊗₁ F[h,i] ∘ (id ⊗₁ φ-M,P ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F-identity ⟩⊗⟨refl ⟩∘⟨ refl ⟨ + (F-l∘m ∘ F[w,x]) ∘ φ-N,R ∘ F₁ id′ ⊗₁ F[h,i] ∘ (id ⊗₁ φ-M,P ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (id′ , [ h , i ])) ⟩ + (F-l∘m ∘ F[w,x]) ∘ F-id+[h,i] ∘ φ-N,M+P ∘ (id ⊗₁ φ-M,P ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ pullˡ assoc ⟩ + (F-l∘m ∘ F[w,x] ∘ F-id+[h,i]) ∘ φ-N,M+P ∘ (id ⊗₁ φ-M,P ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩ + (F-l∘m ∘ F[w,x] ∘ F-id+[h,i]) ∘ φ-N,M+P ∘ id ⊗₁ φ-M,P ∘ s⊗[t⊗u] ≈⟨ refl⟩∘⟨ sym-assoc ⟩ + (F-l∘m ∘ F[w,x] ∘ F-id+[h,i]) ∘ (φ-N,M+P ∘ id ⊗₁ φ-M,P) ∘ s⊗[t⊗u] ≈⟨ F-copairings ⟩∘⟨ coherences ⟩∘⟨ unitors ⟩ + (F[y,z] ∘ F-[f,g]+id ∘ F₁ +-α⇒) ∘ (F₁ +-α⇐ ∘ φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ sym-assoc ⟩∘⟨ assoc ⟩ + ((F[y,z] ∘ F-[f,g]+id) ∘ F₁ +-α⇒) ∘ F₁ +-α⇐ ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ assoc ⟩ + (F[y,z] ∘ F-[f,g]+id) ∘ F₁ +-α⇒ ∘ F₁ +-α⇐ ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ pushˡ homomorphism ⟨ + (F[y,z] ∘ F-[f,g]+id) ∘ F₁ (+-α⇒ ∘′ +-α⇐) ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ F-resp-≈ +-assoc.isoʳ ⟩∘⟨refl ⟩ + (F[y,z] ∘ F-[f,g]+id) ∘ F₁ id′ ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ F-identity ⟩∘⟨refl ⟩ + (F[y,z] ∘ F-[f,g]+id) ∘ id ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ identityˡ ⟩ + (F[y,z] ∘ F-[f,g]+id) ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ sym-assoc ⟩∘⟨refl ⟩ + (F[y,z] ∘ F-[f,g]+id) ∘ ((φ-N+M,P ∘ φ-N,M ⊗₁ id) ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ cancelInner α≅.isoˡ ⟩ + (F[y,z] ∘ F-[f,g]+id) ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id) ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ assoc ⟩ + (F[y,z] ∘ F-[f,g]+id) ∘ φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ [s⊗t]⊗u ≈⟨ assoc ⟩ + F[y,z] ∘ F-[f,g]+id ∘ φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟨ + F[y,z] ∘ F-[f,g]+id ∘ φ-N+M,P ∘ (φ-N,M ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute ([ f , g ] , id′)) ⟨ + F[y,z] ∘ φ-Q,P ∘ F[f,g] ⊗₁ F₁ id′ ∘ (φ-N,M ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ F-identity ⟩∘⟨ refl ⟩ + F[y,z] ∘ φ-Q,P ∘ F[f,g] ⊗₁ id ∘ (φ-N,M ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟨ + F[y,z] ∘ φ-Q,P ∘ (F[f,g] ∘ φ-N,M ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ∎ diff --git a/Category/Monoidal/Coherence.agda b/Category/Monoidal/Coherence.agda new file mode 100644 index 0000000..7603860 --- /dev/null +++ b/Category/Monoidal/Coherence.agda @@ -0,0 +1,132 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category.Core using (Category) +open import Categories.Category.Monoidal.Core using (Monoidal) + +module Category.Monoidal.Coherence {o ℓ e} {𝒞 : Category o ℓ e} (monoidal : Monoidal 𝒞) where + +import Categories.Morphism as Morphism +import Categories.Morphism.IsoEquiv as IsoEquiv +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning + +open import Categories.Functor.Properties using ([_]-resp-≅) + +open Monoidal monoidal +open Category 𝒞 + +open ⇒-Reasoning 𝒞 +open ⊗-Reasoning monoidal +open Morphism 𝒞 using (_≅_) +open IsoEquiv 𝒞 using (to-unique) + +open Equiv + +𝟏 : Obj +𝟏 = unit + +module α≅ = associator +module λ≅ = unitorˡ +module ρ≅ = unitorʳ + +private + variable + A B C D : Obj + +α⇒ : (A ⊗₀ B) ⊗₀ C ⇒ A ⊗₀ B ⊗₀ C +α⇒ = α≅.from + +α⇐ : A ⊗₀ B ⊗₀ C ⇒ (A ⊗₀ B) ⊗₀ C +α⇐ = α≅.to + +λ⇒ : 𝟏 ⊗₀ A ⇒ A +λ⇒ = λ≅.from + +λ⇐ : A ⇒ 𝟏 ⊗₀ A +λ⇐ = λ≅.to + +ρ⇒ : A ⊗₀ 𝟏 ⇒ A +ρ⇒ = ρ≅.from + +ρ⇐ : A ⇒ A ⊗₀ 𝟏 +ρ⇐ = ρ≅.to + +α⊗id : ((A ⊗₀ B) ⊗₀ C) ⊗₀ D ≅ (A ⊗₀ B ⊗₀ C) ⊗₀ D +α⊗id {A} {B} {C} {D} = [ -⊗ D ]-resp-≅ (associator {A} {B} {C}) + +module α⊗id {A} {B} {C} {D} = _≅_ (α⊗id {A} {B} {C} {D}) + +perimeter + : α⇒ {𝟏} {A} {B} ∘ (ρ⇒ {𝟏} ⊗₁ id {A}) ⊗₁ id {B} + ≈ id {𝟏} ⊗₁ λ⇒ {A ⊗₀ B} ∘ id {𝟏} ⊗₁ α⇒ {𝟏} {A} {B} ∘ α⇒ {𝟏} {𝟏 ⊗₀ A} {B} ∘ α⇒ {𝟏} {𝟏} {A} ⊗₁ id {B} +perimeter = begin + α⇒ ∘ (ρ⇒ ⊗₁ id) ⊗₁ id ≈⟨ assoc-commute-from ⟩ + ρ⇒ ⊗₁ id ⊗₁ id ∘ α⇒ ≈⟨ refl⟩⊗⟨ ⊗.identity ⟩∘⟨refl ⟩ + ρ⇒ ⊗₁ id ∘ α⇒ ≈⟨ pullˡ triangle ⟨ + id ⊗₁ λ⇒ ∘ α⇒ ∘ α⇒ ≈⟨ refl⟩∘⟨ pentagon ⟨ + id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ α⇒ ∘ α⇒ ⊗₁ id ∎ + +perimeter-triangle + : α⇒ {𝟏} {A} {C} ∘ (id {𝟏} ⊗₁ λ⇒ {A}) ⊗₁ id {C} + ≈ id {𝟏} ⊗₁ λ⇒ {A ⊗₀ C} ∘ id {𝟏} ⊗₁ α⇒ {𝟏} {A} {C} ∘ α⇒ {𝟏} {𝟏 ⊗₀ A} {C} +perimeter-triangle = begin + α⇒ ∘ (id ⊗₁ λ⇒) ⊗₁ id ≈⟨ refl⟩∘⟨ identityʳ ⟨ + α⇒ ∘ (id ⊗₁ λ⇒) ⊗₁ id ∘ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ α⊗id.isoʳ ⟨ + α⇒ ∘ (id ⊗₁ λ⇒) ⊗₁ id ∘ α⇒ ⊗₁ id ∘ α⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟨ + α⇒ ∘ (id ⊗₁ λ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ triangle ⟩⊗⟨refl ⟩∘⟨refl ⟩ + α⇒ ∘ (ρ⇒ ⊗₁ id) ⊗₁ id ∘ α⇐ ⊗₁ id ≈⟨ extendʳ perimeter ⟩ + id ⊗₁ λ⇒ ∘ (id ⊗₁ α⇒ ∘ α⇒ ∘ α⇒ ⊗₁ id) ∘ α⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ assoc ⟩ + id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ (α⇒ ∘ α⇒ ⊗₁ id) ∘ α⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩ + id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ α⇒ ∘ α⇒ ⊗₁ id ∘ α⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ α⊗id.isoʳ ⟩ + id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ α⇒ ∘ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ ⟩ + id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ α⇒ ∎ + +perimeter-triangle-square + : ∀ {A C : Obj} + → id {𝟏} ⊗₁ λ⇒ {A} ⊗₁ id {C} + ≈ id {𝟏} ⊗₁ λ⇒ {A ⊗₀ C} ∘ id {𝟏} ⊗₁ α⇒ {𝟏} {A} {C} +perimeter-triangle-square = begin + id ⊗₁ λ⇒ ⊗₁ id ≈⟨ identityʳ ⟨ + id ⊗₁ λ⇒ ⊗₁ id ∘ id ≈⟨ refl⟩∘⟨ associator.isoʳ ⟨ + id ⊗₁ λ⇒ ⊗₁ id ∘ α⇒ ∘ α⇐ ≈⟨ extendʳ assoc-commute-from ⟨ + α⇒ ∘ (id ⊗₁ λ⇒) ⊗₁ id ∘ α⇐ ≈⟨ extendʳ perimeter-triangle ⟩ + id ⊗₁ λ⇒ ∘ (id ⊗₁ α⇒ ∘ α⇒) ∘ α⇐ ≈⟨ refl⟩∘⟨ assoc ⟩ + id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ α⇒ ∘ α⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ associator.isoʳ ⟩ + id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩ + id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∎ + +λₕi≈λₕᵢ∘α₁ₕᵢ : λ⇒ {A} ⊗₁ id {C} ≈ λ⇒ {A ⊗₀ C} ∘ α⇒ {𝟏} {A} {C} +λₕi≈λₕᵢ∘α₁ₕᵢ = begin + λ⇒ ⊗₁ id ≈⟨ insertʳ unitorˡ.isoʳ ⟩ + (λ⇒ ⊗₁ id ∘ λ⇒) ∘ λ⇐ ≈⟨ unitorˡ-commute-from ⟩∘⟨refl ⟨ + (λ⇒ ∘ id ⊗₁ λ⇒ ⊗₁ id) ∘ λ⇐ ≈⟨ (refl⟩∘⟨ perimeter-triangle-square) ⟩∘⟨refl ⟩ + (λ⇒ ∘ id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒) ∘ λ⇐ ≈⟨ (refl⟩∘⟨ merge₂ˡ) ⟩∘⟨refl ⟩ + (λ⇒ ∘ id ⊗₁ (λ⇒ ∘ α⇒)) ∘ λ⇐ ≈⟨ unitorˡ-commute-from ⟩∘⟨refl ⟩ + ((λ⇒ ∘ α⇒) ∘ λ⇒) ∘ λ⇐ ≈⟨ cancelʳ unitorˡ.isoʳ ⟩ + λ⇒ ∘ α⇒ ∎ + +1λ₁≈λ₁₁ : id {𝟏} ⊗₁ λ⇒ {𝟏} ≈ λ⇒ {𝟏 ⊗₀ 𝟏} +1λ₁≈λ₁₁ = begin + id ⊗₁ λ⇒ ≈⟨ insertˡ unitorˡ.isoˡ ⟩ + λ⇐ ∘ λ⇒ ∘ id ⊗₁ λ⇒ ≈⟨ refl⟩∘⟨ unitorˡ-commute-from ⟩ + λ⇐ ∘ λ⇒ ∘ λ⇒ ≈⟨ cancelˡ unitorˡ.isoˡ ⟩ + λ⇒ ∎ + +λ₁𝟏≈ρ₁𝟏 : λ⇒ {𝟏} ⊗₁ id {𝟏} ≈ ρ⇒ {𝟏} ⊗₁ id {𝟏} +λ₁𝟏≈ρ₁𝟏 = begin + λ⇒ ⊗₁ id ≈⟨ λₕi≈λₕᵢ∘α₁ₕᵢ ⟩ + λ⇒ ∘ α⇒ ≈⟨ 1λ₁≈λ₁₁ ⟩∘⟨refl ⟨ + id ⊗₁ λ⇒ ∘ α⇒ ≈⟨ triangle ⟩ + ρ⇒ ⊗₁ id ∎ + +λ₁≅ρ₁⇒ : λ⇒ {𝟏} ≈ ρ⇒ {𝟏} +λ₁≅ρ₁⇒ = begin + λ⇒ ≈⟨ insertʳ unitorʳ.isoʳ ⟩ + (λ⇒ ∘ ρ⇒) ∘ ρ⇐ ≈⟨ unitorʳ-commute-from ⟩∘⟨refl ⟨ + (ρ⇒ ∘ λ⇒ ⊗₁ id) ∘ ρ⇐ ≈⟨ (refl⟩∘⟨ λ₁𝟏≈ρ₁𝟏) ⟩∘⟨refl ⟩ + (ρ⇒ ∘ ρ⇒ ⊗₁ id) ∘ ρ⇐ ≈⟨ unitorʳ-commute-from ⟩∘⟨refl ⟩ + (ρ⇒ ∘ ρ⇒) ∘ ρ⇐ ≈⟨ cancelʳ unitorʳ.isoʳ ⟩ + ρ⇒ ∎ + +λ₁≅ρ₁⇐ : λ⇐ {𝟏} ≈ ρ⇐ {𝟏} +λ₁≅ρ₁⇐ = to-unique λ≅.iso ρ≅.iso λ₁≅ρ₁⇒ |