5 files changed, 53 insertions, 45 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-≗
diff --git a/Functor/Monoidal/Construction/MultisetOf.agda b/Functor/Monoidal/Construction/MultisetOf.agda
index eca7b3a..83bdf52 100644
--- a/Functor/Monoidal/Construction/MultisetOf.agda
+++ b/Functor/Monoidal/Construction/MultisetOf.agda
@@ -81,9 +81,9 @@ open SymmetricMonoidalFunctor
 
 module ListOf,++,[] = MonoidalFunctor ListOf,++,[]
 
-BagOf,++,[] : SymmetricMonoidalFunctor 𝒞-SMC S
-BagOf,++,[] .F = List∘G
-BagOf,++,[] .isBraidedMonoidal = record
+MultisetOf,++,[] : SymmetricMonoidalFunctor 𝒞-SMC S
+MultisetOf,++,[] .F = List∘G
+MultisetOf,++,[] .isBraidedMonoidal = record
     { isMonoidal = ListOf,++,[].isMonoidal
     ; braiding-compat = ++-⊗-σ
     }
diff --git a/Functor/Monoidal/Instance/Nat/Circ.agda b/Functor/Monoidal/Instance/Nat/Circ.agda
index 9d38127..0e2d3eb 100644
--- a/Functor/Monoidal/Instance/Nat/Circ.agda
+++ b/Functor/Monoidal/Instance/Nat/Circ.agda
@@ -46,29 +46,29 @@ Nat-Cocartesian-Category : CocartesianCategory 0ℓ 0ℓ 0ℓ
 Nat-Cocartesian-Category = record { cocartesian = Nat-Cocartesian }
 
 open import Functor.Monoidal.Construction.MultisetOf
-     {𝒞 = Nat-Cocartesian-Category} (Edge Gates) FreeCMonoid using (BagOf,++,[])
+     {𝒞 = Nat-Cocartesian-Category} (Edge Gates) FreeCMonoid using (MultisetOf,++,[])
 
 open Lax using (SymmetricMonoidalFunctor)
 
-module BagOf,++,[] = SymmetricMonoidalFunctor BagOf,++,[]
+module MultisetOf,++,[] = SymmetricMonoidalFunctor MultisetOf,++,[]
 
 open SymmetricMonoidalFunctor
 
 ε⇒ : SingletonSetoid ⟶ₛ Circuitₛ 0
-ε⇒ = mkCircuitₛ ∙ BagOf,++,[].ε
+ε⇒ = mkCircuitₛ ∙ MultisetOf,++,[].ε
 
 open Cocartesian Nat-Cocartesian using (-+-)
 
 open Func
 
 η : {n m : ℕ} → Circuitₛ n ×ₛ Circuitₛ m ⟶ₛ Circuitₛ (n + m)
-η {n} {m} .to (mkCircuit X , mkCircuit Y) = mkCircuit (BagOf,++,[].⊗-homo.η (n , m) ⟨$⟩ (X , Y))
-η {n} {m} .cong (mk≈ x , mk≈ y) = mk≈ (cong (BagOf,++,[].⊗-homo.η (n , m)) (x , y))
+η {n} {m} .to (mkCircuit X , mkCircuit Y) = mkCircuit (MultisetOf,++,[].⊗-homo.η (n , m) ⟨$⟩ (X , Y))
+η {n} {m} .cong (mk≈ x , mk≈ y) = mk≈ (cong (MultisetOf,++,[].⊗-homo.η (n , m)) (x , y))
 
 ⊗-homomorphism : NaturalTransformation (-×- ∘F (Circ ⁂ Circ)) (Circ ∘F -+-)
 ⊗-homomorphism = ntHelper record
     { η = λ (n , m) → η {n} {m}
-    ; commute = λ { (f , g) {mkCircuit X , mkCircuit Y} → mk≈ (BagOf,++,[].⊗-homo.commute (f , g) {X , Y}) }
+    ; commute = λ { (f , g) {mkCircuit X , mkCircuit Y} → mk≈ (MultisetOf,++,[].⊗-homo.commute (f , g) {X , Y}) }
     }
 
 Circ,⊗,ε : SymmetricMonoidalFunctor Nat,+,0 Setoids-×
@@ -78,10 +78,10 @@ Circ,⊗,ε .isBraidedMonoidal = record
         { ε = ε⇒
         ; ⊗-homo = ⊗-homomorphism
         ; associativity = λ { {n} {m} {o} {(mkCircuit x , mkCircuit y) , mkCircuit z} →
-                  mk≈ (BagOf,++,[].associativity {n} {m} {o} {(x , y) , z}) }
-        ; unitaryˡ = λ { {n} {_ , mkCircuit x} → mk≈ (BagOf,++,[].unitaryˡ {n} {_ , x}) }
-        ; unitaryʳ = λ { {n} {mkCircuit x , _} → mk≈ (BagOf,++,[].unitaryʳ {n} {x , _}) }
+                  mk≈ (MultisetOf,++,[].associativity {n} {m} {o} {(x , y) , z}) }
+        ; unitaryˡ = λ { {n} {_ , mkCircuit x} → mk≈ (MultisetOf,++,[].unitaryˡ {n} {_ , x}) }
+        ; unitaryʳ = λ { {n} {mkCircuit x , _} → mk≈ (MultisetOf,++,[].unitaryʳ {n} {x , _}) }
         }
     ; braiding-compat = λ { {n} {m} {mkCircuit x , mkCircuit y} →
-        mk≈ (BagOf,++,[].braiding-compat {n} {m} {x , y}) }
+        mk≈ (MultisetOf,++,[].braiding-compat {n} {m} {x , y}) }
     }