Use permutation for equivalence of hypergraphs

2 files changed, 6 insertions, 7 deletions

diff --git a/Functor/Instance/Nat/Circ.agda b/Functor/Instance/Nat/Circ.agda
index 0f18c4c..d5bcc9b 100644
--- a/Functor/Instance/Nat/Circ.agda
+++ b/Functor/Instance/Nat/Circ.agda
@@ -24,7 +24,7 @@ module List∘Edge = Functor List∘Edge
 open Func
 open Functor
 
-Circ : Functor Nat (Setoids c (c ⊔ ℓ))
+Circ : Functor Nat (Setoids c ℓ)
 Circ .F₀ = Circuitₛ
 Circ .F₁ = mapₛ
 Circ .identity = cong mkCircuitₛ List∘Edge.identity
diff --git a/Functor/Instance/Nat/Edge.agda b/Functor/Instance/Nat/Edge.agda
index 618807d..f8d47c2 100644
--- a/Functor/Instance/Nat/Edge.agda
+++ b/Functor/Instance/Nat/Edge.agda
@@ -11,7 +11,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.Hypergraph.Edge HL as Edge using (≈-Edge-IsEquivalence; map; ≈-Edge; Edgeₛ)
+open import Data.Hypergraph.Edge HL as Edge using (Edgeₛ; map; _≈_)
 open import Data.Nat using (ℕ)
 open import Data.Vec.Relation.Binary.Equality.Cast using (≈-cong′; ≈-reflexive)
 open import Level using (0ℓ)
@@ -22,10 +22,9 @@ open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
 module HL = HypergraphLabel HL
 
 open Edge.Edge
+open Edge._≈_
 open Func
 open Functor
-open Setoid
-open ≈-Edge
 
 Edge₁ : {n m : ℕ} → (Fin n → Fin m) → Edgeₛ n ⟶ₛ Edgeₛ m
 Edge₁ f .to = map f
@@ -35,7 +34,7 @@ Edge₁ f .cong x≈y = record
     ; ≡ports = ≈-cong′ (Vec.map f) (≡ports x≈y)
     }
 
-map-id : {v : ℕ} {e : Edge.Edge v} → ≈-Edge (map id e) e
+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))
@@ -45,7 +44,7 @@ map-∘
       (f : Fin n → Fin m)
       (g : Fin m → Fin o)
       {e : Edge.Edge n}
-    → ≈-Edge (map (g ∘ f) e) (map g (map f e))
+    → 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))
@@ -55,7 +54,7 @@ map-resp-≗
       {f g : Fin n → Fin m}
     → f ≗ g
     → {e : Edge.Edge n}
-    → ≈-Edge (map f e) (map g e)
+    → 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))