diff options
Diffstat (limited to 'Data')
| -rw-r--r-- | Data/WiringDiagram/Balanced.agda | 77 | ||||
| -rw-r--r-- | Data/WiringDiagram/Core.agda | 26 | ||||
| -rw-r--r-- | Data/WiringDiagram/Directed.agda | 192 | ||||
| -rw-r--r-- | Data/WiringDiagram/Equalities.agda | 179 | ||||
| -rw-r--r-- | Data/WiringDiagram/Looped.agda | 28 |
5 files changed, 158 insertions, 344 deletions
diff --git a/Data/WiringDiagram/Balanced.agda b/Data/WiringDiagram/Balanced.agda index 2af7cb6..5a3aa3a 100644 --- a/Data/WiringDiagram/Balanced.agda +++ b/Data/WiringDiagram/Balanced.agda @@ -1,17 +1,16 @@ {-# OPTIONS --without-K --safe #-} open import Categories.Category using (Category) -open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger) +open import Category.Dagger.Semiadditive using (SemiadditiveDagger) open import Level using (Level) module Data.WiringDiagram.Balanced {o ℓ e : Level} {𝒞 : Category o ℓ e} - (S : IdempotentSemiadditiveDagger 𝒞) + (S : SemiadditiveDagger 𝒞) where -import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning -import Categories.Morphism.Reasoning as ⇒-Reasoning +import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning open import Categories.Functor using (Functor) open import Data.WiringDiagram.Core S using (WiringDiagram; _□_; _⌸_; push; pull) @@ -51,37 +50,21 @@ Push = record ; F-resp-≈ = λ f≈g → (⟨ f≈g ⟩† ⟩∘⟨refl) ⌸ f≈g } where - open IdempotentSemiadditiveDagger S - using (+-monoidal; _†; p₂; _⊕₁_; △; !; p₁; p₂-⊕; ⇒!; ⇒△; ρ⇒≈p₁; p₁∘△; †-homomorphism; †-identity; ⟨_⟩†) - open Monoidal +-monoidal using (assoc-commute-from; unitorˡ-commute-from; triangle) - open Shorthands +-monoidal using (α⇒; λ⇒; ρ⇒) - open ⇒-Reasoning 𝒞 - open ⊗-Reasoning +-monoidal + open SemiadditiveDagger S + open ⇒-Reasoning + open HomReasoning + open Equiv homoᵢ : {A B C : Obj} (f : A ⇒ B) (g : B ⇒ C) - → (g ∘ f) † ∘ p₂ - ≈ (f † ∘ p₂) ∘ id ⊕₁ ((g † ∘ p₂) ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + → (g ∘ f) † ∘ π₂ + ≈ (f † ∘ π₂) ∘ ⟨ π₁ , ((g † ∘ π₂) ∘ f ×₁ id) ⟩ homoᵢ f g = begin - (g ∘ f) † ∘ p₂ ≈⟨ pushˡ †-homomorphism ⟩ - f † ∘ g † ∘ p₂ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ p₂-⊕ ⟩ - f † ∘ g † ∘ λ⇒ ∘ ! ⊕₁ id ≈⟨ refl⟩∘⟨ extendʳ unitorˡ-commute-from ⟨ - f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ ! ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ insertˡ p₁∘△ ⟩⊗⟨refl ⟩ - f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ (p₁ ∘ △ ∘ !) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (ρ⇒≈p₁ ⟩∘⟨refl) ⟩⊗⟨refl ⟨ - f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ (ρ⇒ ∘ △ ∘ !) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ˡ ⟩ - f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ ρ⇒ ⊕₁ id ∘ (△ ∘ !) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⇒△ ⟩⊗⟨refl ⟩ - f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ ρ⇒ ⊕₁ id ∘ (! ⊕₁ ! ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ˡ ⟩ - f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ ρ⇒ ⊕₁ id ∘ (! ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (Equiv.sym triangle) ⟩ - f † ∘ λ⇒ ∘ id ⊕₁ (g †) ∘ id ⊕₁ λ⇒ ∘ α⇒ ∘ (! ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩ - f † ∘ λ⇒ ∘ id ⊕₁ (g † ∘ λ⇒) ∘ α⇒ ∘ (! ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟩ - f † ∘ λ⇒ ∘ id ⊕₁ (g † ∘ λ⇒) ∘ ! ⊕₁ ! ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩ - f † ∘ λ⇒ ∘ ! ⊕₁ ((g † ∘ λ⇒) ∘ ! ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (pullʳ (refl⟩∘⟨ (Equiv.sym ⇒! ⟩⊗⟨refl))) ⟩∘⟨refl ⟩ - f † ∘ λ⇒ ∘ ! ⊕₁ (g † ∘ λ⇒ ∘ (! ∘ f) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ (pushʳ split₁ˡ)) ⟩∘⟨refl ⟩ - f † ∘ λ⇒ ∘ ! ⊕₁ (g † ∘ (λ⇒ ∘ ! ⊕₁ id) ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (pullˡ (refl⟩∘⟨ Equiv.sym p₂-⊕)) ⟩∘⟨refl ⟩ - f † ∘ λ⇒ ∘ ! ⊕₁ ((g † ∘ p₂) ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ pushʳ (extendʳ (pushʳ serialize₁₂)) ⟩ - (f † ∘ (λ⇒ ∘ ! ⊕₁ id)) ∘ id ⊕₁ ((g † ∘ p₂) ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ (refl⟩∘⟨ p₂-⊕) ⟩∘⟨refl ⟨ - (f † ∘ p₂) ∘ id ⊕₁ ((g † ∘ p₂) ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ∎ + (g ∘ f) † ∘ π₂ ≈⟨ pushˡ †-homomorphism ⟩ + f † ∘ g † ∘ π₂ ≈⟨ refl⟩∘⟨ pushʳ (sym π₂∘first) ⟩ + f † ∘ (g † ∘ π₂) ∘ f ×₁ id ≈⟨ pushʳ (sym project₂) ⟩ + (f † ∘ π₂) ∘ ⟨ π₁ , (g † ∘ π₂) ∘ f ×₁ id ⟩ ∎ -- Contravariant functor from underlying category to BWD Pull : Functor op BWD @@ -93,33 +76,17 @@ Pull = record ; F-resp-≈ = λ f≈g → (f≈g ⟩∘⟨refl) ⌸ ⟨ f≈g ⟩† } where - open IdempotentSemiadditiveDagger S - using (+-monoidal; _†; p₂; _⊕₁_; △; !; p₁; p₂-⊕; ⇒!; ⇒△; ρ⇒≈p₁; p₁∘△; †-homomorphism; †-identity; ⟨_⟩†) - open Monoidal +-monoidal using (assoc-commute-from; unitorˡ-commute-from; triangle) - open Shorthands +-monoidal using (α⇒; λ⇒; ρ⇒) - open ⇒-Reasoning 𝒞 - open ⊗-Reasoning +-monoidal + open SemiadditiveDagger S + open HomReasoning + open ⇒-Reasoning + open Equiv homoᵢ : {A B C : Obj} (f : B ⇒ A) (g : C ⇒ B) - → (f ∘ g) ∘ p₂ - ≈ (f ∘ p₂) ∘ id ⊕₁ ((g ∘ p₂) ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + → (f ∘ g) ∘ π₂ + ≈ (f ∘ π₂) ∘ ⟨ π₁ , (g ∘ π₂) ∘ (f †) ×₁ id ⟩ homoᵢ f g = begin - (f ∘ g) ∘ p₂ ≈⟨ pullʳ (refl⟩∘⟨ p₂-⊕) ⟩ - f ∘ g ∘ λ⇒ ∘ ! ⊕₁ id ≈⟨ refl⟩∘⟨ extendʳ unitorˡ-commute-from ⟨ - f ∘ λ⇒ ∘ id ⊕₁ g ∘ ! ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ insertˡ p₁∘△ ⟩⊗⟨refl ⟩ - f ∘ λ⇒ ∘ id ⊕₁ g ∘ (p₁ ∘ △ ∘ !) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (ρ⇒≈p₁ ⟩∘⟨refl) ⟩⊗⟨refl ⟨ - f ∘ λ⇒ ∘ id ⊕₁ g ∘ (ρ⇒ ∘ △ ∘ !) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ˡ ⟩ - f ∘ λ⇒ ∘ id ⊕₁ g ∘ ρ⇒ ⊕₁ id ∘ (△ ∘ !) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⇒△ ⟩⊗⟨refl ⟩ - f ∘ λ⇒ ∘ id ⊕₁ g ∘ ρ⇒ ⊕₁ id ∘ (! ⊕₁ ! ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ˡ ⟩ - f ∘ λ⇒ ∘ id ⊕₁ g ∘ ρ⇒ ⊕₁ id ∘ (! ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (Equiv.sym triangle) ⟩ - f ∘ λ⇒ ∘ id ⊕₁ g ∘ id ⊕₁ λ⇒ ∘ α⇒ ∘ (! ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩ - f ∘ λ⇒ ∘ id ⊕₁ (g ∘ λ⇒) ∘ α⇒ ∘ (! ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟩ - f ∘ λ⇒ ∘ id ⊕₁ (g ∘ λ⇒) ∘ ! ⊕₁ ! ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩ - f ∘ λ⇒ ∘ ! ⊕₁ ((g ∘ λ⇒) ∘ ! ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (pullʳ (refl⟩∘⟨ (Equiv.sym ⇒! ⟩⊗⟨refl))) ⟩∘⟨refl ⟩ - f ∘ λ⇒ ∘ ! ⊕₁ (g ∘ λ⇒ ∘ (! ∘ f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ (pushʳ split₁ˡ)) ⟩∘⟨refl ⟩ - f ∘ λ⇒ ∘ ! ⊕₁ (g ∘ (λ⇒ ∘ ! ⊕₁ id) ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (pullˡ (refl⟩∘⟨ Equiv.sym p₂-⊕)) ⟩∘⟨refl ⟩ - f ∘ λ⇒ ∘ ! ⊕₁ ((g ∘ p₂) ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ pushʳ (extendʳ (pushʳ serialize₁₂)) ⟩ - (f ∘ (λ⇒ ∘ ! ⊕₁ id)) ∘ id ⊕₁ ((g ∘ p₂) ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ (refl⟩∘⟨ p₂-⊕) ⟩∘⟨refl ⟨ - (f ∘ p₂) ∘ id ⊕₁ ((g ∘ p₂) ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ∎ + (f ∘ g) ∘ π₂ ≈⟨ pullʳ (pushʳ (sym π₂∘first)) ⟩ + f ∘ (g ∘ π₂) ∘ (f †) ×₁ id ≈⟨ pushʳ (sym project₂) ⟩ + (f ∘ π₂) ∘ ⟨ π₁ , (g ∘ π₂) ∘ (f †) ×₁ id ⟩ ∎ diff --git a/Data/WiringDiagram/Core.agda b/Data/WiringDiagram/Core.agda index 9903ce5..76ab70a 100644 --- a/Data/WiringDiagram/Core.agda +++ b/Data/WiringDiagram/Core.agda @@ -1,21 +1,19 @@ {-# OPTIONS --without-K --safe #-} open import Categories.Category using (Category) +open import Category.Dagger.Semiadditive using (SemiadditiveDagger) open import Level using (Level) -open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger) module Data.WiringDiagram.Core {o ℓ e : Level} {𝒞 : Category o ℓ e} - (S : IdempotentSemiadditiveDagger 𝒞) + (S : SemiadditiveDagger 𝒞) where -open import Categories.Category.Monoidal.Utilities using (module Shorthands) open import Relation.Binary using (IsEquivalence) open Category 𝒞 using (Obj; _∘_; _⇒_; id; _≈_; module Equiv) -open IdempotentSemiadditiveDagger S using (_⊕₀_; _⊕₁_; p₂; +-monoidal; △; ▽; _†) -open Shorthands +-monoidal using (α⇒) +open SemiadditiveDagger S using (_⊕_; _×₁_; π₁; π₂; Δ; ∇; _†; ⟨_,_⟩) -- A "Box" is a pair of objects from the underlying category, -- representing input and output ports @@ -68,7 +66,7 @@ record WiringDiagram (A B : Box) : Set ℓ where module B = Box B field - input : A.ₒ ⊕₀ B.ᵢ ⇒ A.ᵢ + input : A.ₒ ⊕ B.ᵢ ⇒ A.ᵢ output : A.ₒ ⇒ B.ₒ infix 4 _⧈_ @@ -114,24 +112,24 @@ module _ {A B : Box} where -- The identity wiring diagram id-⧈ : {A : Box} → WiringDiagram A A -id-⧈ = p₂ ⧈ id +id-⧈ = π₂ ⧈ id -- Composition of wiring diagrams _⌻_ : {A B C : Box} → WiringDiagram B C → WiringDiagram A B → WiringDiagram A C -_⌻_ {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {Cᵢ □ Cₒ} (f′ ⧈ g′) (f ⧈ g) = f″ ⧈ g′ ∘ g +_⌻_ {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {Cᵢ □ Cₒ} (f ⧈ g) (h ⧈ i) = hfi ⧈ g ∘ i where - f″ : Aₒ ⊕₀ Cᵢ ⇒ Aᵢ - f″ = f ∘ id ⊕₁ (f′ ∘ g ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + hfi : Aₒ ⊕ Cᵢ ⇒ Aᵢ + hfi = h ∘ ⟨ π₁ , f ∘ i ×₁ id ⟩ infixr 9 _⌻_ -- Special wiring diagrams loop : {A : Obj} → WiringDiagram (A □ A) (A □ A) -loop = ▽ ⧈ id +loop = ∇ ⧈ id pulsh : {A B C D : Obj} → A ⇒ B → C ⇒ D → WiringDiagram (B □ C) (A □ D) -pulsh f g = f ∘ p₂ ⧈ g +pulsh f g = f ∘ π₂ ⧈ g push : {A B : Obj} → A ⇒ B → WiringDiagram (A □ A) (B □ B) push f = pulsh (f †) f @@ -140,7 +138,7 @@ pull : {A B : Obj} → A ⇒ B → WiringDiagram (B □ B) (A □ A) pull f = pulsh f (f †) merge : {A B : Obj} → A ⇒ B → WiringDiagram (A □ A) (B □ B) -merge f = f † ∘ ▽ ∘ f ⊕₁ id ⧈ f +merge f = f † ∘ ∇ ∘ f ×₁ id ⧈ f split : {A B : Obj} → A ⇒ B → WiringDiagram (B □ B) (A □ A) -split f = ▽ ∘ id ⊕₁ f ⧈ f † +split f = ∇ ∘ id ×₁ f ⧈ f † diff --git a/Data/WiringDiagram/Directed.agda b/Data/WiringDiagram/Directed.agda index f1cbb93..f6fcc4e 100644 --- a/Data/WiringDiagram/Directed.agda +++ b/Data/WiringDiagram/Directed.agda @@ -1,18 +1,16 @@ {-# OPTIONS --without-K --safe #-} open import Categories.Category using (Category) -open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger) +open import Category.Dagger.Semiadditive using (SemiadditiveDagger) open import Level using (Level) module Data.WiringDiagram.Directed {o ℓ e : Level} {𝒞 : Category o ℓ e} - (S : IdempotentSemiadditiveDagger 𝒞) + (S : SemiadditiveDagger 𝒞) where -import Categories.Category.Monoidal.Properties as ⊗-Properties -import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning -import Categories.Morphism.Reasoning as ⇒-Reasoning +import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning open import Categories.Category.Helper using (categoryHelper) open import Categories.Category.Monoidal using (Monoidal) @@ -22,153 +20,54 @@ open import Data.Product using (_,_) open import Data.WiringDiagram.Core S using (Box; WiringDiagram; _≈-⧈_; _□_; _⧈_; _⌸_; id-⧈; _⌻_; ≈-isEquiv; pulsh) open Category 𝒞 -open IdempotentSemiadditiveDagger S -open Monoidal +-monoidal -open Shorthands +-monoidal using (α⇒; α⇐; λ⇒; λ⇐; ρ⇒; ρ⇐) -open ⊗-Properties +-monoidal using (coherence₁) +open SemiadditiveDagger S private ⌻-resp-≈ : {A B C : Box} {f h : WiringDiagram B C} {g i : WiringDiagram A B} → f ≈-⧈ h → g ≈-⧈ i → f ⌻ g ≈-⧈ h ⌻ i ⌻-resp-≈ {A} {B} {C} {fᵢ ⧈ fₒ} {hᵢ ⧈ hₒ} {gᵢ ⧈ gₒ} {iᵢ ⧈ iₒ} (fᵢ≈hᵢ ⌸ fₒ≈hₒ) (gᵢ≈iᵢ ⌸ gₒ≈iₒ) = ≈ᵢ ⌸ ∘-resp-≈ fₒ≈hₒ gₒ≈iₒ where - open ⊗-Reasoning +-monoidal - ≈ᵢ : gᵢ ∘ id ⊕₁ (fᵢ ∘ gₒ ⊕₁ id) ∘ α⇒ ∘ △ {Box.ₒ A} ⊕₁ id - ≈ iᵢ ∘ id ⊕₁ (hᵢ ∘ iₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id - ≈ᵢ = gᵢ≈iᵢ ⟩∘⟨ refl⟩⊗⟨ (fᵢ≈hᵢ ⟩∘⟨ gₒ≈iₒ ⟩⊗⟨refl) ⟩∘⟨refl + open HomReasoning + ≈ᵢ : gᵢ ∘ ⟨ π₁ , fᵢ ∘ gₒ ×₁ id ⟩ + ≈ iᵢ ∘ ⟨ π₁ , hᵢ ∘ iₒ ×₁ id ⟩ + ≈ᵢ = gᵢ≈iᵢ ⟩∘⟨ ⟨⟩-congˡ (fᵢ≈hᵢ ⟩∘⟨ first-cong gₒ≈iₒ) ⌻-assoc : {A B C D : Box} {f : WiringDiagram A B} {g : WiringDiagram B C} {h : WiringDiagram C D} → (h ⌻ g) ⌻ f ≈-⧈ h ⌻ (g ⌻ f) ⌻-assoc {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {Cᵢ □ Cₒ} {Dᵢ □ Dₒ} {fᵢ ⧈ fₒ} {gᵢ ⧈ gₒ} {hᵢ ⧈ hₒ} = ≈ᵢ ⌸ assoc where - open ⊗-Reasoning +-monoidal - - term₁ : Aₒ ⊕₀ Dᵢ ⇒ Cᵢ - term₁ = hᵢ ∘ (gₒ ∘ fₒ) ⊕₁ id - - term₂ : Bₒ ⊕₀ Dᵢ ⇒ Cᵢ - term₂ = hᵢ ∘ gₒ ⊕₁ id - - term₃ : Aₒ ⊕₀ Cᵢ ⇒ Bᵢ - term₃ = gᵢ ∘ fₒ ⊕₁ id - open ⇒-Reasoning 𝒞 - - lemma₁ : α⇒ {Aₒ ⊕₀ Aₒ} {Aₒ} {Dᵢ} ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id ≈ △ ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id - lemma₁ = begin - α⇒ ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩ - α⇒ ∘ α⇐ ⊕₁ id ∘ (id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ˡ ⟩ - α⇒ ∘ α⇐ ⊕₁ id ∘ (id ⊕₁ △ ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ △-assoc ⟩⊗⟨refl ⟩ - α⇒ ∘ α⇐ ⊕₁ id ∘ (α⇒ ∘ △ ⊕₁ id ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ merge₁ʳ ⟩ - α⇒ ∘ (α⇐ ∘ α⇒ ∘ △ ⊕₁ id ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ cancelˡ associator.isoˡ ⟩⊗⟨refl ⟩ - α⇒ ∘ (△ ⊕₁ id ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ split₁ˡ ⟩ - α⇒ ∘ (△ ⊕₁ id) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ extendʳ assoc-commute-from ⟩ - △ ⊕₁ id ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩⊗⟨ ⊕.identity ⟩∘⟨refl ⟩ - △ ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ∎ - - lemma₂ : △ ⊕₁ id {Dᵢ} ∘ fₒ ⊕₁ id ≈ (fₒ ⊕₁ fₒ) ⊕₁ id ∘ △ ⊕₁ id - lemma₂ = begin - △ ⊕₁ id ∘ fₒ ⊕₁ id ≈⟨ merge₁ʳ ⟩ - (△ ∘ fₒ) ⊕₁ id ≈⟨ ⇒△ ⟩⊗⟨refl ⟩ - (fₒ ⊕₁ fₒ ∘ △) ⊕₁ id ≈⟨ split₁ʳ ⟩ - (fₒ ⊕₁ fₒ) ⊕₁ id ∘ △ ⊕₁ id ∎ - - ≈ᵢ : fᵢ ∘ id ⊕₁ ((gᵢ ∘ id ⊕₁ (hᵢ ∘ gₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id) ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id - ≈ (fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ (hᵢ ∘ (gₒ ∘ fₒ) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + open HomReasoning + open ⇒-Reasoning + open Equiv + ≈ᵢ : fᵢ ∘ ⟨ π₁ , (gᵢ ∘ ⟨ π₁ , hᵢ ∘ gₒ ×₁ id ⟩) ∘ fₒ ×₁ id ⟩ + ≈ (fᵢ ∘ ⟨ π₁ , gᵢ ∘ fₒ ×₁ id ⟩) ∘ ⟨ π₁ , hᵢ ∘ (gₒ ∘ fₒ) ×₁ id ⟩ ≈ᵢ = begin - fᵢ ∘ id ⊕₁ ((gᵢ ∘ id ⊕₁ term₂ ∘ α⇒ ∘ △ ⊕₁ id) ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendˡ (extendˡ assoc) ⟩∘⟨refl ⟩ - fᵢ ∘ id ⊕₁ ((gᵢ ∘ id ⊕₁ term₂ ∘ α⇒) ∘ △ ⊕₁ id ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ lemma₂) ⟩∘⟨refl ⟩ - fᵢ ∘ id ⊕₁ ((gᵢ ∘ id ⊕₁ term₂ ∘ α⇒) ∘ (fₒ ⊕₁ fₒ) ⊕₁ id ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendˡ assoc ⟩∘⟨refl ⟩ - fᵢ ∘ id ⊕₁ ((gᵢ ∘ id ⊕₁ term₂) ∘ α⇒ ∘ (fₒ ⊕₁ fₒ) ⊕₁ id ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ extendʳ assoc-commute-from ) ⟩∘⟨refl ⟩ - fᵢ ∘ id ⊕₁ ((gᵢ ∘ id ⊕₁ term₂) ∘ fₒ ⊕₁ fₒ ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ assoc ⟩∘⟨refl ⟩ - fᵢ ∘ id ⊕₁ (gᵢ ∘ id ⊕₁ term₂ ∘ fₒ ⊕₁ fₒ ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ pullˡ merge₂ˡ ) ⟩∘⟨refl ⟩ - fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ (term₂ ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ refl⟩⊗⟨ pullʳ merge₁ʳ ⟩∘⟨refl) ⟩∘⟨refl ⟩ - fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁ ∘ α⇒ ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ assoc ⟩∘⟨refl ⟨ - fᵢ ∘ id ⊕₁ ((gᵢ ∘ fₒ ⊕₁ term₁) ∘ α⇒ ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendˡ assoc ⟩∘⟨refl ⟨ - fᵢ ∘ id ⊕₁ ((gᵢ ∘ fₒ ⊕₁ term₁ ∘ α⇒) ∘ △ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩ - fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁ ∘ α⇒) ∘ id ⊕₁ △ ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨ - fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁ ∘ α⇒) ∘ α⇒ ∘ (id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ extendʳ (refl⟩⊗⟨ assoc ⟩∘⟨refl) ⟨ - fᵢ ∘ id ⊕₁ ((gᵢ ∘ fₒ ⊕₁ term₁) ∘ α⇒) ∘ α⇒ ∘ (id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩ - fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁) ∘ id ⊕₁ α⇒ ∘ α⇒ ∘ (id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ insertˡ associator.isoʳ ⟩⊗⟨refl ⟩∘⟨refl ⟩ - fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁) ∘ id ⊕₁ α⇒ ∘ α⇒ ∘ (α⇒ ∘ α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ʳ ⟩ - fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁) ∘ id ⊕₁ α⇒ ∘ α⇒ ∘ α⇒ ⊕₁ id ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟨ - fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁) ∘ id ⊕₁ α⇒ ∘ (α⇒ ∘ α⇒ ⊕₁ id) ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ pentagon ⟩ - fᵢ ∘ id ⊕₁ (gᵢ ∘ fₒ ⊕₁ term₁) ∘ α⇒ ∘ α⇒ ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ pushʳ serialize₁₂ ⟩∘⟨refl ⟩ - fᵢ ∘ id ⊕₁ (term₃ ∘ id ⊕₁ term₁) ∘ α⇒ ∘ α⇒ ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩ - fᵢ ∘ id ⊕₁ term₃ ∘ id ⊕₁ id ⊕₁ term₁ ∘ α⇒ ∘ α⇒ ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨ - fᵢ ∘ id ⊕₁ term₃ ∘ α⇒ ∘ (id ⊕₁ id) ⊕₁ term₁ ∘ α⇒ ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊕.identity ⟩⊗⟨refl ⟩∘⟨refl ⟩ - fᵢ ∘ id ⊕₁ term₃ ∘ α⇒ ∘ id ⊕₁ term₁ ∘ α⇒ ∘ (α⇐ ∘ id ⊕₁ △) ⊕₁ id ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ lemma₁ ⟩ - fᵢ ∘ id ⊕₁ term₃ ∘ α⇒ ∘ id ⊕₁ term₁ ∘ △ ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (Equiv.sym serialize₂₁ ○ serialize₁₂) ⟩ - fᵢ ∘ id ⊕₁ term₃ ∘ α⇒ ∘ △ ⊕₁ id ∘ id ⊕₁ term₁ ∘ α⇒ ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟨ - fᵢ ∘ id ⊕₁ term₃ ∘ (α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ term₁ ∘ α⇒ ∘ △ ⊕₁ id - ≈⟨ refl⟩∘⟨ assoc ⟨ - fᵢ ∘ (id ⊕₁ term₃ ∘ α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ term₁ ∘ α⇒ ∘ △ ⊕₁ id - ≈⟨ assoc ⟨ - (fᵢ ∘ id ⊕₁ term₃ ∘ α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ term₁ ∘ α⇒ ∘ △ ⊕₁ id ∎ + fᵢ ∘ ⟨ π₁ , (gᵢ ∘ ⟨ π₁ , hᵢ ∘ gₒ ×₁ id ⟩) ∘ fₒ ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (pullʳ ⟨⟩∘) ⟩ + fᵢ ∘ ⟨ π₁ , gᵢ ∘ ⟨ π₁ ∘ fₒ ×₁ id , (hᵢ ∘ gₒ ×₁ id) ∘ fₒ ×₁ id ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (refl⟩∘⟨ ⟨⟩-cong₂ π₁∘×₁ (pullʳ first∘first)) ⟩ + fᵢ ∘ ⟨ π₁ , gᵢ ∘ ⟨ fₒ ∘ π₁ , hᵢ ∘ (gₒ ∘ fₒ) ×₁ id ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ project₁ (pullʳ first∘⟨⟩) ⟨ + fᵢ ∘ ⟨ π₁ ∘ ⟨ π₁ , _ ⟩ , (gᵢ ∘ fₒ ×₁ id) ∘ ⟨ π₁ , _ ⟩ ⟩ ≈⟨ pushʳ (sym ⟨⟩∘) ⟩ + (fᵢ ∘ ⟨ π₁ , gᵢ ∘ fₒ ×₁ id ⟩) ∘ ⟨ π₁ , hᵢ ∘ (gₒ ∘ fₒ) ×₁ id ⟩ ∎ ⌻-identityˡ : {A B : Box} {f : WiringDiagram A B} → id-⧈ ⌻ f ≈-⧈ f ⌻-identityˡ {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {fᵢ ⧈ fₒ} = ≈ᵢ ⌸ identityˡ where - open ⇒-Reasoning 𝒞 - open ⊗-Reasoning +-monoidal - ≈ᵢ : fᵢ ∘ id ⊕₁ (p₂ ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈ fᵢ + open HomReasoning + open ⇒-Reasoning + ≈ᵢ : fᵢ ∘ ⟨ π₁ , π₂ ∘ fₒ ×₁ id ⟩ ≈ fᵢ ≈ᵢ = begin - fᵢ ∘ id ⊕₁ (p₂ ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (p₂-⊕ ⟩∘⟨refl) ⟩∘⟨refl ⟩ - fᵢ ∘ id ⊕₁ ((λ⇒ ∘ ! ⊕₁ id) ∘ fₒ ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ pullʳ merge₁ʳ ⟩∘⟨refl ⟩ - fᵢ ∘ id ⊕₁ (λ⇒ ∘ (! ∘ fₒ) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ ⇒! ⟩⊗⟨refl) ⟩∘⟨refl ⟩ - fᵢ ∘ id ⊕₁ (λ⇒ ∘ ! ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩ - fᵢ ∘ id ⊕₁ λ⇒ ∘ id ⊕₁ ! ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨ - fᵢ ∘ id ⊕₁ λ⇒ ∘ α⇒ ∘ (id ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ˡ ⟩ - fᵢ ∘ id ⊕₁ λ⇒ ∘ α⇒ ∘ (id ⊕₁ ! ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ pullˡ triangle ⟩ - fᵢ ∘ ρ⇒ ⊕₁ id ∘ (id ⊕₁ ! ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ merge₁ʳ ⟩ - fᵢ ∘ (ρ⇒ ∘ id ⊕₁ ! ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ △-identityʳ ) ⟩⊗⟨refl ⟩ - fᵢ ∘ (ρ⇒ ∘ ρ⇐) ⊕₁ id ≈⟨ refl⟩∘⟨ unitorʳ.isoʳ ⟩⊗⟨refl ⟩ - fᵢ ∘ id ⊕₁ id ≈⟨ elimʳ ⊕.identity ⟩ - fᵢ ∎ + fᵢ ∘ ⟨ π₁ , π₂ ∘ fₒ ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ π₂∘first ⟩ + fᵢ ∘ ⟨ π₁ , π₂ ⟩ ≈⟨ elimʳ η ⟩ + fᵢ ∎ ⌻-identityʳ : {A B : Box} {f : WiringDiagram A B} → f ⌻ id-⧈ ≈-⧈ f ⌻-identityʳ {Aᵢ □ Aₒ} {Bᵢ □ Bₒ} {fᵢ ⧈ fₒ} = ≈ᵢ ⌸ identityʳ where - open ⇒-Reasoning 𝒞 - open ⊗-Reasoning +-monoidal - ≈ᵢ : p₂ ∘ id ⊕₁ (fᵢ ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈ fᵢ + open HomReasoning + open ⇒-Reasoning + ≈ᵢ : π₂ ∘ ⟨ π₁ , fᵢ ∘ id ×₁ id ⟩ ≈ fᵢ ≈ᵢ = begin - p₂ ∘ id ⊕₁ (fᵢ ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ p₂-⊕ ⟩∘⟨refl ⟩ - (λ⇒ ∘ ! ⊕₁ id) ∘ id ⊕₁ (fᵢ ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ elimʳ ⊕.identity ⟩∘⟨refl ⟩ - (λ⇒ ∘ ! ⊕₁ id) ∘ id ⊕₁ fᵢ ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ pullˡ (pullʳ (Equiv.sym serialize₁₂)) ⟩ - (λ⇒ ∘ ! ⊕₁ fᵢ) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ pullʳ (pushˡ serialize₂₁) ⟩ - λ⇒ ∘ id ⊕₁ fᵢ ∘ ! ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ ⊕.identity ⟩∘⟨refl ⟨ - λ⇒ ∘ id ⊕₁ fᵢ ∘ ! ⊕₁ id ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨ - λ⇒ ∘ id ⊕₁ fᵢ ∘ α⇒ ∘ (! ⊕₁ id) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ʳ ⟩ - λ⇒ ∘ id ⊕₁ fᵢ ∘ α⇒ ∘ (! ⊕₁ id ∘ △) ⊕₁ id ≈⟨ extendʳ unitorˡ-commute-from ⟩ - fᵢ ∘ λ⇒ ∘ α⇒ ∘ (! ⊕₁ id ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ △-identityˡ ⟩⊗⟨refl ⟩ - fᵢ ∘ λ⇒ ∘ α⇒ ∘ λ⇐ ⊕₁ id ≈⟨ refl⟩∘⟨ pullˡ coherence₁ ⟩ - fᵢ ∘ λ⇒ ⊕₁ id ∘ λ⇐ ⊕₁ id ≈⟨ refl⟩∘⟨ merge₁ʳ ⟩ - fᵢ ∘ (λ⇒ ∘ λ⇐) ⊕₁ id ≈⟨ refl⟩∘⟨ unitorˡ.isoʳ ⟩⊗⟨refl ⟩ - fᵢ ∘ id ⊕₁ id ≈⟨ elimʳ ⊕.identity ⟩ - fᵢ ∎ + π₂ ∘ ⟨ π₁ , fᵢ ∘ id ×₁ id ⟩ ≈⟨ project₂ ⟩ + fᵢ ∘ id ×₁ id ≈⟨ elimʳ id×₁id ⟩ + fᵢ ∎ -- The category of directed wiring diagrams DWD : Category o ℓ e @@ -195,26 +94,13 @@ Pulsh = record ; F-resp-≈ = λ (f≈f′ , g≈g′) → (f≈f′ ⟩∘⟨refl) ⌸ g≈g′ } where - open ⇒-Reasoning 𝒞 - open ⊗-Reasoning +-monoidal - homoᵢ : {A B C D E F : Obj} (g : A ⇒ B) (g′ : B ⇒ C) (f : E ⇒ F) (f′ : D ⇒ E) - → (f ∘ f′) ∘ p₂ - ≈ (f ∘ p₂) ∘ (id ⊕₁ ((f′ ∘ p₂) ∘ g ⊕₁ id)) ∘ α⇒ ∘ (△ ⊕₁ id) + open HomReasoning + open ⇒-Reasoning + open Equiv + homoᵢ + : {A B C D E F : Obj} (g : A ⇒ B) (g′ : B ⇒ C) (f : E ⇒ F) (f′ : D ⇒ E) + → (f ∘ f′) ∘ π₂ ≈ (f ∘ π₂) ∘ ⟨ π₁ , (f′ ∘ π₂) ∘ g ×₁ id ⟩ homoᵢ g g′ f f′ = begin - (f ∘ f′) ∘ p₂ ≈⟨ refl⟩∘⟨ p₂-⊕ ⟩ - (f ∘ f′) ∘ λ⇒ ∘ ! ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ insertˡ p₁∘△ ⟩⊗⟨refl ⟩ - (f ∘ f′) ∘ λ⇒ ∘ (p₁ ∘ △ ∘ !) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (ρ⇒≈p₁ ⟩∘⟨refl) ⟩⊗⟨refl ⟨ - (f ∘ f′) ∘ λ⇒ ∘ (ρ⇒ ∘ △ ∘ !) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ ⇒△) ⟩⊗⟨refl ⟩ - (f ∘ f′) ∘ λ⇒ ∘ (ρ⇒ ∘ ! ⊕₁ ! ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ʳ ⟩ - (f ∘ f′) ∘ λ⇒ ∘ ρ⇒ ⊕₁ id ∘ (! ⊕₁ ! ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ʳ ⟩ - (f ∘ f′) ∘ λ⇒ ∘ ρ⇒ ⊕₁ id ∘ (! ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (Equiv.sym triangle) ⟩ - (f ∘ f′) ∘ λ⇒ ∘ id ⊕₁ λ⇒ ∘ α⇒ ∘ (! ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟩ - (f ∘ f′) ∘ λ⇒ ∘ id ⊕₁ λ⇒ ∘ ! ⊕₁ ! ⊕₁ id ∘ α⇒ ∘ (△ ⊕₁ id) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩ - (f ∘ f′) ∘ λ⇒ ∘ ! ⊕₁ (λ⇒ ∘ ! ⊕₁ id) ∘ α⇒ ∘ (△ ⊕₁ id) ≈⟨ pullʳ (extendʳ (Equiv.sym unitorˡ-commute-from)) ⟩ - f ∘ λ⇒ ∘ id ⊕₁ f′ ∘ ! ⊕₁ (λ⇒ ∘ ! ⊕₁ id) ∘ α⇒ ∘ (△ ⊕₁ id) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩ - f ∘ λ⇒ ∘ ! ⊕₁ (f′ ∘ λ⇒ ∘ ! ⊕₁ id) ∘ α⇒ ∘ (△ ⊕₁ id) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ refl⟩∘⟨ ⇒! ⟩⊗⟨refl) ⟩∘⟨refl ⟨ - f ∘ λ⇒ ∘ ! ⊕₁ (f′ ∘ λ⇒ ∘ (! ∘ g) ⊕₁ id) ∘ α⇒ ∘ (△ ⊕₁ id) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ pushʳ split₁ˡ) ⟩∘⟨refl ⟩ - f ∘ λ⇒ ∘ ! ⊕₁ (f′ ∘ (λ⇒ ∘ ! ⊕₁ id) ∘ g ⊕₁ id) ∘ α⇒ ∘ (△ ⊕₁ id) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ pushˡ (refl⟩∘⟨ p₂-⊕) ⟩∘⟨refl ⟨ - f ∘ λ⇒ ∘ ! ⊕₁ ((f′ ∘ p₂) ∘ g ⊕₁ id) ∘ α⇒ ∘ (△ ⊕₁ id) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₁₂ ⟩ - f ∘ λ⇒ ∘ ! ⊕₁ id ∘ (id ⊕₁ ((f′ ∘ p₂) ∘ g ⊕₁ id)) ∘ α⇒ ∘ (△ ⊕₁ id) ≈⟨ pushʳ (pullˡ (Equiv.sym p₂-⊕)) ⟩ - (f ∘ p₂) ∘ (id ⊕₁ ((f′ ∘ p₂) ∘ g ⊕₁ id)) ∘ α⇒ ∘ (△ ⊕₁ id) ∎ + (f ∘ f′) ∘ π₂ ≈⟨ pullʳ (pushʳ (sym π₂∘first)) ⟩ + f ∘ (f′ ∘ π₂) ∘ g ×₁ id ≈⟨ pushʳ (sym project₂) ⟩ + (f ∘ π₂) ∘ ⟨ π₁ , (f′ ∘ π₂) ∘ g ×₁ id ⟩ ∎ diff --git a/Data/WiringDiagram/Equalities.agda b/Data/WiringDiagram/Equalities.agda index 1e5eb47..61deee4 100644 --- a/Data/WiringDiagram/Equalities.agda +++ b/Data/WiringDiagram/Equalities.agda @@ -1,150 +1,111 @@ {-# OPTIONS --without-K --safe #-} open import Categories.Category using (Category) -open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger) +open import Category.Dagger.Semiadditive using (SemiadditiveDagger; IdempotentSemiadditiveDagger) open import Level using (Level) module Data.WiringDiagram.Equalities {o ℓ e : Level} {𝒞 : Category o ℓ e} (S : IdempotentSemiadditiveDagger 𝒞) where -import Categories.Category.Monoidal.Properties as ⊗-Properties -import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning -import Categories.Morphism.Reasoning as ⇒-Reasoning +module S = IdempotentSemiadditiveDagger S + +import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning open import Categories.Category.Monoidal using (module Monoidal) open import Categories.Category.Monoidal.Utilities using (module Shorthands) -open import Data.WiringDiagram.Core S using (_⌸_; _⌻_; _≈-⧈_; ≈-trans; loop; push; pull; merge; split) +open import Data.WiringDiagram.Core S.semiadditiveDagger using (_⌸_; _⌻_; _≈-⧈_; ≈-trans; loop; push; pull; merge; split) open Category 𝒞 + +open Equiv +open HomReasoning open IdempotentSemiadditiveDagger S -open Monoidal +-monoidal using (module unitorˡ; module unitorʳ; triangle; assoc-commute-from; unitorˡ-commute-from) -open Shorthands +-monoidal using (α⇒; α⇐; λ⇒; λ⇐; ρ⇒; ρ⇐) -open ⊗-Properties +-monoidal using (coherence₁) +open ⇒-Reasoning + +⟨π₁,id⟩ : {A B : Obj} → ⟨ π₁ {A} {B} , id ⟩ ≈ assocˡ ∘ Δ ×₁ id +⟨π₁,id⟩ = begin + ⟨ π₁ , id ⟩ ≈⟨ ⟨⟩-congˡ η ⟨ + ⟨ π₁ , ⟨ π₁ , π₂ ⟩ ⟩ ≈⟨ assocˡ∘⟨⟩ ⟨ + assocˡ ∘ ⟨ ⟨ π₁ , π₁ ⟩ , π₂ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ Δ∘ identityˡ ⟨ + assocˡ ∘ Δ ×₁ id ∎ loop∘loop : {A : Obj} → loop ⌻ loop ≈-⧈ loop {A} loop∘loop {A} = ≈ᵢ ⌸ identity² where - open ⇒-Reasoning 𝒞 - open ⊗-Reasoning +-monoidal - ≈ᵢ : ▽ ∘ id ⊕₁ (▽ ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈ ▽ + ≈ᵢ : ∇ ∘ ⟨ π₁ , (∇ ∘ id ×₁ id) ⟩ ≈ ∇ ≈ᵢ = begin - ▽ ∘ id ⊕₁ (▽ ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ elimʳ ⊕.identity ⟩∘⟨refl ⟩ - ▽ ∘ id ⊕₁ ▽ ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ assoc ⟨ - ▽ ∘ (id ⊕₁ ▽ ∘ α⇒) ∘ △ ⊕₁ id ≈⟨ extendʳ ▽-assoc ⟨ - ▽ ∘ ▽ ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ merge₁ˡ ⟩ - ▽ ∘ (▽ ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ ▽∘△ ⟩⊗⟨refl ⟩ - ▽ ∘ id ⊕₁ id ≈⟨ elimʳ ⊕.identity ⟩ - ▽ ∎ + ∇ ∘ ⟨ π₁ , ∇ ∘ id ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (sym identityˡ) (refl⟩∘⟨ id×₁id) ⟩ + ∇ ∘ ⟨ id ∘ π₁ , ∇ ∘ id ⟩ ≈⟨ refl⟩∘⟨ ×₁∘⟨⟩ ⟨ + ∇ ∘ id ×₁ ∇ ∘ ⟨ π₁ , id ⟩ ≈⟨ refl⟩∘⟨ pushʳ ⟨π₁,id⟩ ⟩ + ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ Δ ×₁ id ≈⟨ extendʳ ∇-assoc-×₁ ⟨ + ∇ ∘ ∇ ×₁ id ∘ Δ ×₁ id ≈⟨ refl⟩∘⟨ first∘first ⟩ + ∇ ∘ (∇ ∘ Δ) ×₁ id ≈⟨ refl⟩∘⟨ first-cong ∇∘Δ ⟩ + ∇ ∘ id ×₁ id ≈⟨ elimʳ id×₁id ⟩ + ∇ ∎ loop∘push∘loop≈merge : {A B : Obj} (f : A ⇒ B) → id ≤ ((f †) ∘ f) → loop ⌻ push f ⌻ loop ≈-⧈ merge f loop∘push∘loop≈merge f id≤f†∘f = ≈ᵢ ⌸ (identityˡ ○ identityʳ) where - open ⇒-Reasoning 𝒞 - open ⊗-Reasoning +-monoidal - ≈ᵢ : (▽ ∘ (id ⊕₁ ((f † ∘ p₂) ∘ id ⊕₁ id)) ∘ α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ (▽ ∘ (f ∘ id) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id - ≈ f † ∘ ▽ ∘ f ⊕₁ id + ≈ᵢ : (∇ ∘ ⟨ π₁ , (f † ∘ π₂) ∘ id ×₁ id ⟩) ∘ ⟨ π₁ , ∇ ∘ (f ∘ id) ×₁ id ⟩ + ≈ f † ∘ ∇ ∘ f ×₁ id ≈ᵢ = begin - (▽ ∘ id ⊕₁ ((f † ∘ p₂) ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ (▽ ∘ (f ∘ id) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ (refl⟩∘⟨ refl⟩⊗⟨ elimʳ ⊕.identity ⟩∘⟨refl) ⟩∘⟨refl ⟩ - (▽ ∘ id ⊕₁ (f † ∘ p₂) ∘ α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ (▽ ∘ (f ∘ id) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ (identityʳ ⟩⊗⟨refl)) ⟩∘⟨refl ⟩ - (▽ ∘ id ⊕₁ (f † ∘ p₂) ∘ α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ (▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ pushˡ (refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ p₂-⊕) ⟩∘⟨refl) ⟩ - ▽ ∘ (id ⊕₁ (f † ∘ λ⇒ ∘ ! ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id) ∘ id ⊕₁ (▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ extendʳ (pullʳ (pullʳ (Equiv.sym serialize₁₂))) ⟩ - ▽ ∘ id ⊕₁ (f † ∘ λ⇒ ∘ ! ⊕₁ id) ∘ (α⇒ ∘ △ ⊕₁ (▽ ∘ f ⊕₁ id)) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩ - ▽ ∘ id ⊕₁ (f †) ∘ id ⊕₁ (λ⇒ ∘ ! ⊕₁ id) ∘ (α⇒ ∘ △ ⊕₁ (▽ ∘ f ⊕₁ id)) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩ - ▽ ∘ id ⊕₁ (f †) ∘ id ⊕₁ λ⇒ ∘ id ⊕₁ ! ⊕₁ id ∘ (α⇒ ∘ △ ⊕₁ (▽ ∘ f ⊕₁ id)) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (pullˡ (Equiv.sym assoc-commute-from)) ⟩ - ▽ ∘ id ⊕₁ (f †) ∘ id ⊕₁ λ⇒ ∘ (α⇒ ∘ (id ⊕₁ !) ⊕₁ id) ∘ △ ⊕₁ (▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (pullˡ triangle) ⟩ - ▽ ∘ id ⊕₁ (f †) ∘ ρ⇒ ⊕₁ id ∘ (id ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ (▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₁ˡ ⟩ - ▽ ∘ id ⊕₁ (f †) ∘ (ρ⇒ ∘ id ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ (▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₁ˡ ⟩ - ▽ ∘ id ⊕₁ (f †) ∘ ((ρ⇒ ∘ id ⊕₁ !) ∘ △) ⊕₁ (▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ △-identityʳ ⟩⊗⟨refl ⟩∘⟨refl ⟩ - ▽ ∘ id ⊕₁ (f †) ∘ (ρ⇒ ∘ ρ⇐) ⊕₁ (▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ unitorʳ.isoʳ ⟩⊗⟨refl ⟩∘⟨refl ⟩ - ▽ ∘ id ⊕₁ (f †) ∘ id ⊕₁ (▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩ - ▽ ∘ id ⊕₁ (f † ∘ ▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendʳ ⇒▽ ⟩∘⟨refl ⟩ - ▽ ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ (f †) ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ merge₁ʳ) ⟩∘⟨refl ⟩ - ▽ ∘ id ⊕₁ (▽ ∘ (f † ∘ f) ⊕₁ (f †)) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩ - ▽ ∘ id ⊕₁ ▽ ∘ id ⊕₁ (f † ∘ f) ⊕₁ (f †) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨ - ▽ ∘ id ⊕₁ ▽ ∘ α⇒ ∘ (id ⊕₁ (f † ∘ f)) ⊕₁ (f †) ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ʳ ⟩ - ▽ ∘ id ⊕₁ ▽ ∘ α⇒ ∘ (id ⊕₁ (f † ∘ f) ∘ △) ⊕₁ (f †) ≈⟨ refl⟩∘⟨ sym-assoc ⟩ - ▽ ∘ (id ⊕₁ ▽ ∘ α⇒) ∘ (id ⊕₁ (f † ∘ f) ∘ △) ⊕₁ (f †) ≈⟨ extendʳ ▽-assoc ⟨ - ▽ ∘ ▽ ⊕₁ id ∘ (id ⊕₁ (f † ∘ f) ∘ △) ⊕₁ (f †) ≈⟨ refl⟩∘⟨ merge₁ˡ ⟩ - ▽ ∘ (id + (f † ∘ f)) ⊕₁ (f †) ≈⟨ refl⟩∘⟨ id≤f†∘f ⟩⊗⟨refl ⟩ - ▽ ∘ (f † ∘ f) ⊕₁ (f †) ≈⟨ refl⟩∘⟨ split₁ʳ ⟩ - ▽ ∘ (f †) ⊕₁ (f †) ∘ f ⊕₁ id ≈⟨ extendʳ ⇒▽ ⟨ - f † ∘ ▽ ∘ f ⊕₁ id ∎ + (∇ ∘ ⟨ π₁ , (f † ∘ π₂) ∘ id ×₁ id ⟩) ∘ ⟨ π₁ , ∇ ∘ (f ∘ id) ×₁ id ⟩ ≈⟨ pullʳ (⟨⟩-congˡ (elimʳ id×₁id) ⟩∘⟨ ⟨⟩-congˡ (refl⟩∘⟨ first-cong identityʳ)) ⟩ + ∇ ∘ ⟨ π₁ , f † ∘ π₂ ⟩ ∘ ⟨ π₁ , ∇ ∘ f ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟩ + ∇ ∘ ⟨ π₁ ∘ ⟨ π₁ , ∇ ∘ f ×₁ id ⟩ , (f † ∘ π₂) ∘ ⟨ π₁ , ∇ ∘ f ×₁ id ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ project₁ (pullʳ project₂) ⟩ + ∇ ∘ ⟨ π₁ , f † ∘ ∇ ∘ f ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (extendʳ ⇒∇-×₁) ⟩ + ∇ ∘ ⟨ π₁ , ∇ ∘ (f †) ×₁ (f †) ∘ f ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (refl⟩∘⟨ ×₁∘first) ⟩ + ∇ ∘ ⟨ π₁ , ∇ ∘ (f † ∘ f) ×₁ (f †) ⟩ ≈⟨ refl⟩∘⟨ second∘⟨⟩ ⟨ + ∇ ∘ id ×₁ ∇ ∘ ⟨ π₁ , (f † ∘ f) ×₁ (f †) ⟩ ≈⟨ refl⟩∘⟨ pushʳ (sym assocˡ∘⟨⟩) ⟩ + ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ ⟨ π₁ , (f † ∘ f) ∘ π₁ ⟩ , f † ∘ π₂ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congʳ (⟨⟩-congʳ identityˡ) ⟨ + ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ ⟨ id ∘ π₁ , (f † ∘ f) ∘ π₁ ⟩ , f † ∘ π₂ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congʳ ⟨⟩∘ ⟨ + ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ ⟨ id , f † ∘ f ⟩ ×₁ (f †) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁-congʳ ×₁∘Δ ⟨ + ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ (id ×₁ (f † ∘ f) ∘ Δ) ×₁ (f †) ≈⟨ extendʳ ∇-assoc-×₁ ⟨ + ∇ ∘ (∇ ×₁ id) ∘ (id ×₁ (f † ∘ f) ∘ Δ) ×₁ (f †) ≈⟨ refl⟩∘⟨ first∘×₁ ⟩ + ∇ ∘ (id + (f † ∘ f)) ×₁ (f †) ≈⟨ refl⟩∘⟨ ×₁-congʳ id≤f†∘f ⟩ + ∇ ∘ (f † ∘ f) ×₁ (f †) ≈⟨ refl⟩∘⟨ ×₁∘first ⟨ + ∇ ∘ (f †) ×₁ (f †) ∘ f ×₁ id ≈⟨ extendʳ ⇒∇-×₁ ⟨ + f † ∘ ∇ ∘ f ×₁ id ∎ merge≈loop∘push : {A B : Obj} (f : A ⇒ B) → merge f ≈-⧈ loop ⌻ push f merge≈loop∘push f = ≈ᵢ ⌸ Equiv.sym identityˡ where - open ⇒-Reasoning 𝒞 - open ⊗-Reasoning +-monoidal - ≈ᵢ : f † ∘ ▽ ∘ f ⊕₁ id - ≈ (f † ∘ p₂) ∘ id ⊕₁ (▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + ≈ᵢ : f † ∘ ∇ ∘ f ×₁ id ≈ (f † ∘ π₂) ∘ ⟨ π₁ , ∇ ∘ f ×₁ id ⟩ ≈ᵢ = begin - f † ∘ ▽ ∘ f ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ introʳ unitorˡ.isoʳ ⟩⊗⟨refl ⟩ - f † ∘ ▽ ∘ (f ∘ λ⇒ ∘ λ⇐) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ refl⟩∘⟨ △-identityˡ ) ⟩⊗⟨refl ⟨ - f † ∘ ▽ ∘ (f ∘ λ⇒ ∘ ! ⊕₁ id ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ unitorˡ-commute-from ⟩⊗⟨refl ⟨ - f † ∘ ▽ ∘ (λ⇒ ∘ id ⊕₁ f ∘ ! ⊕₁ id ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ pullˡ (Equiv.sym serialize₂₁)) ⟩⊗⟨refl ⟩ - f † ∘ ▽ ∘ (λ⇒ ∘ ! ⊕₁ f ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ˡ ⟩ - f † ∘ ▽ ∘ λ⇒ ⊕₁ id ∘ (! ⊕₁ f ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ˡ ⟩ - f † ∘ ▽ ∘ λ⇒ ⊕₁ id ∘ (! ⊕₁ f) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (Equiv.sym coherence₁) ⟩ - f † ∘ ▽ ∘ λ⇒ ∘ α⇒ ∘ (! ⊕₁ f) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ extendʳ unitorˡ-commute-from ⟨ - f † ∘ λ⇒ ∘ id ⊕₁ ▽ ∘ α⇒ ∘ (! ⊕₁ f) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟩ - f † ∘ λ⇒ ∘ id ⊕₁ ▽ ∘ ! ⊕₁ f ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩ - f † ∘ λ⇒ ∘ ! ⊕₁ (▽ ∘ (f ⊕₁ id)) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩ - f † ∘ λ⇒ ∘ ! ⊕₁ ▽ ∘ id ⊕₁ f ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₁₂ ⟩ - f † ∘ λ⇒ ∘ ! ⊕₁ id ∘ id ⊕₁ ▽ ∘ id ⊕₁ f ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ pushʳ (pullˡ (Equiv.sym p₂-⊕)) ⟩ - (f † ∘ p₂) ∘ id ⊕₁ ▽ ∘ id ⊕₁ f ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩ - (f † ∘ p₂) ∘ id ⊕₁ (▽ ∘ f ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ∎ + f † ∘ ∇ ∘ f ×₁ id ≈⟨ pushʳ (sym project₂) ⟩ + (f † ∘ π₂) ∘ ⟨ π₁ , ∇ ∘ f ×₁ id ⟩ ∎ loop∘pull∘loop≈split : {A B : Obj} (f : A ⇒ B) → (f ∘ (f †)) ≤ id → loop ⌻ pull f ⌻ loop ≈-⧈ split f loop∘pull∘loop≈split f f∘f†≤id = ≈ᵢ ⌸ (identityˡ ○ identityʳ) where - open ⇒-Reasoning 𝒞 - open ⊗-Reasoning +-monoidal - ≈ᵢ : (▽ ∘ (id ⊕₁ ((f ∘ p₂) ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id)) ∘ id ⊕₁ (▽ ∘ (f † ∘ id) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id - ≈ ▽ ∘ id ⊕₁ f + ≈ᵢ : (∇ ∘ ⟨ π₁ , (f ∘ π₂) ∘ id ×₁ id ⟩) ∘ ⟨ π₁ , ∇ ∘ (f † ∘ id) ×₁ id ⟩ ≈ ∇ ∘ id ×₁ f ≈ᵢ = begin - (▽ ∘ (id ⊕₁ ((f ∘ p₂) ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id)) ∘ id ⊕₁ (▽ ∘ (f † ∘ id) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ (refl⟩∘⟨ refl⟩⊗⟨ elimʳ ⊕.identity ⟩∘⟨refl) ⟩∘⟨refl ⟩ - (▽ ∘ (id ⊕₁ (f ∘ p₂) ∘ α⇒ ∘ △ ⊕₁ id)) ∘ id ⊕₁ (▽ ∘ (f † ∘ id) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ pullʳ (pullʳ (pullʳ (refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ identityʳ ⟩⊗⟨refl) ⟩∘⟨refl)))⟩ - ▽ ∘ id ⊕₁ (f ∘ p₂) ∘ α⇒ ∘ △ ⊕₁ id ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩ - ▽ ∘ id ⊕₁ f ∘ id ⊕₁ p₂ ∘ α⇒ ∘ △ ⊕₁ id ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ p₂-⊕ ⟩∘⟨refl ⟩ - ▽ ∘ id ⊕₁ f ∘ id ⊕₁ (λ⇒ ∘ ! ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩ - ▽ ∘ id ⊕₁ f ∘ id ⊕₁ λ⇒ ∘ id ⊕₁ ! ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨ - ▽ ∘ id ⊕₁ f ∘ id ⊕₁ λ⇒ ∘ α⇒ ∘ (id ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ triangle ⟩ - ▽ ∘ id ⊕₁ f ∘ ρ⇒ ⊕₁ id ∘ (id ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₁ˡ ⟩ - ▽ ∘ id ⊕₁ f ∘ ρ⇒ ⊕₁ id ∘ (id ⊕₁ ! ∘ △) ⊕₁ id ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ △-identityʳ ⟩⊗⟨refl ⟩∘⟨refl ⟩ - ▽ ∘ id ⊕₁ f ∘ ρ⇒ ⊕₁ id ∘ ρ⇐ ⊕₁ id ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₁ˡ ⟩ - ▽ ∘ id ⊕₁ f ∘ (ρ⇒ ∘ ρ⇐) ⊕₁ id ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ unitorʳ.isoʳ ⟩⊗⟨refl ⟩∘⟨refl ⟩ - ▽ ∘ id ⊕₁ f ∘ id ⊕₁ id ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ elimˡ ⊕.identity ⟩ - ▽ ∘ id ⊕₁ f ∘ id ⊕₁ (▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩ - ▽ ∘ id ⊕₁ (f ∘ ▽ ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendʳ ⇒▽ ⟩∘⟨refl ⟩ - ▽ ∘ id ⊕₁ (▽ ∘ f ⊕₁ f ∘ (f †) ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ merge₁ʳ) ⟩∘⟨refl ⟩ - ▽ ∘ id ⊕₁ (▽ ∘ (f ∘ f †) ⊕₁ f) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩ - ▽ ∘ id ⊕₁ ▽ ∘ id ⊕₁ (f ∘ f †) ⊕₁ f ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ pushʳ (extendʳ (Equiv.sym assoc-commute-from)) ⟩ - ▽ ∘ (id ⊕₁ ▽ ∘ α⇒) ∘ (id ⊕₁ (f ∘ f †)) ⊕₁ f ∘ △ ⊕₁ id ≈⟨ extendʳ ▽-assoc ⟨ - ▽ ∘ ▽ ⊕₁ id ∘ (id ⊕₁ (f ∘ f †)) ⊕₁ f ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ merge₁ʳ ⟩ - ▽ ∘ ▽ ⊕₁ id ∘ (id ⊕₁ (f ∘ f †) ∘ △) ⊕₁ f ≈⟨ refl⟩∘⟨ merge₁ˡ ⟩ - ▽ ∘ (id + (f ∘ f †)) ⊕₁ f ≈⟨ refl⟩∘⟨ +-commutative ⟩⊗⟨refl ⟩ - ▽ ∘ ((f ∘ f †) + id) ⊕₁ f ≈⟨ refl⟩∘⟨ f∘f†≤id ⟩⊗⟨refl ⟩ - ▽ ∘ id ⊕₁ f ∎ + (∇ ∘ ⟨ π₁ , (f ∘ π₂) ∘ id ×₁ id ⟩) ∘ ⟨ π₁ , ∇ ∘ (f † ∘ id) ×₁ id ⟩ ≈⟨ pullʳ (⟨⟩-congˡ (elimʳ id×₁id) ⟩∘⟨ ⟨⟩-congˡ (refl⟩∘⟨ first-cong identityʳ)) ⟩ + ∇ ∘ ⟨ π₁ , (f ∘ π₂) ⟩ ∘ ⟨ π₁ , ∇ ∘ (f †) ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩∘ ⟩ + ∇ ∘ ⟨ π₁ ∘ ⟨ π₁ , ∇ ∘ (f †) ×₁ id ⟩ , (f ∘ π₂) ∘ ⟨ π₁ , ∇ ∘ (f †) ×₁ id ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ project₁ (pullʳ project₂) ⟩ + ∇ ∘ ⟨ π₁ , f ∘ ∇ ∘ (f †) ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (extendʳ ⇒∇-×₁) ⟩ + ∇ ∘ ⟨ π₁ , ∇ ∘ f ×₁ f ∘ (f †) ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (refl⟩∘⟨ ×₁∘first) ⟩ + ∇ ∘ ⟨ π₁ , ∇ ∘ (f ∘ f †) ×₁ f ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ identityʳ ⟨ + ∇ ∘ ⟨ π₁ , (∇ ∘ (f ∘ f †) ×₁ f) ∘ id ⟩ ≈⟨ refl⟩∘⟨ second∘⟨⟩ ⟨ + ∇ ∘ id ×₁ (∇ ∘ (f ∘ f †) ×₁ f) ∘ ⟨ π₁ , id ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congˡ η ⟨ + ∇ ∘ id ×₁ (∇ ∘ (f ∘ f †) ×₁ f) ∘ ⟨ π₁ , ⟨ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assocˡ∘⟨⟩ ⟨ + ∇ ∘ id ×₁ (∇ ∘ (f ∘ f †) ×₁ f) ∘ assocˡ ∘ ⟨ ⟨ π₁ , π₁ ⟩ , π₂ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ Δ∘ identityˡ ⟨ + ∇ ∘ id ×₁ (∇ ∘ (f ∘ f †) ×₁ f) ∘ assocˡ ∘ Δ ×₁ id ≈⟨ refl⟩∘⟨ pushˡ (sym second∘×₁) ⟩ + ∇ ∘ id ×₁ ∇ ∘ id ×₁ (f ∘ f †) ×₁ f ∘ assocˡ ∘ Δ ×₁ id ≈⟨ refl⟩∘⟨ pushʳ (extendʳ (sym assocˡ∘×₁)) ⟩ + ∇ ∘ (id ×₁ ∇ ∘ assocˡ) ∘ (id ×₁ (f ∘ f †)) ×₁ f ∘ Δ ×₁ id ≈⟨ extendʳ ∇-assoc-×₁ ⟨ + ∇ ∘ ∇ ×₁ id ∘ (id ×₁ (f ∘ f †)) ×₁ f ∘ Δ ×₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁∘first ⟩ + ∇ ∘ ∇ ×₁ id ∘ (id ×₁ (f ∘ f †) ∘ Δ) ×₁ f ≈⟨ refl⟩∘⟨ first∘×₁ ⟩ + ∇ ∘ (id + (f ∘ f †)) ×₁ f ≈⟨ refl⟩∘⟨ ×₁-congʳ (+-comm id (f ∘ f †)) ⟩ + ∇ ∘ ((f ∘ f †) + id) ×₁ f ≈⟨ refl⟩∘⟨ ×₁-congʳ f∘f†≤id ⟩ + ∇ ∘ id ×₁ f ∎ split≈pull∘loop : {A B : Obj} (f : A ⇒ B) → split f ≈-⧈ pull f ⌻ loop split≈pull∘loop f = ≈ᵢ ⌸ Equiv.sym identityʳ where - open ⇒-Reasoning 𝒞 - open ⊗-Reasoning +-monoidal - ≈ᵢ : ▽ ∘ id ⊕₁ f - ≈ ▽ ∘ id ⊕₁ ((f ∘ p₂) ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id + ≈ᵢ : ∇ ∘ id ×₁ f + ≈ ∇ ∘ ⟨ π₁ , (f ∘ π₂) ∘ id ×₁ id ⟩ ≈ᵢ = begin - ▽ ∘ id ⊕₁ f ≈⟨ refl⟩∘⟨ introʳ ⊕.identity ⟩ - ▽ ∘ id ⊕₁ f ∘ id ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ unitorʳ.isoʳ ⟩⊗⟨refl ⟨ - ▽ ∘ id ⊕₁ f ∘ (ρ⇒ ∘ ρ⇐) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ˡ ⟩ - ▽ ∘ id ⊕₁ f ∘ ρ⇒ ⊕₁ id ∘ ρ⇐ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ △-identityʳ ⟩⊗⟨refl ⟨ - ▽ ∘ id ⊕₁ f ∘ ρ⇒ ⊕₁ id ∘ (id ⊕₁ ! ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (Equiv.sym triangle) ⟩ - ▽ ∘ id ⊕₁ f ∘ id ⊕₁ λ⇒ ∘ α⇒ ∘ (id ⊕₁ ! ∘ △) ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ˡ ⟩ - ▽ ∘ id ⊕₁ f ∘ id ⊕₁ λ⇒ ∘ α⇒ ∘ (id ⊕₁ !) ⊕₁ id ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟩ - ▽ ∘ id ⊕₁ f ∘ id ⊕₁ λ⇒ ∘ id ⊕₁ ! ⊕₁ id ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩ - ▽ ∘ id ⊕₁ f ∘ id ⊕₁ (λ⇒ ∘ ! ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ p₂-⊕ ⟩∘⟨refl ⟨ - ▽ ∘ id ⊕₁ f ∘ id ⊕₁ p₂ ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩ - ▽ ∘ id ⊕₁ (f ∘ p₂) ∘ α⇒ ∘ △ ⊕₁ id ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (pushʳ (introʳ ⊕.identity)) ⟩∘⟨refl ⟩ - ▽ ∘ id ⊕₁ ((f ∘ p₂) ∘ id ⊕₁ id) ∘ α⇒ ∘ △ ⊕₁ id ∎ + ∇ ∘ id ×₁ f ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ identityˡ ⟩ + ∇ ∘ ⟨ π₁ , f ∘ π₂ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (introʳ id×₁id) ⟩ + ∇ ∘ ⟨ π₁ , (f ∘ π₂) ∘ id ×₁ id ⟩ ∎ loop∘push∘loop : {A B : Obj} (f : A ⇒ B) → id ≤ ((f †) ∘ f) → loop ⌻ push f ⌻ loop ≈-⧈ loop ⌻ push f loop∘push∘loop f id≤f†∘f = ≈-trans (loop∘push∘loop≈merge f id≤f†∘f) (merge≈loop∘push f) diff --git a/Data/WiringDiagram/Looped.agda b/Data/WiringDiagram/Looped.agda index 6f63e88..9669e4a 100644 --- a/Data/WiringDiagram/Looped.agda +++ b/Data/WiringDiagram/Looped.agda @@ -2,7 +2,7 @@ open import Categories.Category using (Category) open import Categories.Functor using (Functor; _∘F_) -open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger) +open import Category.Dagger.Semiadditive using (SemiadditiveDagger; IdempotentSemiadditiveDagger) open import Category.KaroubiComplete using (KaroubiComplete) open import Data.WiringDiagram.Balanced using (BWD) open import Level using (Level) @@ -12,8 +12,10 @@ module Data.WiringDiagram.Looped {𝒞 : Category o ℓ e} {𝒟 : Category o′ ℓ′ e′} {S : IdempotentSemiadditiveDagger 𝒞} + (let module S = IdempotentSemiadditiveDagger S) + (let S′ = S.semiadditiveDagger) (karoubiComplete : KaroubiComplete 𝒟) - (F : Functor (BWD S) 𝒟) + (F : Functor (BWD S′) 𝒟) where import Categories.Morphism.Idempotent as Idempotent @@ -22,11 +24,11 @@ import Categories.Morphism.Reasoning as ⇒-Reasoning open import Categories.Category using (Category) open import Categories.Functor.Properties using ([_]-resp-∘) open import Category.Dagger.2-Poset using (Dagger-2-Poset; dagger-2-poset; Maps; Map) -open import Data.WiringDiagram.Balanced S using (Include; Push; Pull) -open import Data.WiringDiagram.Core S using (loop; id-⧈; _□_) +open import Data.WiringDiagram.Balanced S′ using (Include; Push; Pull) +open import Data.WiringDiagram.Core S′ using (loop; id-⧈; _□_) open import Data.WiringDiagram.Equalities S using (loop∘loop; loop∘push∘loop; loop∘pull∘loop) -module BWD = Category (BWD S) +module BWD = Category (BWD S′) module F = Functor F module 𝒞 = Category 𝒞 module 𝒟 = Category 𝒟 @@ -67,10 +69,10 @@ module _ (A : 𝒞.Obj) where module Push = Functor Push module Pull = Functor Pull -S′ : Dagger-2-Poset -S′ = dagger-2-poset S +S-≤ : Dagger-2-Poset +S-≤ = dagger-2-poset S -Merge : Functor (Maps S′) 𝒟 +Merge : Functor (Maps S-≤) 𝒟 Merge = record { F₀ = Looped ; F₁ = λ {A} {B} f → π B ∘ F.₁ (Push.₁ (map f)) ∘ forget A @@ -91,8 +93,8 @@ Merge = record 𝒟.id ∎ homo : {X Y Z : 𝒞.Obj} - {f : Map S′ X Y} - {g : Map S′ Y Z} + {f : Map S-≤ X Y} + {g : Map S-≤ Y Z} → π Z ∘ F.₁ (Push.₁ (map g 𝒞.∘ map f)) ∘ forget X 𝒟.≈ (π Z ∘ F.₁ (Push.₁ (map g)) ∘ forget Y) ∘ π Y ∘ F.₁ (Push.₁ (map f)) ∘ forget X homo {X} {Y} {Z} {f′} {g′} = begin π Z ∘ F.₁ (Push.₁ (g 𝒞.∘ f)) ∘ forget X ≈⟨ refl⟩∘⟨ F.F-resp-≈ Push.homomorphism ⟩∘⟨refl ⟩ @@ -113,7 +115,7 @@ Merge = record resp : {A B : 𝒞.Obj} {f g : A 𝒞.⇒ B} → f 𝒞.≈ g → π B ∘ F.₁ (Push.₁ f) ∘ forget A 𝒟.≈ π B ∘ F.₁ (Push.₁ g) ∘ forget A resp {A} {B} {f} {g} f≈g = refl⟩∘⟨ F.F-resp-≈ (Push.F-resp-≈ f≈g) ⟩∘⟨refl -Split : Functor (op (Maps S′)) 𝒟 +Split : Functor (op (Maps S-≤)) 𝒟 Split = record { F₀ = Looped ; F₁ = λ {A} {B} f → π B ∘ F.₁ (Pull.₁ (map f)) ∘ forget A @@ -134,8 +136,8 @@ Split = record 𝒟.id ∎ homo : {X Y Z : 𝒞.Obj} - {f : Map S′ Y X} - {g : Map S′ Z Y} + {f : Map S-≤ Y X} + {g : Map S-≤ Z Y} → π Z ∘ F.₁ (Pull.₁ (map f 𝒞.∘ map g)) ∘ forget X 𝒟.≈ (π Z ∘ F.₁ (Pull.₁ (map g)) ∘ forget Y) ∘ π Y ∘ F.₁ (Pull.₁ (map f)) ∘ forget X homo {X} {Y} {Z} {f′} {g′} = begin π Z ∘ F.₁ (Pull.₁ (f 𝒞.∘ g)) ∘ forget X ≈⟨ refl⟩∘⟨ F.F-resp-≈ Pull.homomorphism ⟩∘⟨refl ⟩ |