From d2ce2675b5e0331b6bf5647a4fc195e458d9b5ee Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Thu, 30 Oct 2025 19:23:31 -0500
Subject: Add Circ functor

---
 Functor/Instance/Nat/Circ.agda | 32 ++++++++++++++++++++++++++++++++
 Functor/Instance/Nat/Edge.agda |  5 +----
 2 files changed, 33 insertions(+), 4 deletions(-)
 create mode 100644 Functor/Instance/Nat/Circ.agda

(limited to 'Functor')

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
-- 
cgit v1.2.3