1 files changed, 113 insertions, 0 deletions
diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda
new file mode 100644
index 0000000..447f008
--- /dev/null
+++ b/Data/Hypergraph/Edge.agda
@@ -0,0 +1,113 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Hypergraph.Label using (HypergraphLabel)
+
+open import Level using (Level; 0ℓ)
+module Data.Hypergraph.Edge {ℓ : Level} (HL : HypergraphLabel) where
+
+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 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 Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
+open import Function using (_⟶ₛ_; Func; _∘_)
+
+module HL = HypergraphLabel HL
+
+open HL using (Label)
+open Vec using (Vector)
+open Func
+
+record Edge (v : ℕ) : Set ℓ where
+  constructor mkEdge
+  field
+    {arity} : ℕ
+    label : Label arity
+    ports : Fin arity → Fin v
+
+map : {n m : ℕ} → (Fin n → Fin m) → Edge n → Edge m
+map f edge = record
+    { label = label
+    ; ports = Vec.map f ports
+    }
+  where
+    open Edge edge
+
+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≈
+    module E = Edge E
+    module E′ = Edge E′
+    field
+      ≡arity : E.arity ≡ E′.arity
+      ≡label : HL.cast ≡arity E.label ≡ E′.label
+      ≡ports : E.ports ≋ E′.ports ∘ Fin.cast ≡arity
+
+  ≈-refl : {x : Edge v} → x ≈ x
+  ≈-refl {x} = record
+      { ≡arity = ≡.refl
+      ; ≡label = HL.≈-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 = ≡.sym ∘ ≡ports-sym
+      }
+    where
+      open _≈_ x≈y
+      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 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
+      { refl = ≈-refl
+      ; sym = ≈-sym
+      ; trans = ≈-trans
+      }
+
+  show : Edge v → String
+  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 (≡.cong f ∘ ≡p)