1 files changed, 60 insertions, 0 deletions
diff --git a/Functor/Instance/Nat/Edge.agda b/Functor/Instance/Nat/Edge.agda
new file mode 100644
index 0000000..c69a1db
--- /dev/null
+++ b/Functor/Instance/Nat/Edge.agda
@@ -0,0 +1,60 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Hypergraph.Label using (HypergraphLabel)
+open import Level using (Level; 0ℓ)
+
+module Functor.Instance.Nat.Edge {ℓ : Level} (HL : HypergraphLabel) where
+
+import Data.Vec as Vec
+import Data.Vec.Properties as VecProps
+
+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.Fin.Properties using (cast-is-id)
+open import Data.Hypergraph.Edge {ℓ} HL as Edge using (Edgeₛ; map; mapₛ; _≈_)
+open import Data.Nat using (ℕ)
+open import Data.Vec.Relation.Binary.Equality.Cast using (≈-reflexive)
+open import Function using (id; _∘_; Func; _⟶ₛ_)
+open import Relation.Binary using (Setoid)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
+
+module HL = HypergraphLabel HL
+
+open Edge.Edge
+open Edge._≈_
+open Func
+open Functor
+
+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 = ≡.cong (ports e) ∘ ≡.sym ∘ cast-is-id ≡.refl
+
+map-∘
+    : {n m o : ℕ}
+      (f : Fin n → Fin m)
+      (g : Fin m → Fin o)
+      {e : Edge.Edge n}
+    → 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 = ≡.cong (g ∘ f ∘ ports e) ∘ ≡.sym ∘ cast-is-id ≡.refl
+
+map-resp-≗
+    : {n m : ℕ}
+      {f g : Fin n → Fin m}
+    → f ≗ g
+    → {e : Edge.Edge n}
+    → map f e ≈ map g e
+map-resp-≗ f≗g .≡arity = ≡.refl
+map-resp-≗ f≗g .≡label = HL.≈-reflexive ≡.refl
+map-resp-≗ {g = g} f≗g {e} .≡ports i = ≡.trans (f≗g (ports e i)) (≡.cong (g ∘ ports e) (≡.sym (cast-is-id ≡.refl i)))
+
+Edge : Functor Nat (Setoids ℓ ℓ)
+Edge .F₀ = Edgeₛ
+Edge .F₁ = mapₛ
+Edge .identity = map-id
+Edge .homomorphism {f = f} {g} = map-∘ f g
+Edge .F-resp-≈ = map-resp-≗