diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-10-30 19:23:31 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-10-30 19:23:31 -0500 |
| commit | d2ce2675b5e0331b6bf5647a4fc195e458d9b5ee (patch) | |
| tree | acf00b930c01778fc520ffe99fd046615cf2f3a5 /Functor/Instance/Nat/Edge.agda | |
| parent | e90c54ce55d36019d32e239509ff5f96c5dff2b3 (diff) | |
Add Circ functormain
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 |