{-# 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.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 = ≈-reflexive (VecProps.map-id (ports e))

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 = ≈-reflexive (VecProps.map-∘ g f (ports e))

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-≗ f≗g {e} .≡ports = ≈-reflexive (VecProps.map-cong f≗g (ports e))

Edge : Functor Nat (Setoids ℓ ℓ)
Edge .F₀ = Edgeₛ
Edge .F₁ = mapₛ
Edge .identity = map-id
Edge .homomorphism = map-∘ _ _
Edge .F-resp-≈ = map-resp-≗