blob: 5de8f84d241885209afa1205e6d94686bd104570 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
{-# 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-≗
|
