diff options
| -rw-r--r-- | Data/Hypergraph.agda | 2 | ||||
| -rw-r--r-- | Data/Hypergraph/Edge.agda | 72 | ||||
| -rw-r--r-- | Data/Opaque/List.agda | 61 | ||||
| -rw-r--r-- | Functor/Instance/List.agda | 61 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Circ.agda | 2 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Edge.agda | 9 | ||||
| -rw-r--r-- | Functor/Monoidal/Construction/MultisetOf.agda | 6 | ||||
| -rw-r--r-- | Functor/Monoidal/Instance/Nat/Circ.agda | 20 |
8 files changed, 157 insertions, 76 deletions
diff --git a/Data/Hypergraph.agda b/Data/Hypergraph.agda index 770c500..7d22129 100644 --- a/Data/Hypergraph.agda +++ b/Data/Hypergraph.agda @@ -12,6 +12,8 @@ import Data.Hypergraph.Edge {ℓ} HL as Hyperedge import Data.List.Relation.Binary.Permutation.Propositional as List-↭ import Data.List.Relation.Binary.Permutation.Setoid as ↭ +open HypergraphLabel HL using (Label) public + open import Data.List using (List; map) open import Data.Nat using (ℕ) open import Data.String using (String; unlines) diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda index 5c22a04..447f008 100644 --- a/Data/Hypergraph/Edge.agda +++ b/Data/Hypergraph/Edge.agda @@ -5,23 +5,24 @@ open import Data.Hypergraph.Label using (HypergraphLabel) open import Level using (Level; 0ℓ) module Data.Hypergraph.Edge {ℓ : Level} (HL : HypergraphLabel) where -import Data.Vec as Vec -import Data.Vec.Relation.Binary.Equality.Cast as VecCast -import Relation.Binary.PropositionalEquality as ≡ +import Data.Vec.Functional as Vec +import Data.Vec.Functional.Relation.Binary.Equality.Setoid as PW +import Data.Fin.Properties as FinProp -open import Data.Fin using (Fin) +open import Data.Fin as Fin using (Fin) open import Data.Fin.Show using () renaming (show to showFin) open import Data.Nat using (ℕ) open import Data.String using (String; _<+>_) open import Data.Vec.Show using () renaming (show to showVec) open import Level using (0ℓ) open import Relation.Binary using (Setoid; IsEquivalence) -open import Function using (_⟶ₛ_; Func) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning) +open import Function using (_⟶ₛ_; Func; _∘_) module HL = HypergraphLabel HL -open HL using (Label; cast; cast-is-id) -open Vec using (Vec) +open HL using (Label) +open Vec using (Vector) open Func record Edge (v : ℕ) : Set ℓ where @@ -29,7 +30,7 @@ record Edge (v : ℕ) : Set ℓ where field {arity} : ℕ label : Label arity - ports : Vec (Fin v) arity + ports : Fin arity → Fin v map : {n m : ℕ} → (Fin n → Fin m) → Edge n → Edge m map f edge = record @@ -39,11 +40,10 @@ map f edge = record where open Edge edge -open ≡ using (_≡_) -open VecCast using (_≈[_]_) - module _ {v : ℕ} where + open PW (≡.setoid (Fin v)) using (_≋_) + -- an equivalence relation on edges with v nodes record _≈_ (E E′ : Edge v) : Set ℓ where constructor mk≈ @@ -51,34 +51,49 @@ module _ {v : ℕ} where module E′ = Edge E′ field ≡arity : E.arity ≡ E′.arity - ≡label : cast ≡arity E.label ≡ E′.label - ≡ports : E.ports ≈[ ≡arity ] E′.ports + ≡label : HL.cast ≡arity E.label ≡ E′.label + ≡ports : E.ports ≋ E′.ports ∘ Fin.cast ≡arity ≈-refl : {x : Edge v} → x ≈ x - ≈-refl = record + ≈-refl {x} = record { ≡arity = ≡.refl ; ≡label = HL.≈-reflexive ≡.refl - ; ≡ports = VecCast.≈-reflexive ≡.refl + ; ≡ports = ≡.cong (Edge.ports x) ∘ ≡.sym ∘ FinProp.cast-is-id _ } ≈-sym : {x y : Edge v} → x ≈ y → y ≈ x ≈-sym x≈y = record { ≡arity = ≡.sym ≡arity ; ≡label = HL.≈-sym ≡label - ; ≡ports = VecCast.≈-sym ≡ports + ; ≡ports = ≡.sym ∘ ≡ports-sym } where open _≈_ x≈y - - ≈-trans : {i j k : Edge v} → i ≈ j → j ≈ k → i ≈ k - ≈-trans {i} {j} {k} i≈j j≈k = record - { ≡arity = ≡.trans i≈j.≡arity j≈k.≡arity - ; ≡label = HL.≈-trans i≈j.≡label j≈k.≡label - ; ≡ports = VecCast.≈-trans i≈j.≡ports j≈k.≡ports + open ≡-Reasoning + ≡ports-sym : (i : Fin E′.arity) → E.ports (Fin.cast _ i) ≡ E′.ports i + ≡ports-sym i = begin + E.ports (Fin.cast _ i) ≡⟨ ≡ports (Fin.cast _ i) ⟩ + E′.ports (Fin.cast ≡arity (Fin.cast _ i)) + ≡⟨ ≡.cong E′.ports (FinProp.cast-involutive ≡arity _ i) ⟩ + E′.ports i ∎ + + ≈-trans : {x y z : Edge v} → x ≈ y → y ≈ z → x ≈ z + ≈-trans {x} {y} {z} x≈y y≈z = record + { ≡arity = ≡.trans x≈y.≡arity y≈z.≡arity + ; ≡label = HL.≈-trans x≈y.≡label y≈z.≡label + ; ≡ports = ≡-ports } where - module i≈j = _≈_ i≈j - module j≈k = _≈_ j≈k + module x≈y = _≈_ x≈y + module y≈z = _≈_ y≈z + open ≡-Reasoning + ≡-ports : (i : Fin x≈y.E.arity) → x≈y.E.ports i ≡ y≈z.E′.ports (Fin.cast _ i) + ≡-ports i = begin + x≈y.E.ports i ≡⟨ x≈y.≡ports i ⟩ + y≈z.E.ports (Fin.cast _ i) ≡⟨ y≈z.≡ports (Fin.cast _ i) ⟩ + y≈z.E′.ports (Fin.cast y≈z.≡arity (Fin.cast _ i)) + ≡⟨ ≡.cong y≈z.E′.ports (FinProp.cast-trans _ y≈z.≡arity i) ⟩ + y≈z.E′.ports (Fin.cast _ i) ∎ ≈-IsEquivalence : IsEquivalence _≈_ ≈-IsEquivalence = record @@ -88,16 +103,11 @@ module _ {v : ℕ} where } show : Edge v → String - show (mkEdge {a} l p) = HL.showLabel a l <+> showVec showFin p - - ≈⇒≡ : {x y : Edge v} → x ≈ y → x ≡ y - ≈⇒≡ {mkEdge l p} (mk≈ ≡.refl ≡.refl ≡.refl) - rewrite cast-is-id ≡.refl l - rewrite VecCast.cast-is-id ≡.refl p = ≡.refl + show (mkEdge {a} l p) = HL.showLabel a l <+> showVec showFin (Vec.toVec p) Edgeₛ : (v : ℕ) → Setoid ℓ ℓ Edgeₛ v = record { isEquivalence = ≈-IsEquivalence {v} } mapₛ : {n m : ℕ} → (Fin n → Fin m) → Edgeₛ n ⟶ₛ Edgeₛ m mapₛ f .to = map f -mapₛ f .cong (mk≈ ≡a ≡l ≡p) = mk≈ ≡a ≡l (VecCast.≈-cong′ (Vec.map f) ≡p) +mapₛ f .cong (mk≈ ≡a ≡l ≡p) = mk≈ ≡a ≡l (≡.cong f ∘ ≡p) diff --git a/Data/Opaque/List.agda b/Data/Opaque/List.agda new file mode 100644 index 0000000..a8e536f --- /dev/null +++ b/Data/Opaque/List.agda @@ -0,0 +1,61 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Opaque.List where + +import Data.List as L +import Function.Construct.Constant as Const + +open import Level using (Level; _⊔_) +open import Data.List.Relation.Binary.Pointwise as PW using (++⁺; map⁺) +open import Data.Product using (uncurry′) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Unit.Polymorphic using (⊤) +open import Function using (_⟶ₛ_; Func) +open import Relation.Binary using (Setoid) + +open Func + +private + + variable + a c ℓ : Level + A B : Set a + Aₛ Bₛ : Setoid c ℓ + + ⊤ₛ : Setoid c ℓ + ⊤ₛ = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } + +opaque + + List : Set a → Set a + List = L.List + + [] : List A + [] = L.[] + + _∷_ : A → List A → List A + _∷_ = L._∷_ + + map : (A → B) → List A → List B + map = L.map + + _++_ : List A → List A → List A + _++_ = L._++_ + + Listₛ : Setoid c ℓ → Setoid c (c ⊔ ℓ) + Listₛ = PW.setoid + + []ₛ : ⊤ₛ {c} {c ⊔ ℓ} ⟶ₛ Listₛ {c} {ℓ} Aₛ + []ₛ = Const.function ⊤ₛ (Listₛ _) [] + + ∷ₛ : Aₛ ×ₛ Listₛ Aₛ ⟶ₛ Listₛ Aₛ + ∷ₛ .to = uncurry′ _∷_ + ∷ₛ .cong = uncurry′ PW._∷_ + + mapₛ : (Aₛ ⟶ₛ Bₛ) → Listₛ Aₛ ⟶ₛ Listₛ Bₛ + mapₛ f .to = map (to f) + mapₛ f .cong xs≈ys = map⁺ (to f) (to f) (PW.map (cong f) xs≈ys) + + ++ₛ : Listₛ Aₛ ×ₛ Listₛ Aₛ ⟶ₛ Listₛ Aₛ + ++ₛ .to = uncurry′ _++_ + ++ₛ .cong = uncurry′ ++⁺ diff --git a/Functor/Instance/List.agda b/Functor/Instance/List.agda index b40670d..ceb73e1 100644 --- a/Functor/Instance/List.agda +++ b/Functor/Instance/List.agda @@ -4,13 +4,12 @@ open import Level using (Level; _⊔_) module Functor.Instance.List {c ℓ : Level} where -import Data.List as List import Data.List.Properties as ListProps import Data.List.Relation.Binary.Pointwise as PW open import Categories.Category.Instance.Setoids using (Setoids) open import Categories.Functor using (Functor) -open import Data.Setoid using (∣_∣) +open import Data.Setoid using (∣_∣; _⇒ₛ_) open import Function.Base using (_∘_; id) open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_) open import Relation.Binary using (Setoid) @@ -19,40 +18,48 @@ open Functor open Setoid using (reflexive) open Func +open import Data.Opaque.List as List hiding (List) + private variable A B C : Setoid c ℓ --- the List functor takes a carrier A to lists of A --- and the equivalence on A to pointwise equivalence on lists of A +open import Function.Construct.Identity using () renaming (function to Id) +open import Function.Construct.Setoid using (_∙_) -Listₛ : Setoid c ℓ → Setoid c (c ⊔ ℓ) -Listₛ = PW.setoid +opaque --- List on morphisms is the familiar map operation --- which applies the same function to every element of a list + unfolding List.List + + map-id + : (xs : ∣ Listₛ A ∣) + → (open Setoid (Listₛ A)) + → mapₛ (Id _) ⟨$⟩ xs ≈ xs + map-id {A} = reflexive (Listₛ A) ∘ ListProps.map-id -mapₛ : A ⟶ₛ B → Listₛ A ⟶ₛ Listₛ B -mapₛ f .to = List.map (to f) -mapₛ f .cong = PW.map⁺ (to f) (to f) ∘ PW.map (cong f) + List-homo + : (f : A ⟶ₛ B) + (g : B ⟶ₛ C) + → (xs : ∣ Listₛ A ∣) + → (open Setoid (Listₛ C)) + → mapₛ (g ∙ f) ⟨$⟩ xs ≈ mapₛ g ⟨$⟩ (mapₛ f ⟨$⟩ xs) + List-homo {C = C} f g = reflexive (Listₛ C) ∘ ListProps.map-∘ -map-id - : (xs : ∣ Listₛ A ∣) - → (open Setoid (Listₛ A)) - → List.map id xs ≈ xs -map-id {A} = reflexive (Listₛ A) ∘ ListProps.map-id + List-resp-≈ + : (f g : A ⟶ₛ B) + → (let open Setoid (A ⇒ₛ B) in f ≈ g) + → (let open Setoid (Listₛ A ⇒ₛ Listₛ B) in mapₛ f ≈ mapₛ g) + List-resp-≈ f g f≈g = PW.map⁺ (to f) (to g) (PW.refl f≈g) -List-homo - : (f : A ⟶ₛ B) - (g : B ⟶ₛ C) - → (xs : ∣ Listₛ A ∣) - → (open Setoid (Listₛ C)) - → List.map (to g ∘ to f) xs ≈ List.map (to g) (List.map (to f) xs) -List-homo {C = C} f g = reflexive (Listₛ C) ∘ ListProps.map-∘ +-- the List functor takes a carrier A to lists of A +-- and the equivalence on A to pointwise equivalence on lists of A + +-- List on morphisms is the familiar map operation +-- which applies the same function to every element of a list List : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ)) -List .F₀ = Listₛ -List .F₁ = mapₛ -List .identity {A} {xs} = map-id {A} xs +List .F₀ = List.Listₛ +List .F₁ = List.mapₛ +List .identity {_} {xs} = map-id xs List .homomorphism {f = f} {g} {xs} = List-homo f g xs -List .F-resp-≈ {A} {B} {f} {g} f≈g = PW.map⁺ (to f) (to g) (PW.refl f≈g) +List .F-resp-≈ {f = f} {g} f≈g = List-resp-≈ f g f≈g diff --git a/Functor/Instance/Nat/Circ.agda b/Functor/Instance/Nat/Circ.agda index 09bc495..36d726d 100644 --- a/Functor/Instance/Nat/Circ.agda +++ b/Functor/Instance/Nat/Circ.agda @@ -28,5 +28,5 @@ Circ : Functor Nat (Setoids ℓ ℓ) Circ .F₀ = Circuitₛ Circ .F₁ = mapₛ Circ .identity = cong mkCircuitₛ Multiset∘Edge.identity -Circ .homomorphism = cong mkCircuitₛ Multiset∘Edge.homomorphism +Circ .homomorphism {f = f} {g = g} = cong mkCircuitₛ (Multiset∘Edge.homomorphism {f = f} {g = g}) Circ .F-resp-≈ f≗g = cong mkCircuitₛ (Multiset∘Edge.F-resp-≈ f≗g) diff --git a/Functor/Instance/Nat/Edge.agda b/Functor/Instance/Nat/Edge.agda index 5de8f84..c69a1db 100644 --- a/Functor/Instance/Nat/Edge.agda +++ b/Functor/Instance/Nat/Edge.agda @@ -12,6 +12,7 @@ open import Categories.Category.Instance.Nat using (Nat) open import Categories.Category.Instance.Setoids using (Setoids) open import Categories.Functor using (Functor) open import Data.Fin using (Fin) +open import Data.Fin.Properties using (cast-is-id) open import Data.Hypergraph.Edge {ℓ} HL as Edge using (Edgeₛ; map; mapₛ; _≈_) open import Data.Nat using (ℕ) open import Data.Vec.Relation.Binary.Equality.Cast using (≈-reflexive) @@ -29,7 +30,7 @@ open Functor map-id : {v : ℕ} {e : Edge.Edge v} → map id e ≈ e map-id .≡arity = ≡.refl map-id .≡label = HL.≈-reflexive ≡.refl -map-id {_} {e} .≡ports = ≈-reflexive (VecProps.map-id (ports e)) +map-id {_} {e} .≡ports = ≡.cong (ports e) ∘ ≡.sym ∘ cast-is-id ≡.refl map-∘ : {n m o : ℕ} @@ -39,7 +40,7 @@ map-∘ → map (g ∘ f) e ≈ map g (map f e) map-∘ f g .≡arity = ≡.refl map-∘ f g .≡label = HL.≈-reflexive ≡.refl -map-∘ f g {e} .≡ports = ≈-reflexive (VecProps.map-∘ g f (ports e)) +map-∘ f g {e} .≡ports = ≡.cong (g ∘ f ∘ ports e) ∘ ≡.sym ∘ cast-is-id ≡.refl map-resp-≗ : {n m : ℕ} @@ -49,11 +50,11 @@ map-resp-≗ → map f e ≈ map g e map-resp-≗ f≗g .≡arity = ≡.refl map-resp-≗ f≗g .≡label = HL.≈-reflexive ≡.refl -map-resp-≗ f≗g {e} .≡ports = ≈-reflexive (VecProps.map-cong f≗g (ports e)) +map-resp-≗ {g = g} f≗g {e} .≡ports i = ≡.trans (f≗g (ports e i)) (≡.cong (g ∘ ports e) (≡.sym (cast-is-id ≡.refl i))) Edge : Functor Nat (Setoids ℓ ℓ) Edge .F₀ = Edgeₛ Edge .F₁ = mapₛ Edge .identity = map-id -Edge .homomorphism = map-∘ _ _ +Edge .homomorphism {f = f} {g} = map-∘ f g Edge .F-resp-≈ = map-resp-≗ diff --git a/Functor/Monoidal/Construction/MultisetOf.agda b/Functor/Monoidal/Construction/MultisetOf.agda index eca7b3a..83bdf52 100644 --- a/Functor/Monoidal/Construction/MultisetOf.agda +++ b/Functor/Monoidal/Construction/MultisetOf.agda @@ -81,9 +81,9 @@ open SymmetricMonoidalFunctor module ListOf,++,[] = MonoidalFunctor ListOf,++,[] -BagOf,++,[] : SymmetricMonoidalFunctor 𝒞-SMC S -BagOf,++,[] .F = List∘G -BagOf,++,[] .isBraidedMonoidal = record +MultisetOf,++,[] : SymmetricMonoidalFunctor 𝒞-SMC S +MultisetOf,++,[] .F = List∘G +MultisetOf,++,[] .isBraidedMonoidal = record { isMonoidal = ListOf,++,[].isMonoidal ; braiding-compat = ++-⊗-σ } diff --git a/Functor/Monoidal/Instance/Nat/Circ.agda b/Functor/Monoidal/Instance/Nat/Circ.agda index 9d38127..0e2d3eb 100644 --- a/Functor/Monoidal/Instance/Nat/Circ.agda +++ b/Functor/Monoidal/Instance/Nat/Circ.agda @@ -46,29 +46,29 @@ Nat-Cocartesian-Category : CocartesianCategory 0ℓ 0ℓ 0ℓ Nat-Cocartesian-Category = record { cocartesian = Nat-Cocartesian } open import Functor.Monoidal.Construction.MultisetOf - {𝒞 = Nat-Cocartesian-Category} (Edge Gates) FreeCMonoid using (BagOf,++,[]) + {𝒞 = Nat-Cocartesian-Category} (Edge Gates) FreeCMonoid using (MultisetOf,++,[]) open Lax using (SymmetricMonoidalFunctor) -module BagOf,++,[] = SymmetricMonoidalFunctor BagOf,++,[] +module MultisetOf,++,[] = SymmetricMonoidalFunctor MultisetOf,++,[] open SymmetricMonoidalFunctor ε⇒ : SingletonSetoid ⟶ₛ Circuitₛ 0 -ε⇒ = mkCircuitₛ ∙ BagOf,++,[].ε +ε⇒ = mkCircuitₛ ∙ MultisetOf,++,[].ε open Cocartesian Nat-Cocartesian using (-+-) open Func η : {n m : ℕ} → Circuitₛ n ×ₛ Circuitₛ m ⟶ₛ Circuitₛ (n + m) -η {n} {m} .to (mkCircuit X , mkCircuit Y) = mkCircuit (BagOf,++,[].⊗-homo.η (n , m) ⟨$⟩ (X , Y)) -η {n} {m} .cong (mk≈ x , mk≈ y) = mk≈ (cong (BagOf,++,[].⊗-homo.η (n , m)) (x , y)) +η {n} {m} .to (mkCircuit X , mkCircuit Y) = mkCircuit (MultisetOf,++,[].⊗-homo.η (n , m) ⟨$⟩ (X , Y)) +η {n} {m} .cong (mk≈ x , mk≈ y) = mk≈ (cong (MultisetOf,++,[].⊗-homo.η (n , m)) (x , y)) ⊗-homomorphism : NaturalTransformation (-×- ∘F (Circ ⁂ Circ)) (Circ ∘F -+-) ⊗-homomorphism = ntHelper record { η = λ (n , m) → η {n} {m} - ; commute = λ { (f , g) {mkCircuit X , mkCircuit Y} → mk≈ (BagOf,++,[].⊗-homo.commute (f , g) {X , Y}) } + ; commute = λ { (f , g) {mkCircuit X , mkCircuit Y} → mk≈ (MultisetOf,++,[].⊗-homo.commute (f , g) {X , Y}) } } Circ,⊗,ε : SymmetricMonoidalFunctor Nat,+,0 Setoids-× @@ -78,10 +78,10 @@ Circ,⊗,ε .isBraidedMonoidal = record { ε = ε⇒ ; ⊗-homo = ⊗-homomorphism ; associativity = λ { {n} {m} {o} {(mkCircuit x , mkCircuit y) , mkCircuit z} → - mk≈ (BagOf,++,[].associativity {n} {m} {o} {(x , y) , z}) } - ; unitaryˡ = λ { {n} {_ , mkCircuit x} → mk≈ (BagOf,++,[].unitaryˡ {n} {_ , x}) } - ; unitaryʳ = λ { {n} {mkCircuit x , _} → mk≈ (BagOf,++,[].unitaryʳ {n} {x , _}) } + mk≈ (MultisetOf,++,[].associativity {n} {m} {o} {(x , y) , z}) } + ; unitaryˡ = λ { {n} {_ , mkCircuit x} → mk≈ (MultisetOf,++,[].unitaryˡ {n} {_ , x}) } + ; unitaryʳ = λ { {n} {mkCircuit x , _} → mk≈ (MultisetOf,++,[].unitaryʳ {n} {x , _}) } } ; braiding-compat = λ { {n} {m} {mkCircuit x , mkCircuit y} → - mk≈ (BagOf,++,[].braiding-compat {n} {m} {x , y}) } + mk≈ (MultisetOf,++,[].braiding-compat {n} {m} {x , y}) } } |