6 files changed, 451 insertions, 0 deletions
diff --git a/Functor/Instance/Nat/Circ.agda b/Functor/Instance/Nat/Circ.agda
new file mode 100644
index 0000000..88a6ec6
--- /dev/null
+++ b/Functor/Instance/Nat/Circ.agda
@@ -0,0 +1,56 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+module Functor.Instance.Nat.Circ {ℓ : Level} where
+
+import Data.List.Relation.Binary.Permutation.Setoid as ↭
+
+open import Categories.Category.Instance.Nat using (Nat)
+open import Categories.Functor using (Functor; _∘F_)
+open import Categories.Morphism.Notation using (_[_≅_])
+open import Category.Instance.Setoids.SymmetricMonoidal {ℓ} {ℓ} using (Setoids-×)
+open import Data.Circuit using (mk≈)
+open import Data.Circuit {ℓ} using (Circuitₛ; mkCircuitₛ; edgesₛ)
+open import Data.Circuit.Gate using (Gates)
+open import Data.Nat using (ℕ)
+open import Data.Opaque.Multiset using (Multisetₛ)
+open import Data.Product using (proj₁; proj₂; Σ-syntax)
+open import Functor.Free.Instance.CMonoid using (Free)
+open import Functor.Instance.Nat.Edge {ℓ} Gates using (Edge)
+open import Functor.Properties using (define-by-pw-iso)
+
+open import Category.Construction.CMonoids Setoids-×.symmetric using (CMonoids)
+open import Category.Construction.CMonoids.Properties Setoids-×.symmetric using (transport-by-iso)
+open import Object.Monoid.Commutative Setoids-×.symmetric using (CommutativeMonoid)
+
+Edges : Functor Nat CMonoids
+Edges = Free ∘F Edge
+
+module Edges = Functor Edges
+module Edge = Functor Edge
+
+opaque
+  unfolding Multisetₛ
+  Edges≅Circₛ : (n : ℕ) → Setoids-×.U [ Multisetₛ (Edge.₀ n) ≅ Circuitₛ n ]
+  Edges≅Circₛ n = record
+      { from = mkCircuitₛ
+      ; to = edgesₛ
+      ; iso = record
+          { isoˡ = ↭.↭-refl (Edge.₀ n)
+          ; isoʳ = mk≈ (↭.↭-refl (Edge.₀ n))
+          }
+      }
+
+private
+  Edges≅ : (n : ℕ) → Σ[ M ∈ CommutativeMonoid ] CMonoids [ Edges.₀ n ≅ M ]
+  Edges≅ n = transport-by-iso (Edges.₀ n) (Edges≅Circₛ n)
+
+Circuitₘ : ℕ → CommutativeMonoid
+Circuitₘ n = proj₁ (Edges≅ n)
+
+Edges≅Circₘ : (n : ℕ) → CMonoids [ Edges.₀ n ≅ Circuitₘ n ]
+Edges≅Circₘ n = proj₂ (Edges≅ n)
+
+Circ : Functor Nat CMonoids
+Circ = proj₁ (define-by-pw-iso Edges Circuitₘ Edges≅Circₘ)
diff --git a/Functor/Instance/Nat/Edge.agda b/Functor/Instance/Nat/Edge.agda
new file mode 100644
index 0000000..c69a1db
--- /dev/null
+++ b/Functor/Instance/Nat/Edge.agda
@@ -0,0 +1,60 @@
+{-# 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.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)
+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 = ≡.cong (ports e) ∘ ≡.sym ∘ cast-is-id ≡.refl
+
+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 = ≡.cong (g ∘ f ∘ ports e) ∘ ≡.sym ∘ cast-is-id ≡.refl
+
+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-≗ {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 {f = f} {g} = map-∘ f g
+Edge .F-resp-≈ = map-resp-≗
diff --git a/Functor/Instance/Nat/Preimage.agda b/Functor/Instance/Nat/Preimage.agda
new file mode 100644
index 0000000..7da00f4
--- /dev/null
+++ b/Functor/Instance/Nat/Preimage.agda
@@ -0,0 +1,65 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Instance.Nat.Preimage where
+
+open import Categories.Category.Instance.Nat using (Natop)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Functor using (Functor)
+open import Data.Fin.Base using (Fin)
+open import Data.Bool.Base using (Bool)
+open import Data.Nat.Base using (ℕ)
+open import Data.Subset.Functional using (Subset)
+open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid)
+open import Function.Base using (id; _∘_)
+open import Function.Bundles using (Func; _⟶ₛ_)
+open import Function.Construct.Identity using () renaming (function to Id)
+open import Function.Construct.Setoid using (setoid; _∙_)
+open import Level using (0ℓ)
+open import Relation.Binary using (Rel; Setoid)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
+
+open Functor
+open Func
+
+_≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ
+_≈_ {X} {Y} = Setoid._≈_ (setoid X Y)
+infixr 4 _≈_
+
+private
+  variable A B C : ℕ
+
+-- action on objects (Subset n)
+Subsetₛ : ℕ → Setoid 0ℓ 0ℓ
+Subsetₛ = ≋-setoid (≡.setoid Bool)
+
+-- action of Preimage on morphisms (contravariant)
+Preimage₁ : (Fin A → Fin B) → Subsetₛ B ⟶ₛ Subsetₛ A
+to (Preimage₁ f) i = i ∘ f
+cong (Preimage₁ f) x≗y = x≗y ∘ f
+
+-- Preimage respects identity
+Preimage-identity : Preimage₁ id ≈ Id (Subsetₛ A)
+Preimage-identity {A} = Setoid.refl (Subsetₛ A)
+
+-- Preimage flips composition
+Preimage-homomorphism
+    : {A B C : ℕ}
+      (f : Fin A → Fin B)
+      (g : Fin B → Fin C)
+    → Preimage₁ (g ∘ f) ≈ Preimage₁ f ∙ Preimage₁ g
+Preimage-homomorphism {A} _ _ = Setoid.refl (Subsetₛ A)
+
+-- Preimage respects equality
+Preimage-resp-≈
+    : {f g : Fin A → Fin B}
+    → f ≗ g
+    → Preimage₁ f ≈ Preimage₁ g
+Preimage-resp-≈ f≗g {v} = ≡.cong v ∘ f≗g
+
+-- the Preimage functor
+Preimage : Functor Natop (Setoids 0ℓ 0ℓ)
+F₀ Preimage = Subsetₛ
+F₁ Preimage = Preimage₁
+identity Preimage = Preimage-identity
+homomorphism Preimage {f = f} {g} {v} = Preimage-homomorphism g f {v}
+F-resp-≈ Preimage = Preimage-resp-≈
diff --git a/Functor/Instance/Nat/Pull.agda b/Functor/Instance/Nat/Pull.agda
new file mode 100644
index 0000000..b1764d9
--- /dev/null
+++ b/Functor/Instance/Nat/Pull.agda
@@ -0,0 +1,81 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Instance.Nat.Pull where
+
+open import Categories.Category.Instance.Nat using (Natop)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Functor using (Functor)
+open import Data.Fin.Base using (Fin)
+open import Data.Nat.Base using (ℕ)
+open import Function.Base using (id; _∘_)
+open import Function.Bundles using (Func; _⟶ₛ_)
+open import Function.Construct.Identity using () renaming (function to Id)
+open import Function.Construct.Setoid using (setoid; _∙_)
+open import Level using (0ℓ)
+open import Relation.Binary using (Rel; Setoid)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
+open import Data.Circuit.Value using (Monoid)
+open import Data.System.Values Monoid using (Values)
+open import Data.Unit using (⊤; tt)
+
+open Functor
+open Func
+
+-- Pull takes a natural number n to the setoid Values n
+
+private
+
+  variable A B C : ℕ
+
+  _≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ
+  _≈_ {X} {Y} = Setoid._≈_ (setoid X Y)
+
+  infixr 4 _≈_
+
+  opaque
+
+    unfolding Values
+
+    -- action of Pull on morphisms (contravariant)
+    Pull₁ : (Fin A → Fin B) → Values B ⟶ₛ Values A
+    to (Pull₁ f) i = i ∘ f
+    cong (Pull₁ f) x≗y = x≗y ∘ f
+
+    -- Pull respects identity
+    Pull-identity : Pull₁ id ≈ Id (Values A)
+    Pull-identity {A} = Setoid.refl (Values A)
+
+  opaque
+
+    unfolding Pull₁
+
+    -- Pull flips composition
+    Pull-homomorphism
+        : (f : Fin A → Fin B)
+          (g : Fin B → Fin C)
+        → Pull₁ (g ∘ f) ≈ Pull₁ f ∙ Pull₁ g
+    Pull-homomorphism {A} _ _ = Setoid.refl (Values A)
+
+    -- Pull respects equality
+    Pull-resp-≈
+        : {f g : Fin A → Fin B}
+        → f ≗ g
+        → Pull₁ f ≈ Pull₁ g
+    Pull-resp-≈ f≗g {v} = ≡.cong v ∘ f≗g
+
+opaque
+
+  unfolding Pull₁
+
+  Pull-defs : ⊤
+  Pull-defs = tt
+
+-- the Pull functor
+Pull : Functor Natop (Setoids 0ℓ 0ℓ)
+F₀ Pull = Values
+F₁ Pull = Pull₁
+identity Pull = Pull-identity
+homomorphism Pull {f = f} {g} = Pull-homomorphism g f
+F-resp-≈ Pull = Pull-resp-≈
+
+module Pull = Functor Pull
diff --git a/Functor/Instance/Nat/Push.agda b/Functor/Instance/Nat/Push.agda
new file mode 100644
index 0000000..8126006
--- /dev/null
+++ b/Functor/Instance/Nat/Push.agda
@@ -0,0 +1,79 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Instance.Nat.Push where
+
+open import Categories.Functor using (Functor)
+open import Categories.Category.Instance.Nat using (Nat)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Data.Circuit.Merge using (merge; merge-cong₁; merge-cong₂; merge-⁅⁆; merge-preimage)
+open import Data.Fin.Base using (Fin)
+open import Data.Fin.Preimage using (preimage; preimage-cong₁)
+open import Data.Nat.Base using (ℕ)
+open import Data.Subset.Functional using (⁅_⁆)
+open import Function.Base using (id; _∘_)
+open import Function.Bundles using (Func; _⟶ₛ_)
+open import Function.Construct.Identity using () renaming (function to Id)
+open import Function.Construct.Setoid using (setoid; _∙_)
+open import Level using (0ℓ)
+open import Relation.Binary using (Rel; Setoid)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
+open import Data.Circuit.Value using (Monoid)
+open import Data.System.Values Monoid using (Values)
+open import Data.Unit using (⊤; tt)
+
+open Func
+open Functor
+
+-- Push sends a natural number n to Values n
+
+private
+
+  variable A B C : ℕ
+
+  _≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ
+  _≈_ {X} {Y} = Setoid._≈_ (setoid X Y)
+  infixr 4 _≈_
+
+  opaque
+
+    unfolding Values
+
+    -- action of Push on morphisms (covariant)
+    Push₁ : (Fin A → Fin B) → Values A ⟶ₛ Values B
+    to (Push₁ f) v = merge v ∘ preimage f ∘ ⁅_⁆
+    cong (Push₁ f) x≗y = merge-cong₁ x≗y ∘ preimage f ∘ ⁅_⁆
+
+    -- Push respects identity
+    Push-identity : Push₁ id ≈ Id (Values A)
+    Push-identity {_} {v} = merge-⁅⁆ v
+
+    -- Push respects composition
+    Push-homomorphism
+        : {f : Fin A → Fin B}
+          {g : Fin B → Fin C}
+        → Push₁ (g ∘ f) ≈ Push₁ g ∙ Push₁ f
+    Push-homomorphism {f = f} {g} {v} = merge-preimage f v ∘ preimage g ∘ ⁅_⁆
+
+    -- Push respects equality
+    Push-resp-≈
+        : {f g : Fin A → Fin B}
+        → f ≗ g
+        → Push₁ f ≈ Push₁ g
+    Push-resp-≈ f≗g {v} = merge-cong₂ v ∘ preimage-cong₁ f≗g ∘ ⁅_⁆
+
+opaque
+
+  unfolding Push₁
+
+  Push-defs : ⊤
+  Push-defs = tt
+
+-- the Push functor
+Push : Functor Nat (Setoids 0ℓ 0ℓ)
+F₀ Push = Values
+F₁ Push = Push₁
+identity Push = Push-identity
+homomorphism Push = Push-homomorphism
+F-resp-≈ Push = Push-resp-≈
+
+module Push = Functor Push
diff --git a/Functor/Instance/Nat/System.agda b/Functor/Instance/Nat/System.agda
new file mode 100644
index 0000000..05e1e7b
--- /dev/null
+++ b/Functor/Instance/Nat/System.agda
@@ -0,0 +1,110 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Instance.Nat.System where
+
+
+open import Level using (suc; 0ℓ)
+
+open import Categories.Category.Instance.Nat using (Nat)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Functor.Core using (Functor)
+open import Data.Circuit.Value using (Monoid)
+open import Data.Fin.Base using (Fin)
+open import Data.Nat.Base using (ℕ)
+open import Data.Product.Base using (_,_; _×_)
+open import Data.System {suc 0ℓ} using (System; _≤_; Systemₛ)
+open import Data.System.Values Monoid using (module ≋)
+open import Data.Unit using (⊤; tt)
+open import Function.Base using (id; _∘_)
+open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
+open import Function.Construct.Identity using () renaming (function to Id)
+open import Function.Construct.Setoid using (_∙_)
+open import Functor.Instance.Nat.Pull using (Pull)
+open import Functor.Instance.Nat.Push using (Push)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
+
+open Func
+open Functor
+open _≤_
+
+private
+
+  variable A B C : ℕ
+
+  opaque
+
+    map : (Fin A → Fin B) → System A → System B
+    map f X = let open System X in record
+        { S = S
+        ; fₛ = fₛ ∙ Pull.₁ f
+        ; fₒ = Push.₁ f ∙ fₒ
+        }
+
+    ≤-cong : (f : Fin A → Fin B) {X Y : System A} → Y ≤ X → map f Y ≤ map f X
+    ⇒S (≤-cong f x≤y) = ⇒S x≤y
+    ≗-fₛ (≤-cong f x≤y) = ≗-fₛ x≤y ∘ to (Pull.₁ f)
+    ≗-fₒ (≤-cong f x≤y) = cong (Push.₁ f) ∘ ≗-fₒ x≤y
+
+    System₁ : (Fin A → Fin B) → Systemₛ A ⟶ₛ Systemₛ B
+    to (System₁ f) = map f
+    cong (System₁ f) (x≤y , y≤x) = ≤-cong f x≤y , ≤-cong f y≤x
+
+  opaque
+
+    unfolding System₁
+
+    id-x≤x : {X : System A} → System₁ id ⟨$⟩ X ≤ X
+    ⇒S (id-x≤x) = Id _
+    ≗-fₛ (id-x≤x {_} {x}) i s = cong (System.fₛ x) Pull.identity
+    ≗-fₒ (id-x≤x {A} {x}) s = Push.identity
+
+    x≤id-x : {x : System A} → x ≤ System₁ id ⟨$⟩ x
+    ⇒S x≤id-x = Id _
+    ≗-fₛ (x≤id-x {A} {x}) i s = cong (System.fₛ x) (≋.sym Pull.identity)
+    ≗-fₒ (x≤id-x {A} {x}) s = ≋.sym Push.identity
+
+    System-homomorphism
+        : {f : Fin A → Fin B}
+          {g : Fin B → Fin C} 
+          {X : System A}
+        → System₁ (g ∘ f) ⟨$⟩ X ≤ System₁ g ⟨$⟩ (System₁ f ⟨$⟩ X)
+        × System₁ g ⟨$⟩ (System₁ f ⟨$⟩ X) ≤ System₁ (g ∘ f) ⟨$⟩ X
+    System-homomorphism {f = f} {g} {X} = left , right
+      where
+        open System X
+        left : map (g ∘ f) X ≤ map g (map f X)
+        left .⇒S = Id S
+        left .≗-fₛ i s = cong fₛ Pull.homomorphism
+        left .≗-fₒ s = Push.homomorphism
+        right : map g (map f X) ≤ map (g ∘ f) X
+        right .⇒S = Id S
+        right .≗-fₛ i s = cong fₛ (≋.sym Pull.homomorphism)
+        right .≗-fₒ s = ≋.sym Push.homomorphism
+
+    System-resp-≈
+        : {f g : Fin A → Fin B}
+        → f ≗ g
+        → {X : System A}
+        → System₁ f ⟨$⟩ X ≤ System₁ g ⟨$⟩ X
+        × System₁ g ⟨$⟩ X ≤ System₁ f ⟨$⟩ X
+    System-resp-≈ {A} {B} {f = f} {g} f≗g {X} = both f≗g , both (≡.sym ∘ f≗g)
+      where
+        open System X
+        both : {f g : Fin A → Fin B} → f ≗ g → map f X ≤ map g X
+        both f≗g .⇒S = Id S
+        both f≗g .≗-fₛ i s = cong fₛ (Pull.F-resp-≈ f≗g {i})
+        both {f} {g} f≗g .≗-fₒ s = Push.F-resp-≈ f≗g
+
+opaque
+  unfolding System₁
+  Sys-defs : ⊤
+  Sys-defs = tt
+
+Sys : Functor Nat (Setoids (suc 0ℓ) (suc 0ℓ))
+Sys .F₀ = Systemₛ
+Sys .F₁ = System₁
+Sys .identity = id-x≤x , x≤id-x
+Sys .homomorphism {x = X} = System-homomorphism {X = X}
+Sys .F-resp-≈ = System-resp-≈
+
+module Sys = Functor Sys