From 78319064329e6b334298ea4bed2eec01d2fc8b47 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Mon, 13 Jul 2026 21:54:23 -0700 Subject: Add split functor --- Data/WiringDiagram/Looped.agda | 67 +++++++++++++++++++++++++++++++++++++----- 1 file changed, 59 insertions(+), 8 deletions(-) diff --git a/Data/WiringDiagram/Looped.agda b/Data/WiringDiagram/Looped.agda index 3698a60..6f63e88 100644 --- a/Data/WiringDiagram/Looped.agda +++ b/Data/WiringDiagram/Looped.agda @@ -3,9 +3,9 @@ open import Categories.Category using (Category) open import Categories.Functor using (Functor; _∘F_) open import Category.Dagger.Semiadditive using (IdempotentSemiadditiveDagger) +open import Category.KaroubiComplete using (KaroubiComplete) 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} @@ -16,18 +16,23 @@ module Data.WiringDiagram.Looped (F : Functor (BWD S) 𝒟) where +import Categories.Morphism.Idempotent as Idempotent +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) +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) +open import Data.WiringDiagram.Equalities S using (loop∘loop; loop∘push∘loop; loop∘pull∘loop) -module 𝒞 = Category 𝒞 -module 𝒟 = Category 𝒟 module BWD = Category (BWD S) module F = Functor F +module 𝒞 = Category 𝒞 +module 𝒟 = Category 𝒟 -open import Categories.Morphism.Idempotent 𝒟 using (IsSplitIdempotent) +open Category using (op) +open Idempotent 𝒟 using (IsSplitIdempotent) module _ (A : 𝒞.Obj) where @@ -56,7 +61,11 @@ module _ (A : 𝒞.Obj) where π∘l : π 𝒟.∘ L 𝒟.≈ π π∘l = retract-absorb + l∘forget : L 𝒟.∘ forget 𝒟.≈ forget + l∘forget = section-absorb + module Push = Functor Push +module Pull = Functor Pull S′ : Dagger-2-Poset S′ = dagger-2-poset S @@ -73,7 +82,6 @@ Merge = record 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 @@ -96,7 +104,7 @@ Merge = record π 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 ∎ + (π Z ∘ F.₁ (Push.₁ g) ∘ forget Y) ∘ π Y ∘ F.₁ (Push.₁ f) ∘ forget X ∎ where f : X 𝒞.⇒ Y f = map f′ @@ -104,3 +112,46 @@ Merge = record 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 + +Split : Functor (op (Maps S′)) 𝒟 +Split = record + { F₀ = Looped + ; F₁ = λ {A} {B} f → π B ∘ F.₁ (Pull.₁ (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 + open ⇒-Reasoning 𝒟 + iden : {A : 𝒞.Obj} → π A ∘ F.₁ (Pull.₁ 𝒞.id) ∘ forget A 𝒟.≈ 𝒟.id + iden {A} = begin + π A ∘ F.₁ (Pull.₁ 𝒞.id) ∘ forget A ≈⟨ refl⟩∘⟨ F.F-resp-≈ Pull.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′ 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 ⟩ + π Z ∘ F.₁ (Pull.₁ g BWD.∘ Pull.₁ f) ∘ forget X ≈⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩ + π Z ∘ F.₁ (Pull.₁ g) ∘ F.₁ (Pull.₁ f) ∘ forget X ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ l∘forget X ⟨ + π Z ∘ F.₁ (Pull.₁ g) ∘ F.₁ (Pull.₁ f) ∘ L X ∘ forget X ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (𝒟.Equiv.sym F.homomorphism) ⟩ + π Z ∘ F.₁ (Pull.₁ g) ∘ F.₁ (Pull.₁ f BWD.∘ loop) ∘ forget X ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F.F-resp-≈ (loop∘pull∘loop f (functional f′)) ⟩∘⟨refl ⟨ + π Z ∘ F.₁ (Pull.₁ g) ∘ F.₁ (loop BWD.∘ Pull.₁ f BWD.∘ loop) ∘ forget X ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩ + π Z ∘ F.₁ (Pull.₁ g) ∘ L Y ∘ F.₁ (Pull.₁ f BWD.∘ loop) ∘ forget X ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩ + π Z ∘ F.₁ (Pull.₁ g) ∘ L Y ∘ F.₁ (Pull.₁ f) ∘ L X ∘ forget X ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ l∘forget X ⟩ + π Z ∘ F.₁ (Pull.₁ g) ∘ L Y ∘ F.₁ (Pull.₁ f) ∘ forget X ≈⟨ pushʳ (pushʳ (pushˡ (𝒟.Equiv.sym (forget∘π Y)))) ⟩ + (π Z ∘ F.₁ (Pull.₁ g) ∘ forget Y) ∘ π Y ∘ F.₁ (Pull.₁ f) ∘ forget X ∎ + where + f : Y 𝒞.⇒ X + f = map f′ + g : Z 𝒞.⇒ Y + g = map g′ + resp : {A B : 𝒞.Obj} {f g : B 𝒞.⇒ A} → f 𝒞.≈ g → π B ∘ F.₁ (Pull.₁ f) ∘ forget A 𝒟.≈ π B ∘ F.₁ (Pull.₁ g) ∘ forget A + resp {A} {B} {f} {g} f≈g = refl⟩∘⟨ F.F-resp-≈ (Pull.F-resp-≈ f≈g) ⟩∘⟨refl -- cgit v1.2.3