diff options
Diffstat (limited to 'Data')
| -rw-r--r-- | Data/WiringDiagram/Equalities.agda | 6 | ||||
| -rw-r--r-- | Data/WiringDiagram/Looped.agda | 106 |
2 files changed, 109 insertions, 3 deletions
diff --git a/Data/WiringDiagram/Equalities.agda b/Data/WiringDiagram/Equalities.agda index 37b8f38..1e5eb47 100644 --- a/Data/WiringDiagram/Equalities.agda +++ b/Data/WiringDiagram/Equalities.agda @@ -102,7 +102,7 @@ loop∘pull∘loop≈split f f∘f†≤id = ≈ᵢ ⌸ (identityˡ ○ identity ≈ ▽ ∘ 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) ∘ α⇒ ∘ △ ⊕₁ 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₂ˡ ⟩ @@ -121,8 +121,8 @@ loop∘pull∘loop≈split f f∘f†≤id = ≈ᵢ ⌸ (identityˡ ○ identity ▽ ∘ (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 †)) ⊕₁ f ≈⟨ refl⟩∘⟨ +-commutative ⟩⊗⟨refl ⟩ + ▽ ∘ ((f ∘ f †) + id) ⊕₁ f ≈⟨ refl⟩∘⟨ f∘f†≤id ⟩⊗⟨refl ⟩ ▽ ∘ id ⊕₁ f ∎ split≈pull∘loop : {A B : Obj} (f : A ⇒ B) → split f ≈-⧈ pull f ⌻ loop diff --git a/Data/WiringDiagram/Looped.agda b/Data/WiringDiagram/Looped.agda new file mode 100644 index 0000000..3698a60 --- /dev/null +++ b/Data/WiringDiagram/Looped.agda @@ -0,0 +1,106 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category using (Category) +open import Categories.Functor using (Functor; _∘F_) +open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger) +open import Data.WiringDiagram.Balanced using (BWD) +open import Level using (Level) +open import Category.KaroubiComplete using (KaroubiComplete) + +module Data.WiringDiagram.Looped + {o ℓ e o′ ℓ′ e′ : Level} + {𝒞 : Category o ℓ e} + {𝒟 : Category o′ ℓ′ e′} + {S : IdempotentSemiadditiveDagger 𝒞} + (karoubiComplete : KaroubiComplete 𝒟) + (F : Functor (BWD S) 𝒟) + where + +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) +open import Data.WiringDiagram.Core S using (loop; id-⧈; _□_) +open import Data.WiringDiagram.Equalities S using (loop∘loop; loop∘push∘loop) + +module 𝒞 = Category 𝒞 +module 𝒟 = Category 𝒟 +module BWD = Category (BWD S) +module F = Functor F + +open import Categories.Morphism.Idempotent 𝒟 using (IsSplitIdempotent) + +module _ (A : 𝒞.Obj) where + + open KaroubiComplete karoubiComplete using (split) + open IsSplitIdempotent (split ([ F ]-resp-∘ (loop∘loop {A}))) + + Unlooped Looped : 𝒟.Obj + Unlooped = F.₀ A + Looped = obj + + L : Unlooped 𝒟.⇒ Unlooped + L = F.₁ loop + + π : Unlooped 𝒟.⇒ Looped + π = retract + + forget : Looped 𝒟.⇒ Unlooped + forget = section + + forget∘π : forget 𝒟.∘ π 𝒟.≈ L + forget∘π = splits + + π∘forget : π 𝒟.∘ forget 𝒟.≈ 𝒟.id + π∘forget = retracts + + π∘l : π 𝒟.∘ L 𝒟.≈ π + π∘l = retract-absorb + +module Push = Functor Push + +S′ : Dagger-2-Poset +S′ = dagger-2-poset S + +Merge : Functor (Maps S′) 𝒟 +Merge = record + { F₀ = Looped + ; F₁ = λ {A} {B} f → π B ∘ F.₁ (Push.₁ (map f)) ∘ forget A + ; identity = iden + ; homomorphism = λ {f = f} {g} → homo {f = f} {g} + ; F-resp-≈ = resp + } + where + open Map + open Category 𝒟 using (_∘_) + open 𝒟.HomReasoning + import Categories.Morphism.Reasoning as ⇒-Reasoning + open ⇒-Reasoning 𝒟 + iden : {A : 𝒞.Obj} → π A ∘ F.₁ (Push.₁ 𝒞.id) ∘ forget A 𝒟.≈ 𝒟.id + iden {A} = begin + π A ∘ F.₁ (Push.₁ 𝒞.id) ∘ forget A ≈⟨ refl⟩∘⟨ F.F-resp-≈ Push.identity ⟩∘⟨refl ⟩ + π A ∘ F.₁ BWD.id ∘ forget A ≈⟨ refl⟩∘⟨ elimˡ F.identity ⟩ + π A ∘ forget A ≈⟨ π∘forget A ⟩ + 𝒟.id ∎ + homo + : {X Y Z : 𝒞.Obj} + {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 ⟩ + π Z ∘ F.₁ (Push.₁ g BWD.∘ Push.₁ f) ∘ forget X ≈⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩ + π Z ∘ F.₁ (Push.₁ g) ∘ F.₁ (Push.₁ f) ∘ forget X ≈⟨ pushˡ (𝒟.Equiv.sym (π∘l Z)) ⟩ + π Z ∘ L Z ∘ F.₁ (Push.₁ g) ∘ F.₁ (Push.₁ f) ∘ forget X ≈⟨ refl⟩∘⟨ pullˡ (𝒟.Equiv.sym F.homomorphism) ⟩ + π Z ∘ F.₁ (loop BWD.∘ Push.₁ g) ∘ F.₁ (Push.₁ f) ∘ forget X ≈⟨ refl⟩∘⟨ F.F-resp-≈ (loop∘push∘loop g (entire g′)) ⟩∘⟨refl ⟨ + π Z ∘ F.₁ (loop BWD.∘ Push.₁ g BWD.∘ loop) ∘ F.₁ (Push.₁ f) ∘ forget X ≈⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩ + π Z ∘ L Z ∘ F.₁ (Push.₁ g BWD.∘ loop) ∘ F.₁ (Push.₁ f) ∘ forget X ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩ + π Z ∘ L Z ∘ F.₁ (Push.₁ g) ∘ L Y ∘ F.₁ (Push.₁ f) ∘ forget X ≈⟨ pullˡ (π∘l Z) ⟩ + π Z ∘ F.₁ (Push.₁ g) ∘ L Y ∘ F.₁ (Push.₁ f) ∘ forget X ≈⟨ pushʳ (pushʳ (pushˡ (𝒟.Equiv.sym (forget∘π Y)))) ⟩ + (π Z ∘ F.₁ (Push.₁ g) ∘ forget Y) ∘ π Y ∘ F.₁ (Push.₁ f) ∘ forget X ∎ + where + f : X 𝒞.⇒ Y + f = map f′ + g : Y 𝒞.⇒ Z + g = map g′ + 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 |