From d2ce2675b5e0331b6bf5647a4fc195e458d9b5ee Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Thu, 30 Oct 2025 19:23:31 -0500 Subject: Add Circ functor --- Functor/Instance/Nat/Edge.agda | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) (limited to 'Functor/Instance/Nat/Edge.agda') 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 -- cgit v1.2.3