diff options
Diffstat (limited to 'Functor/Instance/Nat/Edge.agda')
| -rw-r--r-- | Functor/Instance/Nat/Edge.agda | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/Functor/Instance/Nat/Edge.agda b/Functor/Instance/Nat/Edge.agda index ee54f2e..618807d 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) +open import Data.Hypergraph.Edge HL as Edge using (≈-Edge-IsEquivalence; map; ≈-Edge; Edgeₛ) open import Data.Nat using (ℕ) open import Data.Vec.Relation.Binary.Equality.Cast using (≈-cong′; ≈-reflexive) open import Level using (0ℓ) @@ -27,9 +27,6 @@ open Functor open Setoid open ≈-Edge -Edgeₛ : (v : ℕ) → Setoid 0ℓ 0ℓ -Edgeₛ v = record { isEquivalence = ≈-Edge-IsEquivalence {v} } - Edge₁ : {n m : ℕ} → (Fin n → Fin m) → Edgeₛ n ⟶ₛ Edgeₛ m Edge₁ f .to = map f Edge₁ f .cong x≈y = record |