Use functional vector in edge definition

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}) }
     }