Use functional vector in edge definition

3 files changed, 40 insertions, 32 deletions

diff --git a/Functor/Instance/List.agda b/Functor/Instance/List.agda
index b40670d..ceb73e1 100644
--- a/Functor/Instance/List.agda
+++ b/Functor/Instance/List.agda
@@ -4,13 +4,12 @@ open import Level using (Level; _⊔_)
 
 module Functor.Instance.List {c ℓ : Level} where
 
-import Data.List as List
 import Data.List.Properties as ListProps
 import Data.List.Relation.Binary.Pointwise as PW
 
 open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Functor using (Functor)
-open import Data.Setoid using (∣_∣)
+open import Data.Setoid using (∣_∣; _⇒ₛ_)
 open import Function.Base using (_∘_; id)
 open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
 open import Relation.Binary using (Setoid)
@@ -19,40 +18,48 @@ open Functor
 open Setoid using (reflexive)
 open Func
 
+open import Data.Opaque.List as List hiding (List)
+
 private
   variable
     A B C : Setoid c ℓ
 
--- the List functor takes a carrier A to lists of A
--- and the equivalence on A to pointwise equivalence on lists of A
+open import Function.Construct.Identity using () renaming (function to Id)
+open import Function.Construct.Setoid using (_∙_)
 
-Listₛ : Setoid c ℓ → Setoid c (c ⊔ ℓ)
-Listₛ = PW.setoid
+opaque
 
--- List on morphisms is the familiar map operation
--- which applies the same function to every element of a list
+  unfolding List.List
+
+  map-id
+      : (xs : ∣ Listₛ A ∣)
+      → (open Setoid (Listₛ A))
+      → mapₛ (Id _) ⟨$⟩ xs ≈ xs
+  map-id {A} = reflexive (Listₛ A) ∘ ListProps.map-id
 
-mapₛ : A ⟶ₛ B → Listₛ A ⟶ₛ Listₛ B
-mapₛ f .to = List.map (to f)
-mapₛ f .cong = PW.map⁺ (to f) (to f) ∘ PW.map (cong f)
+  List-homo
+      : (f : A ⟶ₛ B)
+        (g : B ⟶ₛ C)
+      → (xs : ∣ Listₛ A ∣)
+      → (open Setoid (Listₛ C))
+      → mapₛ (g ∙ f) ⟨$⟩ xs ≈ mapₛ g ⟨$⟩ (mapₛ f ⟨$⟩ xs)
+  List-homo {C = C} f g = reflexive (Listₛ C) ∘ ListProps.map-∘
 
-map-id
-    : (xs : ∣ Listₛ A ∣)
-    → (open Setoid (Listₛ A))
-    → List.map id xs ≈ xs
-map-id {A} = reflexive (Listₛ A) ∘ ListProps.map-id
+  List-resp-≈
+      : (f g : A ⟶ₛ B)
+      → (let open Setoid (A ⇒ₛ B) in f ≈ g)
+      → (let open Setoid (Listₛ A ⇒ₛ Listₛ B) in mapₛ f ≈ mapₛ g)
+  List-resp-≈ f g f≈g = PW.map⁺ (to f) (to g) (PW.refl f≈g)
 
-List-homo
-    : (f : A ⟶ₛ B)
-      (g : B ⟶ₛ C)
-    → (xs : ∣ Listₛ A ∣)
-    → (open Setoid (Listₛ C))
-    → List.map (to g ∘ to f) xs ≈ List.map (to g) (List.map (to f) xs)
-List-homo {C = C} f g = reflexive (Listₛ C) ∘ ListProps.map-∘
+-- the List functor takes a carrier A to lists of A
+-- and the equivalence on A to pointwise equivalence on lists of A
+
+-- List on morphisms is the familiar map operation
+-- which applies the same function to every element of a list
 
 List : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ))
-List .F₀ = Listₛ
-List .F₁ = mapₛ
-List .identity {A} {xs} = map-id {A} xs
+List .F₀ = List.Listₛ
+List .F₁ = List.mapₛ
+List .identity {_} {xs} = map-id xs
 List .homomorphism {f = f} {g} {xs} = List-homo f g xs
-List .F-resp-≈ {A} {B} {f} {g} f≈g = PW.map⁺ (to f) (to g) (PW.refl f≈g)
+List .F-resp-≈ {f = f} {g} f≈g = List-resp-≈ f g f≈g
diff --git a/Functor/Instance/Nat/Circ.agda b/Functor/Instance/Nat/Circ.agda
index 09bc495..36d726d 100644
--- a/Functor/Instance/Nat/Circ.agda
+++ b/Functor/Instance/Nat/Circ.agda
@@ -28,5 +28,5 @@ Circ : Functor Nat (Setoids ℓ ℓ)
 Circ .F₀ = Circuitₛ
 Circ .F₁ = mapₛ
 Circ .identity = cong mkCircuitₛ Multiset∘Edge.identity
-Circ .homomorphism = cong mkCircuitₛ Multiset∘Edge.homomorphism
+Circ .homomorphism {f = f} {g = g} = cong mkCircuitₛ (Multiset∘Edge.homomorphism {f = f} {g = g})
 Circ .F-resp-≈ f≗g = cong mkCircuitₛ (Multiset∘Edge.F-resp-≈ f≗g)
diff --git a/Functor/Instance/Nat/Edge.agda b/Functor/Instance/Nat/Edge.agda
index 5de8f84..c69a1db 100644
--- a/Functor/Instance/Nat/Edge.agda
+++ b/Functor/Instance/Nat/Edge.agda
@@ -12,6 +12,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.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)
@@ -29,7 +30,7 @@ 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-id {_} {e} .≡ports = ≡.cong (ports e) ∘ ≡.sym ∘ cast-is-id ≡.refl
 
 map-∘
     : {n m o : ℕ}
@@ -39,7 +40,7 @@ map-∘
     → 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-∘ f g {e} .≡ports = ≡.cong (g ∘ f ∘ ports e) ∘ ≡.sym ∘ cast-is-id ≡.refl
 
 map-resp-≗
     : {n m : ℕ}
@@ -49,11 +50,11 @@ map-resp-≗
     → 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))
+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 = map-∘ _ _
+Edge .homomorphism {f = f} {g} = map-∘ f g
 Edge .F-resp-≈ = map-resp-≗