From 11e8c93b5426ddfd75f1c9c495e4da0defbc08a6 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Wed, 25 Mar 2026 08:53:18 -0500 Subject: Add looped wiring diagrams and merge functor --- Category/KaroubiComplete.agda | 16 ++++++ Data/WiringDiagram/Equalities.agda | 6 +-- Data/WiringDiagram/Looped.agda | 106 +++++++++++++++++++++++++++++++++++++ 3 files changed, 125 insertions(+), 3 deletions(-) create mode 100644 Category/KaroubiComplete.agda create mode 100644 Data/WiringDiagram/Looped.agda diff --git a/Category/KaroubiComplete.agda b/Category/KaroubiComplete.agda new file mode 100644 index 0000000..e4005d1 --- /dev/null +++ b/Category/KaroubiComplete.agda @@ -0,0 +1,16 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category using (Category) +open import Level using (Level; suc; _βŠ”_) + +module Category.KaroubiComplete {o β„“ e : Level} (π’ž : Category o β„“ e) where + +open import Categories.Morphism.Idempotent π’ž using (IsSplitIdempotent) + +open Category π’ž + +-- A Karoubi complete category is one in which all idempotents split +record KaroubiComplete : Set (suc (oΒ βŠ” β„“ βŠ” e)) where + + field + split : {A : Obj} {f : A β‡’ A} β†’ f ∘ f β‰ˆ f β†’ IsSplitIdempotent f 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 -- cgit v1.2.3