4 files changed, 106 insertions, 9 deletions
diff --git a/Functor/Instance/FreeMonoid.agda b/Functor/Instance/FreeMonoid.agda
new file mode 100644
index 0000000..bb26fd4
--- /dev/null
+++ b/Functor/Instance/FreeMonoid.agda
@@ -0,0 +1,64 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; _⊔_)
+
+module Functor.Instance.FreeMonoid {c ℓ : Level} where
+
+import Categories.Object.Monoid as MonoidObject
+
+open import Categories.Category.Construction.Monoids using (Monoids)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Categories.Functor using (Functor)
+open import Categories.NaturalTransformation using (NaturalTransformation)
+open import Category.Instance.Setoids.SymmetricMonoidal {c} {c ⊔ ℓ} using (Setoids-×)
+open import Data.List.Properties using (++-assoc; ++-identityˡ; ++-identityʳ)
+open import Data.Product using (_,_)
+open import Function using (_⟶ₛ_)
+open import Functor.Instance.List {c} {ℓ} using (List)
+open import NaturalTransformation.Instance.EmptyList {c} {ℓ} using (⊤⇒[])
+open import NaturalTransformation.Instance.ListAppend {c} {ℓ} using (++)
+open import Relation.Binary using (Setoid)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+
+module List = Functor List
+module Setoids-× = SymmetricMonoidalCategory Setoids-×
+module ++ = NaturalTransformation ++
+module ⊤⇒[] = NaturalTransformation ⊤⇒[]
+
+open Functor
+open MonoidObject Setoids-×.monoidal using (Monoid; IsMonoid; Monoid⇒)
+open IsMonoid
+
+module _ (X : Setoid c ℓ) where
+
+  private
+    module X = Setoid X
+    module ListX = Setoid (List.₀ X)
+
+  ListMonoid : IsMonoid (List.₀ X)
+  ListMonoid .μ = ++.η X
+  ListMonoid .η = ⊤⇒[].η X
+  ListMonoid .assoc {(x , y) , z} = ListX.reflexive (++-assoc x y z)
+  ListMonoid .identityˡ {_ , x} = ListX.reflexive (++-identityˡ x)
+  ListMonoid .identityʳ {x , _} = ListX.reflexive (≡.sym (++-identityʳ x))
+
+FreeMonoid₀ : (X : Setoid c ℓ) → Monoid
+FreeMonoid₀ X = record { isMonoid = ListMonoid X }
+
+FreeMonoid₁
+    : {A B : Setoid c ℓ}
+      (f : A ⟶ₛ B)
+    → Monoid⇒ (FreeMonoid₀ A) (FreeMonoid₀ B)
+FreeMonoid₁ f = record
+    { arr = List.₁ f
+    ; preserves-μ = λ {x,y} → ++.sym-commute f {x,y}
+    ; preserves-η = ⊤⇒[].commute f
+    }
+
+FreeMonoid : Functor (Setoids c ℓ) (Monoids Setoids-×.monoidal)
+FreeMonoid .F₀ = FreeMonoid₀
+FreeMonoid .F₁ = FreeMonoid₁
+FreeMonoid .identity {X} = List.identity {X}
+FreeMonoid .homomorphism {X} {Y} {Z} {f} {g} = List.homomorphism {X} {Y} {Z} {f} {g}
+FreeMonoid .F-resp-≈ {A} {B} {f} {g} = List.F-resp-≈ {A} {B} {f} {g}
diff --git a/Functor/Instance/List.agda b/Functor/Instance/List.agda
index 05db349..b40670d 100644
--- a/Functor/Instance/List.agda
+++ b/Functor/Instance/List.agda
@@ -16,7 +16,7 @@ open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
 open import Relation.Binary using (Setoid)
 
 open Functor
-open Setoid
+open Setoid using (reflexive)
 open Func
 
 private
@@ -36,15 +36,19 @@ 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)
 
-map-id : (xs : ∣ Listₛ A ∣) → PW.Pointwise (_≈_ A) (List.map id xs) xs
-map-id {A} = PW.map (reflexive A) ∘ PW.≡⇒Pointwise-≡ ∘ ListProps.map-id
+map-id
+    : (xs : ∣ Listₛ A ∣)
+    → (open Setoid (Listₛ A))
+    → List.map id xs ≈ xs
+map-id {A} = reflexive (Listₛ A) ∘ ListProps.map-id
 
 List-homo
     : (f : A ⟶ₛ B)
       (g : B ⟶ₛ C)
     → (xs : ∣ Listₛ A ∣)
-    → PW.Pointwise (_≈_ C) (List.map (to g ∘ to f) xs) (List.map (to g) (List.map (to f) xs))
-List-homo {C = C} f g = PW.map (reflexive C) ∘ PW.≡⇒Pointwise-≡ ∘ ListProps.map-∘
+    → (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-∘
 
 List : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ))
 List .F₀ = Listₛ
diff --git a/Functor/Instance/Nat/Circ.agda b/Functor/Instance/Nat/Circ.agda
new file mode 100644
index 0000000..0f18c4c
--- /dev/null
+++ b/Functor/Instance/Nat/Circ.agda
@@ -0,0 +1,32 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; _⊔_; 0ℓ)
+
+module Functor.Instance.Nat.Circ {c ℓ : Level} where
+
+open import Data.Circuit {c} {ℓ} using (Circuitₛ; mapₛ; mkCircuitₛ)
+open import Data.Nat using (ℕ)
+open import Relation.Binary using (Setoid)
+open import Function using (Func)
+open import Categories.Functor using (Functor; _∘F_)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Category.Instance.Nat using (Nat)
+open import Data.Fin using (Fin)
+open import Data.Circuit.Gate using (Gates)
+open import Functor.Instance.Nat.Edge Gates using (Edge)
+open import Functor.Instance.List using (List)
+
+List∘Edge : Functor Nat (Setoids 0ℓ 0ℓ)
+List∘Edge = List ∘F Edge
+
+module List∘Edge = Functor List∘Edge
+
+open Func
+open Functor
+
+Circ : Functor Nat (Setoids c (c ⊔ ℓ))
+Circ .F₀ = Circuitₛ
+Circ .F₁ = mapₛ
+Circ .identity = cong mkCircuitₛ List∘Edge.identity
+Circ .homomorphism = cong mkCircuitₛ List∘Edge.homomorphism
+Circ .F-resp-≈ f≗g = cong mkCircuitₛ (List∘Edge.F-resp-≈ f≗g)
diff --git a/Functor/Instance/Nat/Edge.agda b/Functor/Instance/Nat/Edge.agda
index ee54f2e..618807d 100644
--- a/Functor/Instance/Nat/Edge.agda
+++ b/Functor/Instance/Nat/Edge.agda
@@ -11,7 +11,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.Hypergraph.Edge HL as Edge using (≈-Edge-IsEquivalence; map; ≈-Edge)
+open import Data.Hypergraph.Edge HL as Edge using (≈-Edge-IsEquivalence; map; ≈-Edge; Edgeₛ)
 open import Data.Nat using (ℕ)
 open import Data.Vec.Relation.Binary.Equality.Cast using (≈-cong′; ≈-reflexive)
 open import Level using (0ℓ)
@@ -27,9 +27,6 @@ open Functor
 open Setoid
 open ≈-Edge
 
-Edgeₛ : (v : ℕ) → Setoid 0ℓ 0ℓ
-Edgeₛ v = record { isEquivalence = ≈-Edge-IsEquivalence {v} }
-
 Edge₁ : {n m : ℕ} → (Fin n → Fin m) → Edgeₛ n ⟶ₛ Edgeₛ m
 Edge₁ f .to = map f
 Edge₁ f .cong x≈y = record