Add shorter name for singleton setoid

15 files changed, 240 insertions, 267 deletions

diff --git a/Category/Instance/Setoids/SymmetricMonoidal.agda b/Category/Instance/Setoids/SymmetricMonoidal.agda
index f21124e..995ddf3 100644
--- a/Category/Instance/Setoids/SymmetricMonoidal.agda
+++ b/Category/Instance/Setoids/SymmetricMonoidal.agda
@@ -42,3 +42,6 @@ Setoids-+ = record
     ; monoidal = +-monoidal
     ; symmetric = +-symmetric
     }
+
+module Setoids-× = SymmetricMonoidalCategory Setoids-×
+module Setoids-+ = SymmetricMonoidalCategory Setoids-+
diff --git a/Data/CMonoid.agda b/Data/CMonoid.agda
index 6aec0c8..8aaf869 100644
--- a/Data/CMonoid.agda
+++ b/Data/CMonoid.agda
@@ -9,7 +9,6 @@ open import Object.Monoid.Commutative using (CommutativeMonoid; CommutativeMonoi
 open import Categories.Object.Monoid using (Monoid)
 
 open import Data.Monoid {c} {ℓ} using (toMonoid; fromMonoid; toMonoid⇒)
-module Setoids-× = SymmetricMonoidalCategory Setoids-×
 
 import Algebra.Bundles as Alg
 
@@ -39,7 +38,7 @@ toCMonoid M = record
       comm x y = commutative {x , y}
 
 open import Function.Construct.Constant using () renaming (function to Const)
-open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ)
+open import Data.Setoid.Unit using (⊤ₛ)
 
 fromCMonoid : Alg.CommutativeMonoid c ℓ → CommutativeMonoid Setoids-×.symmetric
 fromCMonoid M = record
diff --git a/Data/Monoid.agda b/Data/Monoid.agda
index dba3e79..1ba0af4 100644
--- a/Data/Monoid.agda
+++ b/Data/Monoid.agda
@@ -7,8 +7,6 @@ open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory
 open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-monoidal′)
 open import Categories.Object.Monoid using (Monoid; Monoid⇒)
 
-module Setoids-× = SymmetricMonoidalCategory Setoids-×
-
 import Algebra.Bundles as Alg
 
 open import Data.Setoid using (∣_∣)
@@ -20,7 +18,7 @@ open Func
 -- A monoid object in the (monoidal) category of setoids is just a monoid
 
 open import Function.Construct.Constant using () renaming (function to Const)
-open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ)
+open import Data.Setoid.Unit using (⊤ₛ)
 
 opaque
   unfolding ×-monoidal′
diff --git a/Data/Setoid/Unit.agda b/Data/Setoid/Unit.agda
new file mode 100644
index 0000000..8b8edde
--- /dev/null
+++ b/Data/Setoid/Unit.agda
@@ -0,0 +1,11 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+module Data.Setoid.Unit {c ℓ : Level} where
+
+open import Categories.Category.Instance.SingletonSet using (SingletonSetoid)
+open import Relation.Binary using (Setoid)
+
+⊤ₛ : Setoid c ℓ
+⊤ₛ = SingletonSetoid {c} {ℓ}
diff --git a/Data/System.agda b/Data/System.agda
index 5d5e484..d71c2a8 100644
--- a/Data/System.agda
+++ b/Data/System.agda
@@ -8,10 +8,10 @@ import Relation.Binary.Properties.Preorder as PreorderProperties
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 open import Categories.Category using (Category)
-open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ)
 open import Data.Circuit.Value using (Monoid)
 open import Data.Nat using (ℕ)
 open import Data.Setoid using (_⇒ₛ_; ∣_∣)
+open import Data.Setoid.Unit using (⊤ₛ)
 open import Data.System.Values Monoid using (Values; _≋_; module ≋; <ε>)
 open import Function using (Func; _⟨$⟩_; flip)
 open import Function.Construct.Constant using () renaming (function to Const)
diff --git a/DecorationFunctor/Graph.agda b/DecorationFunctor/Graph.agda
index d8a0187..8b62430 100644
--- a/DecorationFunctor/Graph.agda
+++ b/DecorationFunctor/Graph.agda
@@ -4,62 +4,48 @@ module DecorationFunctor.Graph where
 
 import Categories.Morphism as Morphism
 
+open import Level using (0ℓ)
+
 open import Categories.Category.BinaryProducts using (module BinaryProducts)
 open import Categories.Category.Cartesian using (Cartesian)
-open import Categories.Category.Cocartesian using (Cocartesian; module BinaryCoproducts)
-open import Categories.Category.Core using (Category)
-open import Categories.Category.Instance.Nat using (Nat-Cocartesian)
 open import Categories.Category.Instance.Nat using (Nat)
 open import Categories.Category.Instance.Setoids using (Setoids)
-open import Categories.Category.Instance.SingletonSet using (SingletonSetoid)
 open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
 open import Categories.Category.Product using (_⁂_)
 open import Categories.Functor using () renaming (_∘F_ to _∘′_)
 open import Categories.Functor.Core using (Functor)
 open import Categories.Functor.Monoidal.Symmetric using (module Lax)
 open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
-
 open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
-open import Category.Instance.Setoids.SymmetricMonoidal using (Setoids-×)
 open import Category.Instance.Nat.FinitelyCocomplete using (Nat-FinitelyCocomplete)
-
+open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×; ×-symmetric′)
 open import Data.Empty using (⊥-elim)
-open import Data.Fin using (#_)
-open import Data.Fin.Base using (Fin; splitAt; join; zero; suc; _↑ˡ_; _↑ʳ_)
+open import Data.Fin using (#_; Fin; splitAt; join; zero; suc; _↑ˡ_; _↑ʳ_)
 open import Data.Fin.Patterns using (0F; 1F)
 open import Data.Fin.Properties using (splitAt-join; join-splitAt; splitAt-↑ˡ; splitAt⁻¹-↑ˡ)
 open import Data.Nat using (ℕ; _+_)
 open import Data.Product.Base using (_,_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (×-setoid)
+open import Data.Setoid.Unit {0ℓ} {0ℓ} using (⊤ₛ)
 open import Data.Sum.Base using (_⊎_; map; inj₁; inj₂; swap) renaming ([_,_]′ to [_,_])
 open import Data.Sum.Properties using (map-map; [,]-map; [,]-∘; [-,]-cong; [,-]-cong; map-cong; swap-involutive)
 open import Data.Unit using (tt)
-open import Data.Unit.Properties using () renaming (≡-setoid to ⊤-setoid)
-
-open import Function.Base using (_∘_; id; const; case_of_)
-open import Function.Bundles using (Func; Inverse; _↔_; mk↔)
+open import Function using (_∘_; id; const; Func; Inverse; _↔_; mk↔)
 open import Function.Construct.Composition using (_↔-∘_)
+open import Function.Construct.Constant using () renaming (function to Const)
 open import Function.Construct.Identity using (↔-id)
 open import Function.Construct.Symmetry using (↔-sym)
-
-open import Level using (0ℓ; lift)
-
-open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.PropositionalEquality using (_≗_)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; erefl; refl; sym; trans; cong)
+open import Relation.Binary using (Setoid)
+open import Relation.Binary.PropositionalEquality using (_≗_; _≡_; erefl; refl; sym; trans; cong)
 open import Relation.Binary.PropositionalEquality.Properties using (isEquivalence; module ≡-Reasoning)
 open import Relation.Nullary.Negation.Core using (¬_)
 
 open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products)
-open Cocartesian Nat-Cocartesian using (coproducts)
 open FinitelyCocompleteCategory Nat-FinitelyCocomplete
-    using ()
-    renaming (symmetricMonoidalCategory to Nat-smc)
-open Morphism (Setoids 0ℓ 0ℓ) using (_≅_)
+    using (-+-)
+    renaming (symmetricMonoidalCategory to Nat-smc; +-assoc to Nat-+-assoc)
 open Lax using (SymmetricMonoidalFunctor)
-
 open BinaryProducts products using (-×-)
-open BinaryCoproducts coproducts using (-+-) renaming (+-assoc to Nat-+-assoc)
 
 record Graph (v : ℕ) : Set where
 
@@ -182,18 +168,15 @@ F = record
     ; F-resp-≈ = λ f≗g → F-resp-≈ f≗g
     }
 
-empty-graph : Graph 0
-empty-graph = record
+discrete : {n : ℕ} → Graph n
+discrete = record
     { e = 0
     ; s = λ ()
     ; t = λ ()
     }
 
-ε : Func (SingletonSetoid {0ℓ} {0ℓ}) (Graph-setoid 0)
-ε = record
-    { to = const empty-graph
-    ; cong = const Graph-same-refl
-    }
+ε : Func ⊤ₛ (Graph-setoid 0)
+ε = Const ⊤ₛ (Graph-setoid 0) discrete
 
 together : Graph n → Graph m → Graph (n + m)
 together {n} {m} G₁ G₂ = record
@@ -521,7 +504,7 @@ associativity {X} {Y} {Z} G₁ G₂ G₃ = record
         (G₁+[G₂+G₃].t ∘ [ [ _↑ˡ G₂.e + G₃.e , (G₁.e ↑ʳ_) ∘ (_↑ˡ G₃.e) ] ∘ splitAt G₁.e , (G₁.e ↑ʳ_) ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨⟩
         (G₁+[G₂+G₃].t ∘ to (+-assoc-↔ G₁.e G₂.e G₃.e)) x  ∎
 
-unitaryˡ : Graph-same (together empty-graph G) G
+unitaryˡ : Graph-same (together (discrete {0}) G) G
 unitaryˡ = Graph-same-refl
 
 n+0↔n : ∀ n → Fin (n + 0) ↔ Fin n
@@ -544,7 +527,7 @@ n+0↔n n = record
 
 unitaryʳ
     : {G : Graph n}
-    → Graph-same (map-nodes ([ (λ x → x) , (λ ()) ] ∘ splitAt n) (together G empty-graph)) G
+    → Graph-same (map-nodes ([ (λ x → x) , (λ ()) ] ∘ splitAt n) (together G discrete)) G
 unitaryʳ {n} {G} = record
     { ↔e = e+0↔e
     ; ≗s = ≗s+0
@@ -637,28 +620,27 @@ braiding {n} {m} {G₁} {G₂} = record
             ≡⟨ (cong (join m n ∘ map G₂.t G₁.t) ∘ splitAt-join G₂.e G₁.e ∘ swap ∘ splitAt G₁.e) x ⟨
         (join m n ∘ map G₂.t G₁.t ∘ splitAt G₂.e ∘ join G₂.e G₁.e ∘ swap ∘ splitAt G₁.e) x ∎
 
-graph : SymmetricMonoidalFunctor Nat-smc (Setoids-× {0ℓ})
-graph = record
-    { F = F
-    ; isBraidedMonoidal = record
-        { isMonoidal = record
-            { ε = ε
-            ; ⊗-homo = ⊗-homomorphism
-            ; associativity = λ { {x} {y} {z} {(G₁ , G₂) , G₃} → associativity G₁ G₂ G₃ }
-            ; unitaryˡ = unitaryˡ
-            ; unitaryʳ = unitaryʳ
-            }
-        ; braiding-compat = λ { {x} {y} {G₁ , G₂} → braiding {G₁ = G₁} {G₂ = G₂} }
-        }
-    }
+opaque
+  unfolding ×-symmetric′
+  graph : SymmetricMonoidalFunctor Nat-smc Setoids-×
+  graph = record
+      { F = F
+      ; isBraidedMonoidal = record
+          { isMonoidal = record
+              { ε = ε
+              ; ⊗-homo = ⊗-homomorphism
+              ; associativity = λ { {x} {y} {z} {(G₁ , G₂) , G₃} → associativity G₁ G₂ G₃ }
+              ; unitaryˡ = unitaryˡ
+              ; unitaryʳ = unitaryʳ
+              }
+          ; braiding-compat = λ { {x} {y} {G₁ , G₂} → braiding {G₁ = G₁} {G₂ = G₂} }
+          }
+      }
 
 module F = SymmetricMonoidalFunctor graph
 
-and-gate : Func (SingletonSetoid {0ℓ} {0ℓ}) (F.₀ 3)
-and-gate = record
-    { to = λ { (lift tt) → and-graph }
-    ; cong = λ { (lift tt) → Graph-same-refl }
-    }
+and-gate : Func ⊤ₛ (Graph-setoid 3)
+and-gate = Const ⊤ₛ (Graph-setoid 3) and-graph
   where
     and-graph : Graph 3
     and-graph = record
diff --git a/DecorationFunctor/Hypergraph.agda b/DecorationFunctor/Hypergraph.agda
index 5cd83f3..2f61bc3 100644
--- a/DecorationFunctor/Hypergraph.agda
+++ b/DecorationFunctor/Hypergraph.agda
@@ -3,65 +3,51 @@
 module DecorationFunctor.Hypergraph where
 
 import Categories.Morphism as Morphism
+open import Level using (0ℓ)
 
 open import Categories.Category.BinaryProducts using (module BinaryProducts)
 open import Categories.Category.Cartesian using (Cartesian)
-open import Categories.Category.Cocartesian using (Cocartesian; module BinaryCoproducts)
 open import Categories.Category.Core using (Category)
-open import Categories.Category.Instance.Nat using (Nat-Cocartesian)
 open import Categories.Category.Instance.Nat using (Nat)
 open import Categories.Category.Instance.Setoids using (Setoids)
-open import Categories.Category.Instance.SingletonSet using (SingletonSetoid)
 open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
 open import Categories.Category.Product using (_⁂_)
 open import Categories.Functor using () renaming (_∘F_ to _∘′_)
 open import Categories.Functor.Core using (Functor)
 open import Categories.Functor.Monoidal.Symmetric using (module Lax)
 open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
-
 open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
-open import Category.Instance.Setoids.SymmetricMonoidal using (Setoids-×)
 open import Category.Instance.Nat.FinitelyCocomplete using (Nat-FinitelyCocomplete)
-
+open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×; ×-symmetric′)
 open import Data.Empty using (⊥-elim)
-open import Data.Fin using (#_)
-open import Data.Fin.Base using (Fin; splitAt; join; zero; suc; _↑ˡ_; _↑ʳ_; Fin′; toℕ; cast)
+open import Data.Fin using (#_; Fin; splitAt; join; zero; suc; _↑ˡ_; _↑ʳ_; toℕ; cast)
 open import Data.Fin.Patterns using (0F; 1F; 2F)
-open import Data.Fin.Permutation using (lift₀)
 open import Data.Fin.Properties using (splitAt-join; join-splitAt; cast-is-id; cast-trans; toℕ-cast; subst-is-cast; splitAt-↑ˡ; splitAt-↑ʳ; splitAt⁻¹-↑ˡ; ↑ˡ-injective)
 open import Data.Nat using (ℕ; _+_)
 open import Data.Product.Base using (_,_; Σ)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent using (×-setoid)
-open import Data.Sum.Base using (_⊎_; map; inj₁; inj₂; swap; map₂) renaming ([_,_]′ to [_,_])
+open import Data.Setoid using (∣_∣)
+open import Data.Setoid.Unit {0ℓ} {0ℓ} using (⊤ₛ)
+open import Data.Sum using (_⊎_; map; inj₁; inj₂; swap; map₂) renaming ([_,_]′ to [_,_])
 open import Data.Sum.Properties using (map-map; [,]-map; [,]-∘; [-,]-cong; [,-]-cong; [,]-cong; map-cong; swap-involutive)
 open import Data.Unit using (tt)
-open import Data.Unit.Properties using () renaming (≡-setoid to ⊤-setoid)
-
-open import Function.Base using (_∘_; id; const; case_of_; case_returning_of_)
-open import Function.Bundles using (Func; Inverse; _↔_; mk↔)
+open import Function using (_∘_; id; const; Func; Inverse; _↔_; mk↔; _⟨$⟩_)
 open import Function.Construct.Composition using (_↔-∘_)
-open import Function.Construct.Identity using (↔-id)
+open import Function.Construct.Constant using () renaming (function to Const)
+open import Function.Construct.Identity using (↔-id) renaming (function to Id)
 open import Function.Construct.Symmetry using (↔-sym)
-
-open import Level using (0ℓ; lift)
-
-open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.PropositionalEquality using (_≗_)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; erefl; refl; sym; trans; cong; cong₂; subst; cong-app)
+open import Relation.Binary using (Setoid)
+open import Relation.Binary.PropositionalEquality.Core using (_≗_; _≡_; erefl; refl; sym; trans; cong; cong₂; subst; cong-app)
 open import Relation.Binary.PropositionalEquality.Properties using (isEquivalence; module ≡-Reasoning; dcong₂; subst-∘)
 open import Relation.Nullary.Negation.Core using (¬_)
 
 open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products)
-open Cocartesian Nat-Cocartesian using (coproducts)
 open FinitelyCocompleteCategory Nat-FinitelyCocomplete
-    using ()
-    renaming (symmetricMonoidalCategory to Nat-smc)
+    using (-+-; _+₁_)
+    renaming (symmetricMonoidalCategory to Nat-smc; +-assoc to Nat-+-assoc)
 open Morphism (Setoids 0ℓ 0ℓ) using (_≅_)
 open Lax using (SymmetricMonoidalFunctor)
 
 open BinaryProducts products using (-×-)
-open BinaryCoproducts coproducts using (-+-) renaming (+-assoc to Nat-+-assoc)
-
 
 record Hypergraph (v : ℕ) : Set where
 
@@ -80,7 +66,6 @@ record Hypergraph-same {n : ℕ} (H H′ : Hypergraph n) : Set where
   open Hypergraph H public
   open Hypergraph H′ renaming (h to h′; a to a′; arity to arity′; j to j′) public
 
-
   field
     ↔h : Fin h ↔ Fin h′
 
@@ -165,8 +150,8 @@ Hypergraph-same-trans ≡H₁ ≡H₂ = record
             ≡⟨ cong (j′ ≡H₂ (to (↔h ≡H₂) (to (↔h ≡H₁) e))) (cast-trans (≗arity ≡H₁ e) (≗arity ≡H₂ (to (↔h ≡H₁) e)) i) ⟩
         j′ ≡H₂ (to (↔h ≡H₂) (to (↔h ≡H₁) e)) (cast (trans (≗arity ≡H₁ e) (≗arity ≡H₂ (to (↔h ≡H₁) e))) i) ∎
 
-Hypergraph-setoid : ℕ → Setoid 0ℓ 0ℓ
-Hypergraph-setoid p = record
+Hypergraphₛ : ℕ → Setoid 0ℓ 0ℓ
+Hypergraphₛ p = record
     { Carrier = Hypergraph p
     ; _≈_ = Hypergraph-same
     ; isEquivalence = record
@@ -192,12 +177,12 @@ Hypergraph-same-cong
 Hypergraph-same-cong f ≡H = record
     { ↔h = ↔h
     ; ≗a = ≗a
-    ; ≗j = λ { e i → cong f (≗j e i) }
+    ; ≗j = λ e i → cong f (≗j e i)
     }
   where
     open Hypergraph-same ≡H
 
-Hypergraph-Func : (Fin n → Fin m) → Func (Hypergraph-setoid n) (Hypergraph-setoid m)
+Hypergraph-Func : (Fin n → Fin m) → Func (Hypergraphₛ n) (Hypergraphₛ m)
 Hypergraph-Func f = record
     { to = map-nodes f
     ; cong = Hypergraph-same-cong f
@@ -229,7 +214,7 @@ homomorphism {n} {m} {o} {H} f g = record
 
 F : Functor Nat (Setoids 0ℓ 0ℓ)
 F = record
-    { F₀ = Hypergraph-setoid
+    { F₀ = Hypergraphₛ
     ; F₁ = Hypergraph-Func
     ; identity = λ { {n} {H} → Hypergraph-same-refl {H = H} }
     ; homomorphism = λ { {f = f} {g = g} → homomorphism f g }
@@ -238,18 +223,18 @@ F = record
 
 -- monoidal structure
 
-empty-hypergraph : Hypergraph 0
-empty-hypergraph = record
+discrete : {n : ℕ} → Hypergraph n
+discrete {n} = record
     { h = 0
     ; a = λ ()
     ; j = λ ()
     }
 
-ε : Func (SingletonSetoid {0ℓ} {0ℓ}) (Hypergraph-setoid 0)
-ε = record
-    { to = const empty-hypergraph
-    ; cong = const Hypergraph-same-refl
-    }
+opaque
+  unfolding ×-symmetric′
+
+  ε : Func Setoids-×.unit (Hypergraphₛ 0)
+  ε = Const ⊤ₛ (Hypergraphₛ 0) discrete
 
 module _ (H₁ : Hypergraph n) (H₂ : Hypergraph m) where
   private
@@ -364,7 +349,7 @@ commute
     → (g : Fin m → Fin m′)
     → Hypergraph-same
         (together (map-nodes f H₁) (map-nodes g H₂))
-        (map-nodes  ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n) (together H₁ H₂))
+        (map-nodes (f +₁ g) (together H₁ H₂))
 commute {n} {n′} {m} {m′} {H₁} {H₂} f g = record
     { ↔h = ≡H₁+H₂.↔h
     ; ≗a = ≡H₁+H₂.≗a
@@ -380,23 +365,36 @@ commute {n} {n′} {m} {m′} {H₁} {H₂} f g = record
     ≗j  : (e : Fin (H₁.h + H₂.h))
           (i : Fin ((ℕ.suc ∘ [ H₁.a , H₂.a ] ∘ splitAt H₁.h) e))
         → j (together (map-nodes f H₁) (map-nodes g H₂)) e i
-        ≡ j (map-nodes ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n) (together H₁ H₂)) (≡H₁+H₂.to e) (cast refl i)
+        ≡ j (map-nodes (f +₁ g) (together H₁ H₂)) (≡H₁+H₂.to e) (cast refl i)
     ≗j e i with splitAt H₁.h e
     ... | inj₁ e₁ rewrite splitAt-↑ˡ n (H₁.j e₁ (cast refl i)) m = cong ((_↑ˡ m′) ∘ f ∘ H₁.j e₁) (sym (cast-is-id refl i))
     ... | inj₂ e₂ rewrite splitAt-↑ʳ n m (H₂.j e₂ (cast refl i)) = cong ((n′ ↑ʳ_) ∘ g ∘ H₂.j e₂) (sym (cast-is-id refl i))
 
-⊗-homomorphism : NaturalTransformation (-×- ∘′ (F ⁂ F)) (F ∘′ -+-)
-⊗-homomorphism = record
-    { η = λ { (m , n) → η }
-    ; commute = λ { (f , g) {H₁ , H₂} → commute {H₁ = H₁} {H₂ = H₂} f g }
-    ; sym-commute = λ { (f , g) {H₁ , H₂} → Hypergraph-same-sym (commute {H₁ = H₁} {H₂ = H₂} f g) }
+open Setoids-× using (_⊗₀_; _⊗₁_)
+opaque
+  unfolding ×-symmetric′
+  η : Func (Hypergraphₛ n ⊗₀ Hypergraphₛ m) (Hypergraphₛ (n + m))
+  η = record
+      { to = λ (H₁ , H₂) → together H₁ H₂
+      ; cong = λ (≡H₁ , ≡H₂) → together-resp-same ≡H₁ ≡H₂
+      }
+
+opaque
+  unfolding η
+  commute′
+      : (f : Fin n → Fin n′)
+      → (g : Fin m → Fin m′)
+      → {x : ∣ Hypergraphₛ n ⊗₀ Hypergraphₛ m ∣}
+      → Hypergraph-same
+          (η ⟨$⟩ (Hypergraph-Func f ⊗₁ Hypergraph-Func g ⟨$⟩ x))
+          (map-nodes (f +₁ g) (η ⟨$⟩ x))
+  commute′ f g {H₁ , H₂} = commute {H₁ = H₁} {H₂} f g
+
+⊗-homomorphism : NaturalTransformation (Setoids-×.⊗ ∘′ (F ⁂ F)) (F ∘′ -+-)
+⊗-homomorphism = ntHelper record
+    { η = λ (n , m) → η {n} {m}
+    ; commute = λ (f , g) → commute′ f g
     }
-  where
-    η : Func (×-setoid (Hypergraph-setoid n) (Hypergraph-setoid m)) (Hypergraph-setoid (n + m))
-    η = record
-        { to = λ { (H₁ , H₂) → together H₁ H₂ }
-        ; cong = λ { (≡H₁ , ≡H₂) → together-resp-same ≡H₁ ≡H₂ }
-        }
 
 +-assoc-↔ : ∀ (x y z : ℕ) → Fin (x + y + z) ↔ Fin (x + (y + z))
 +-assoc-↔ x y z = record
@@ -412,13 +410,13 @@ commute {n} {n′} {m} {m′} {H₁} {H₂} f g = record
 
 associativity
     : {X Y Z : ℕ}
-    → {H₁ : Hypergraph X}
-    → {H₂ : Hypergraph Y}
-    → {H₃ : Hypergraph Z}
+    → (H₁ : Hypergraph X)
+    → (H₂ : Hypergraph Y)
+    → (H₃ : Hypergraph Z)
     → Hypergraph-same
         (map-nodes (Inverse.to (+-assoc-↔ X Y Z)) (together (together H₁ H₂) H₃))
         (together H₁ (together H₂ H₃))
-associativity {X} {Y} {Z} {H₁} {H₂} {H₃} = record
+associativity {X} {Y} {Z} H₁ H₂ H₃ = record
     { ↔h = ↔h
     ; ≗a = ≗a
     ; ≗j = ≗j
@@ -472,7 +470,6 @@ associativity {X} {Y} {Z} {H₁} {H₂} {H₃} = record
         rewrite splitAt-↑ˡ (X + Y) (H₁.j e₁ i ↑ˡ Y) Z
         rewrite splitAt-↑ˡ X (H₁.j e₁ i) Y = cong ((_↑ˡ Y + Z) ∘ H₁.j e₁) (sym (cast-is-id refl i))
     ≗j e i | inj₁ e₁₂ | inj₂ e₂
-        rewrite splitAt-↑ʳ H₁.h H₂.h e₂
         rewrite splitAt-↑ʳ H₁.h (H₂.h + H₃.h) (e₂ ↑ˡ H₃.h)
         rewrite splitAt-↑ˡ H₂.h e₂ H₃.h
         rewrite splitAt-↑ˡ (X + Y) (X ↑ʳ H₂.j e₂ i) Z
@@ -500,7 +497,7 @@ n+0↔n n = record
     to∘from : (x : Fin n) → to (from x) ≡ x
     to∘from x rewrite splitAt-↑ˡ n x 0 = refl
 
-unitaryʳ : Hypergraph-same (map-nodes ([ (λ x → x) , (λ ()) ] ∘ splitAt n) (together H empty-hypergraph)) H
+unitaryʳ : Hypergraph-same (map-nodes ([ id , (λ ()) ] ∘ splitAt n) (together H discrete)) H
 unitaryʳ {n} {H} = record
     { ↔h = h+0↔h
     ; ≗a = ≗a
@@ -508,22 +505,22 @@ unitaryʳ {n} {H} = record
     }
   where
     module H = Hypergraph H
-    module H+0 = Hypergraph (together H empty-hypergraph)
+    module H+0 = Hypergraph (together {n} {0} H discrete)
     h+0↔h : Fin H+0.h ↔ Fin H.h
     h+0↔h = n+0↔n H.h
     ≗a : (e : Fin (H.h + 0)) → [ H.a , (λ ()) ] (splitAt H.h e) ≡ H.a (Inverse.to h+0↔h e)
     ≗a e with inj₁ e₁ ← splitAt H.h e in eq = refl
     ≗j  : (e : Fin (H.h + 0))
           (i : Fin (ℕ.suc ([ H.a , (λ ()) ] (splitAt H.h e))))
-        → [ (λ x → x) , (λ ()) ] (splitAt n (j+j H empty-hypergraph e i))
+        → [ (λ x → x) , (λ ()) ] (splitAt n (j+j H discrete e i))
         ≡ H.j (Inverse.to h+0↔h e) (cast (cong ℕ.suc (≗a e)) i)
-    ≗j e i = ≗j-aux (splitAt H.h e) refl (j+j H empty-hypergraph e) refl (≗a e) i
+    ≗j e i = ≗j-aux (splitAt H.h e) refl (j+j H discrete e) refl (≗a e) i
       where
         ≗j-aux
             : (w : Fin H.h ⊎ Fin 0)
             → (eq₁ : splitAt H.h e ≡ w)
             → (w₁ : Fin (ℕ.suc ([ H.a , (λ ()) ] w)) → Fin (n + 0))
-            → j+j H empty-hypergraph e ≡ subst (λ hole → Fin (ℕ.suc ([ H.a , (λ ()) ] hole)) → Fin (n + 0)) (sym eq₁) w₁
+            → j+j H discrete e ≡ subst (λ hole → Fin (ℕ.suc ([ H.a , (λ ()) ] hole)) → Fin (n + 0)) (sym eq₁) w₁
             → (w₂ : [ H.a , (λ ()) ] w ≡ H.a (Inverse.to h+0↔h e))
               (i : Fin (ℕ.suc ([ H.a , (λ ()) ] w)))
             → [ (λ x → x) , (λ ()) ] (splitAt n (w₁ i))
@@ -594,43 +591,60 @@ braiding {n} {m} {H₁} {H₂} = record
         rewrite splitAt-↑ʳ n m (H₂.j e₂ i)
         rewrite splitAt-↑ˡ H₂.h e₂ H₁.h = cong ((_↑ˡ n) ∘ H₂.j e₂) (sym (cast-is-id refl i))
 
-hypergraph : SymmetricMonoidalFunctor Nat-smc (Setoids-× {0ℓ})
+opaque
+  unfolding η ε
+
+  associativity′
+      : {n m o : ℕ}
+      → {x : ∣ (Hypergraphₛ n ⊗₀ Hypergraphₛ m) ⊗₀ Hypergraphₛ o ∣}
+      → Hypergraph-same
+          (map-nodes (Inverse.to (+-assoc-↔ n m o)) (η {n + m} {o} ⟨$⟩ ((η {n} {m} ⊗₁ (Id _)) ⟨$⟩ x)))
+          (η {n} {m + o} ⟨$⟩ ((Id _ ⊗₁ η {m} {o}) ⟨$⟩ (Setoids-×.associator.from ⟨$⟩ x)))
+  associativity′ {n} {m} {o} {(x , y) , z} = associativity x y z
+
+  unitaryˡ′
+      : {X : ∣ Setoids-×.unit ⊗₀ Hypergraphₛ n ∣}
+      → Hypergraph-same (η {0} {n} ⟨$⟩ ((ε ⊗₁ Id _) ⟨$⟩ X)) (Setoids-×.unitorˡ.from ⟨$⟩ X)
+  unitaryˡ′ = Hypergraph-same-refl
+
+  unitaryʳ′
+      : {X : ∣ Hypergraphₛ n ⊗₀ Setoids-×.unit ∣}
+      → Hypergraph-same (map-nodes ([ id , (λ ()) ] ∘ splitAt n) (η {n} {0} ⟨$⟩ ((Id _ ⊗₁ ε) ⟨$⟩ X))) (Setoids-×.unitorʳ.from ⟨$⟩ X)
+  unitaryʳ′ = unitaryʳ
+
+  braiding-compat
+      : {n m : ℕ}
+      → {X : ∣ Hypergraphₛ n ⊗₀ Hypergraphₛ m ∣}
+      → Hypergraph-same
+          (map-nodes ([ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n) (η {n} {m} ⟨$⟩ X))
+          (η {m} {n} ⟨$⟩ (Setoids-×.braiding.⇒.η (Hypergraphₛ n , Hypergraphₛ m) ⟨$⟩ X))
+  braiding-compat {n} {m} {H₁ , H₂} = braiding {n} {m} {H₁} {H₂}
+
+hypergraph : SymmetricMonoidalFunctor Nat-smc Setoids-×
 hypergraph = record
     { F = F
     ; isBraidedMonoidal = record
         { isMonoidal = record
             { ε = ε
-            ; ⊗-homo = ntHelper record
-                { η = λ { (m , n) → η }
-                ; commute = λ { (f , g) {H₁ , H₂} → commute {H₁ = H₁} {H₂ = H₂} f g }
-                }
-            ; associativity = λ { {X} {Y} {Z} {(H₁ , H₂) , H₃} → associativity {X} {Y} {Z} {H₁} {H₂} {H₃} }
-            ; unitaryˡ = Hypergraph-same-refl
-            ; unitaryʳ = unitaryʳ
+            ; ⊗-homo = ⊗-homomorphism
+            ; associativity = associativity′
+            ; unitaryˡ = unitaryˡ′
+            ; unitaryʳ = unitaryʳ′
             }
-        ; braiding-compat = λ { {X} {Y} {H₁ , H₂} → braiding {X} {Y} {H₁} {H₂} }
+        ; braiding-compat = braiding-compat
         }
     }
-  where
-    η : Func (×-setoid (Hypergraph-setoid n) (Hypergraph-setoid m)) (Hypergraph-setoid (n + m))
-    η = record
-        { to = λ { (H₁ , H₂) → together H₁ H₂ }
-        ; cong = λ { (≡H₁ , ≡H₂) → together-resp-same ≡H₁ ≡H₂ }
-        }
 
 module F = SymmetricMonoidalFunctor hypergraph
 
-and-gate : Func (SingletonSetoid {0ℓ} {0ℓ}) (F.₀ 3)
-and-gate = record
-    { to = λ { (lift tt) → and-graph }
-    ; cong = λ { (lift tt) → Hypergraph-same-refl }
-    }
+and-gate : Func ⊤ₛ (F.₀ 3)
+and-gate = Const ⊤ₛ (Hypergraphₛ 3) and-graph
   where
     and-graph : Hypergraph 3
     and-graph = record
         { h = 1
         ; a = λ { 0F → 2 }
-        ; j = λ { 0F → edge-0-nodes }
+        ; j = λ { 0F → id }
         }
       where
         edge-0-nodes : Fin 3 → Fin 3
diff --git a/DecorationFunctor/Hypergraph/Labeled.agda b/DecorationFunctor/Hypergraph/Labeled.agda
index 33a7a89..31402b1 100644
--- a/DecorationFunctor/Hypergraph/Labeled.agda
+++ b/DecorationFunctor/Hypergraph/Labeled.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level using (Level; 0ℓ; lift)
+open import Level using (Level)
 
 module DecorationFunctor.Hypergraph.Labeled {c ℓ : Level} where
 
@@ -8,28 +8,20 @@ import Categories.Morphism as Morphism
 
 open import Categories.Category.BinaryProducts using (module BinaryProducts)
 open import Categories.Category.Cartesian using (Cartesian)
-open import Categories.Category.Cocartesian using (Cocartesian; module BinaryCoproducts)
 open import Categories.Category.Core using (Category)
-open import Categories.Category.Instance.Nat using (Nat-Cocartesian)
 open import Categories.Category.Instance.Nat using (Nat)
 open import Categories.Category.Instance.Setoids using (Setoids)
-open import Categories.Category.Instance.SingletonSet using (SingletonSetoid)
 open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
 open import Categories.Category.Product using (_⁂_)
 open import Categories.Functor using () renaming (_∘F_ to _∘′_)
 open import Categories.Functor.Core using (Functor)
 open import Categories.Functor.Monoidal.Symmetric using (module Lax)
 open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
-
 open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
-open import Category.Instance.Setoids.SymmetricMonoidal using (Setoids-×)
 open import Category.Instance.Nat.FinitelyCocomplete using (Nat-FinitelyCocomplete)
-
-open import Data.Empty using (⊥-elim)
-open import Data.Fin using (#_)
-open import Data.Fin.Base using (Fin; splitAt; join; zero; suc; _↑ˡ_; _↑ʳ_; Fin′; cast)
+open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-symmetric′)
+open import Data.Fin using (#_; Fin; splitAt; join; zero; suc; _↑ˡ_; _↑ʳ_; cast)
 open import Data.Fin.Patterns using (0F; 1F; 2F)
-open import Data.Fin.Permutation using (lift₀)
 open import Data.Fin.Properties
   using
     ( splitAt-join ; join-splitAt
@@ -40,33 +32,29 @@ open import Data.Fin.Properties
 open import Data.Nat using (ℕ; _+_)
 open import Data.Product.Base using (_,_; Σ)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Data.Setoid.Unit {c} {ℓ} using (⊤ₛ)
 open import Data.Sum.Base using (_⊎_; map; inj₁; inj₂; swap; map₂) renaming ([_,_]′ to [_,_])
 open import Data.Sum.Properties using (map-map; [,]-map; [,]-∘; [-,]-cong; [,-]-cong; [,]-cong; map-cong; swap-involutive)
 open import Data.Unit.Properties using () renaming (≡-setoid to ⊤-setoid)
-
-open import Function.Base using (_∘_; id; const; case_of_; case_returning_of_)
-open import Function.Bundles using (Func; Inverse; _↔_; mk↔; _⟶ₛ_)
+open import Function using (_∘_; id; const; Func; Inverse; _↔_; mk↔; _⟶ₛ_)
 open import Function.Construct.Composition using (_↔-∘_)
+open import Function.Construct.Constant using () renaming (function to Const)
 open import Function.Construct.Identity using (↔-id)
 open import Function.Construct.Symmetry using (↔-sym)
-
-open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.PropositionalEquality using (_≗_)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; erefl; refl; sym; trans; cong; cong₂; subst; cong-app)
+open import Relation.Binary using (Setoid)
+open import Relation.Binary.PropositionalEquality using (_≗_; _≡_; erefl; refl; sym; trans; cong; cong₂; subst; cong-app)
 open import Relation.Binary.PropositionalEquality.Properties using (isEquivalence; module ≡-Reasoning; dcong; dcong₂; subst-∘; subst-subst; sym-cong; subst-subst-sym; trans-cong; cong-∘; trans-reflʳ)
 open import Relation.Nullary.Negation.Core using (¬_)
 
 open Cartesian (Setoids-Cartesian {c} {ℓ}) using (products)
-open Cocartesian Nat-Cocartesian using (coproducts)
 open FinitelyCocompleteCategory Nat-FinitelyCocomplete
-    using ()
-    renaming (symmetricMonoidalCategory to Nat-smc)
+    using (-+-)
+    renaming (symmetricMonoidalCategory to Nat-smc; +-assoc to Nat-+-assoc)
 open import Category.Monoidal.Instance.Nat using (Nat,+,0)
 open Morphism (Setoids c ℓ) using (_≅_)
 open Lax using (SymmetricMonoidalFunctor)
 
 open BinaryProducts products using (-×-)
-open BinaryCoproducts coproducts using (-+-) renaming (+-assoc to Nat-+-assoc)
 
 open import Data.Circuit.Gate using (Gate; cast-gate; cast-gate-trans; cast-gate-is-id; subst-is-cast-gate)
 
@@ -260,19 +248,16 @@ F = record
 
 -- monoidal structure
 
-empty-hypergraph : Hypergraph 0
-empty-hypergraph = record
+discrete : {n : ℕ} → Hypergraph n
+discrete = record
     { h = 0
     ; a = λ ()
     ; j = λ ()
     ; l = λ ()
     }
 
-ε : SingletonSetoid {c} {ℓ} ⟶ₛ Hypergraph-setoid 0
-ε = record
-    { to = const empty-hypergraph
-    ; cong = const Hypergraph-same-refl
-    }
+ε : ⊤ₛ ⟶ₛ Hypergraph-setoid 0
+ε = Const ⊤ₛ (Hypergraph-setoid 0) discrete
 
 module _ (H₁ : Hypergraph n) (H₂ : Hypergraph m) where
   private
@@ -510,7 +495,6 @@ associativity {X} {Y} {Z} {H₁} {H₂} {H₃} = record
         rewrite splitAt-↑ˡ (X + Y) (H₁.j e₁ i ↑ˡ Y) Z
         rewrite splitAt-↑ˡ X (H₁.j e₁ i) Y = cong ((_↑ˡ Y + Z) ∘ H₁.j e₁) (sym (cast-is-id refl i))
     ≗j e i | inj₁ e₁₂ | inj₂ e₂
-        rewrite splitAt-↑ʳ H₁.h H₂.h e₂
         rewrite splitAt-↑ʳ H₁.h (H₂.h + H₃.h) (e₂ ↑ˡ H₃.h)
         rewrite splitAt-↑ˡ H₂.h e₂ H₃.h
         rewrite splitAt-↑ˡ (X + Y) (X ↑ʳ H₂.j e₂ i) Z
@@ -551,7 +535,7 @@ n+0↔n n = record
     to∘from : (x : Fin n) → to (from x) ≡ x
     to∘from x rewrite splitAt-↑ˡ n x 0 = refl
 
-unitaryʳ : Hypergraph-same (map-nodes ([ id , (λ ()) ] ∘ splitAt n) (together H empty-hypergraph)) H
+unitaryʳ : Hypergraph-same (map-nodes ([ id , (λ ()) ] ∘ splitAt n) (together H (discrete {0}))) H
 unitaryʳ {n} {H} = record
     { ↔h = h+0↔h
     ; ≗a = ≗a
@@ -560,22 +544,22 @@ unitaryʳ {n} {H} = record
     }
   where
     module H = Hypergraph H
-    module H+0 = Hypergraph (together H empty-hypergraph)
+    module H+0 = Hypergraph (together H (discrete {0}))
     h+0↔h : Fin H+0.h ↔ Fin H.h
     h+0↔h = n+0↔n H.h
     ≗a : (e : Fin (H.h + 0)) → [ H.a , (λ ()) ] (splitAt H.h e) ≡ H.a (Inverse.to h+0↔h e)
     ≗a e with inj₁ e₁ ← splitAt H.h e in eq = refl
     ≗j  : (e : Fin (H.h + 0))
           (i : Fin ([ H.a , (λ ()) ] (splitAt H.h e)))
-        → [ (λ x → x) , (λ ()) ] (splitAt n (j+j H empty-hypergraph e i))
+        → [ (λ x → x) , (λ ()) ] (splitAt n (j+j H discrete e i))
         ≡ H.j (Inverse.to h+0↔h e) (cast (≗a e) i)
-    ≗j e i = ≗j-aux (splitAt H.h e) refl (j+j H empty-hypergraph e) refl (≗a e) i
+    ≗j e i = ≗j-aux (splitAt H.h e) refl (j+j H discrete e) refl (≗a e) i
       where
         ≗j-aux
             : (w : Fin H.h ⊎ Fin 0)
             → (eq₁ : splitAt H.h e ≡ w)
             → (w₁ : Fin ([ H.a , (λ ()) ] w) → Fin (n + 0))
-            → j+j H empty-hypergraph e ≡ subst (λ hole → Fin ([ H.a , (λ ()) ] hole) → Fin (n + 0)) (sym eq₁) w₁
+            → j+j H discrete e ≡ subst (λ hole → Fin ([ H.a , (λ ()) ] hole) → Fin (n + 0)) (sym eq₁) w₁
             → (w₂ : [ H.a , (λ ()) ] w ≡ H.a (Inverse.to h+0↔h e))
               (i : Fin ([ H.a , (λ ()) ] w))
             → [ (λ x → x) , (λ ()) ] (splitAt n (w₁ i))
@@ -586,7 +570,7 @@ unitaryʳ {n} {H} = record
                 (↑ˡ-injective 0 x (H.j e₁ i) (trans (splitAt⁻¹-↑ˡ eq₂) (sym (cong-app eq₁ i))))
                 (cong (H.j e₁) (sym (cast-is-id refl i)))
     ≗l  : (e : Fin (H.h + 0))
-        → l+l H empty-hypergraph e
+        → l+l H discrete e
         ≡ cast-gate (sym (≗a e)) (H.l (Inverse.to h+0↔h e))
     ≗l e with splitAt H.h e | {(≗a e)}
     ... | inj₁ e₁ = sym (cast-gate-is-id refl (H.l e₁))
@@ -658,39 +642,38 @@ braiding {n} {m} {H₁} {H₂} = record
     ≗l e | inj₁ e₁ rewrite splitAt-↑ʳ H₂.h H₁.h e₁ = sym (cast-gate-is-id refl (H₁.l e₁))
     ≗l e | inj₂ e₂ rewrite splitAt-↑ˡ H₂.h e₂ H₁.h = sym (cast-gate-is-id refl (H₂.l e₂))
 
-Circ : SymmetricMonoidalFunctor Nat,+,0 Setoids-×
-Circ = record
-    { F = F
-    ; isBraidedMonoidal = record
-        { isMonoidal = record
-            { ε = ε
-            ; ⊗-homo = ntHelper record
-                { η = λ { (m , n) → η }
-                ; commute = λ { (f , g) {H₁ , H₂} → commute {H₁ = H₁} {H₂ = H₂} f g }
-                }
-            ; associativity = λ { {X} {Y} {Z} {(H₁ , H₂) , H₃} → associativity {X} {Y} {Z} {H₁} {H₂} {H₃} }
-            ; unitaryˡ = Hypergraph-same-refl
-            ; unitaryʳ = unitaryʳ
-            }
-        ; braiding-compat = λ { {X} {Y} {H₁ , H₂} → braiding {X} {Y} {H₁} {H₂} }
-        }
-    }
-  where
-    η : Hypergraph-setoid n ×ₛ Hypergraph-setoid m ⟶ₛ Hypergraph-setoid (n + m)
-    η = record
-        { to = λ { (H₁ , H₂) → together H₁ H₂ }
-        ; cong = λ { (≡H₁ , ≡H₂) → together-resp-same ≡H₁ ≡H₂ }
-        }
+opaque
+  unfolding ×-symmetric′
+  Circ : SymmetricMonoidalFunctor Nat,+,0 Setoids-×
+  Circ = record
+      { F = F
+      ; isBraidedMonoidal = record
+          { isMonoidal = record
+              { ε = ε
+              ; ⊗-homo = ntHelper record
+                  { η = λ { (m , n) → η }
+                  ; commute = λ { (f , g) {H₁ , H₂} → commute {H₁ = H₁} {H₂ = H₂} f g }
+                  }
+              ; associativity = λ { {X} {Y} {Z} {(H₁ , H₂) , H₃} → associativity {X} {Y} {Z} {H₁} {H₂} {H₃} }
+              ; unitaryˡ = Hypergraph-same-refl
+              ; unitaryʳ = unitaryʳ
+              }
+          ; braiding-compat = λ { {X} {Y} {H₁ , H₂} → braiding {X} {Y} {H₁} {H₂} }
+          }
+      }
+    where
+      η : Hypergraph-setoid n ×ₛ Hypergraph-setoid m ⟶ₛ Hypergraph-setoid (n + m)
+      η = record
+          { to = λ { (H₁ , H₂) → together H₁ H₂ }
+          ; cong = λ { (≡H₁ , ≡H₂) → together-resp-same ≡H₁ ≡H₂ }
+          }
 
 module F = SymmetricMonoidalFunctor Circ
 
 open Gate
 
-and-gate : SingletonSetoid {c} {ℓ} ⟶ₛ F.₀ 3
-and-gate = record
-    { to = λ _ → and-graph
-    ; cong = λ _ → Hypergraph-same-refl
-    }
+and-gate : ⊤ₛ ⟶ₛ Hypergraph-setoid 3
+and-gate = Const ⊤ₛ (Hypergraph-setoid 3) and-graph
   where
     and-graph : Hypergraph 3
     and-graph = record
diff --git a/DecorationFunctor/Trivial.agda b/DecorationFunctor/Trivial.agda
index 3b88010..6278d05 100644
--- a/DecorationFunctor/Trivial.agda
+++ b/DecorationFunctor/Trivial.agda
@@ -2,85 +2,70 @@
 
 module DecorationFunctor.Trivial where
 
-import Categories.Morphism as Morphism
+open import Level using (0ℓ)
 
 open import Categories.Category.BinaryProducts using (module BinaryProducts)
 open import Categories.Category.Cartesian using (Cartesian)
-open import Categories.Category.Cocartesian using (Cocartesian; module BinaryCoproducts)
-open import Categories.Category.Core using (Category)
-open import Categories.Category.Instance.Nat using (Nat-Cocartesian)
 open import Categories.Category.Instance.Nat using (Nat)
 open import Categories.Category.Instance.Setoids using (Setoids)
-open import Categories.Category.Instance.SingletonSet using (SingletonSetoid)
 open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
 open import Categories.Category.Product using (_⁂_)
-open import Categories.Functor using () renaming (_∘F_ to _∘_)
-open import Categories.Functor.Core using (Functor)
+open import Categories.Functor using (Functor) renaming (_∘F_ to _∘_)
 open import Categories.Functor.Monoidal.Symmetric using (module Lax)
 open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
 open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
-open import Category.Instance.Setoids.SymmetricMonoidal using (Setoids-×)
 open import Category.Instance.Nat.FinitelyCocomplete using (Nat-FinitelyCocomplete)
-open import Data.Nat using (ℕ)
-open import Data.Product.Base using (_,_)
+open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×; ×-symmetric′)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Data.Setoid.Unit {0ℓ} {0ℓ} using (⊤ₛ)
 open import Data.Unit using (tt)
-open import Data.Unit.Properties using () renaming (≡-setoid to ⊤-setoid)
-open import Function.Base using (const)
-open import Function.Bundles using (Func)
-open import Level using (0ℓ; suc; lift)
-open import Relation.Binary.Bundles using (Setoid)
+open import Data.Unit.Properties using () renaming (≡-setoid to ⊤-≡ₛ)
+open import Function using (Func; const)
+open import Function.Construct.Constant using () renaming (function to Const)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
 
 open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products)
-open Cocartesian Nat-Cocartesian using (coproducts)
+open BinaryProducts products using (-×-)
 open FinitelyCocompleteCategory Nat-FinitelyCocomplete
-    using ()
-    renaming (symmetricMonoidalCategory to Nat-smc)
-open Morphism (Setoids 0ℓ 0ℓ) using (_≅_)
+  using (-+-)
+  renaming (symmetricMonoidalCategory to Nat-smc)
 open Lax using (SymmetricMonoidalFunctor)
 
-open BinaryProducts products using (-×-)
-open BinaryCoproducts coproducts using (-+-)
-
-
 F : Functor Nat (Setoids 0ℓ 0ℓ)
 F = record
-    { F₀ = const (⊤-setoid)
-    ; F₁ = const (record { to = const tt ; cong = const refl })
+    { F₀ = const ⊤-≡ₛ
+    ; F₁ = const (Const ⊤-≡ₛ ⊤-≡ₛ tt)
     ; identity = refl
     ; homomorphism = refl
     ; F-resp-≈ = const refl
     }
 
-ε : Func (SingletonSetoid {0ℓ} {0ℓ}) ⊤-setoid
-ε = record
-    { to = const tt
-    ; cong = const refl
-    }
+ε : Func ⊤ₛ ⊤-≡ₛ
+ε = Const ⊤ₛ ⊤-≡ₛ tt
 
 ⊗-homomorphism : NaturalTransformation (-×- ∘ (F ⁂ F)) (F ∘ -+-)
 ⊗-homomorphism = ntHelper record
-    { η = const (record { to = const tt ; cong = const refl })
+    { η = const (Const (⊤-≡ₛ ×ₛ ⊤-≡ₛ) ⊤-≡ₛ tt)
     ; commute = const refl
     }
 
-trivial : SymmetricMonoidalFunctor Nat-smc (Setoids-× {0ℓ})
-trivial = record
-    { F = F
-    ; isBraidedMonoidal = record
-        { isMonoidal = record
-            { ε = ε
-            ; ⊗-homo = ⊗-homomorphism
-            ; associativity = refl
-            ; unitaryˡ = refl
-            ; unitaryʳ = refl
-            }
-        ; braiding-compat = refl
-        }
-    }
+opaque
+  unfolding ×-symmetric′
 
-and-gate : Func (SingletonSetoid {0ℓ} {0ℓ}) ⊤-setoid
-and-gate = record
-    { to = const tt
-    ; cong = const refl
-    }
+  trivial : SymmetricMonoidalFunctor Nat-smc Setoids-×
+  trivial = record
+      { F = F
+      ; isBraidedMonoidal = record
+          { isMonoidal = record
+              { ε = ε
+              ; ⊗-homo = ⊗-homomorphism
+              ; associativity = refl
+              ; unitaryˡ = refl
+              ; unitaryʳ = refl
+              }
+          ; braiding-compat = refl
+          }
+      }
+
+and-gate : Func ⊤ₛ ⊤-≡ₛ
+and-gate = Const ⊤ₛ ⊤-≡ₛ tt
diff --git a/Functor/Monoidal/Instance/Nat/Circ.agda b/Functor/Monoidal/Instance/Nat/Circ.agda
index 0e2d3eb..1b45a75 100644
--- a/Functor/Monoidal/Instance/Nat/Circ.agda
+++ b/Functor/Monoidal/Instance/Nat/Circ.agda
@@ -14,7 +14,7 @@ open import Category.Monoidal.Instance.Nat using (Nat,+,0)
 open import Categories.Category.Construction.Monoids using (Monoids)
 open import Categories.Category.Instance.Nat using (Nat; Nat-Cocartesian)
 open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
-open import Categories.Category.Instance.SingletonSet using (SingletonSetoid)
+open import Data.Setoid.Unit using (⊤ₛ)
 open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
 open import Categories.Category.Cartesian using (Cartesian)
 open Cartesian (Setoids-Cartesian {suc 0ℓ} {suc 0ℓ}) using (products)
@@ -54,7 +54,7 @@ module MultisetOf,++,[] = SymmetricMonoidalFunctor MultisetOf,++,[]
 
 open SymmetricMonoidalFunctor
 
-ε⇒ : SingletonSetoid ⟶ₛ Circuitₛ 0
+ε⇒ : ⊤ₛ ⟶ₛ Circuitₛ 0
 ε⇒ = mkCircuitₛ ∙ MultisetOf,++,[].ε
 
 open Cocartesian Nat-Cocartesian using (-+-)
diff --git a/Functor/Monoidal/Instance/Nat/Preimage.agda b/Functor/Monoidal/Instance/Nat/Preimage.agda
index 59c9391..844df79 100644
--- a/Functor/Monoidal/Instance/Nat/Preimage.agda
+++ b/Functor/Monoidal/Instance/Nat/Preimage.agda
@@ -4,7 +4,7 @@ module Functor.Monoidal.Instance.Nat.Preimage where
 
 open import Category.Monoidal.Instance.Nat using (Natop,+,0; Natop-Cartesian)
 open import Categories.Category.Instance.Nat using (Nat-Cocartesian)
-open import Categories.Category.Instance.SingletonSet using (SingletonSetoid)
+open import Data.Setoid.Unit using (⊤ₛ)
 open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
 open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
 open import Categories.Category.BinaryProducts using (module BinaryProducts)
@@ -38,7 +38,7 @@ open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; mo
 open import Data.Bool.Base using (Bool)
 
 open Func
-Preimage-ε : SingletonSetoid {0ℓ} {0ℓ} ⟶ₛ Subsetₛ 0
+Preimage-ε : ⊤ₛ {0ℓ} {0ℓ} ⟶ₛ Subsetₛ 0
 to Preimage-ε x = []
 cong Preimage-ε x ()
 
diff --git a/Functor/Monoidal/Instance/Nat/Pull.agda b/Functor/Monoidal/Instance/Nat/Pull.agda
index 1d3d338..b267f97 100644
--- a/Functor/Monoidal/Instance/Nat/Pull.agda
+++ b/Functor/Monoidal/Instance/Nat/Pull.agda
@@ -14,7 +14,7 @@ open import Categories.Category.Cartesian using (Cartesian)
 open import Categories.Category.Cocartesian using (Cocartesian; BinaryCoproducts)
 open import Categories.Category.Instance.Nat using (Nat)
 open import Categories.Category.Instance.Nat using (Nat-Cocartesian)
-open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ)
+open import Data.Setoid.Unit using (⊤ₛ)
 open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
 open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
 open import Categories.Category.Product using (_⁂_)
@@ -43,8 +43,6 @@ open import Functor.Instance.Nat.Pull using (Pull; Pull-defs)
 open import Relation.Binary using (Setoid)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; module ≡-Reasoning)
 
-module Setoids-× = SymmetricMonoidalCategory Setoids-×
-
 open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products)
 
 open BinaryProducts products using (-×-)
diff --git a/Functor/Monoidal/Instance/Nat/Push.agda b/Functor/Monoidal/Instance/Nat/Push.agda
index b53282d..2e8c0cf 100644
--- a/Functor/Monoidal/Instance/Nat/Push.agda
+++ b/Functor/Monoidal/Instance/Nat/Push.agda
@@ -10,7 +10,7 @@ open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
 open import Level using (0ℓ; Level)
 open import Relation.Binary using (Rel; Setoid)
 open import Functor.Instance.Nat.Push using (Push; Push-defs)
-open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ)
+open import Data.Setoid.Unit using (⊤ₛ)
 open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
 open import Data.Vec.Functional as Vec using (Vector)
 open import Data.Vector using (++-assoc; ++-↑ˡ; ++-↑ʳ)
diff --git a/Functor/Monoidal/Instance/Nat/System.agda b/Functor/Monoidal/Instance/Nat/System.agda
index 2201c35..6659fb3 100644
--- a/Functor/Monoidal/Instance/Nat/System.agda
+++ b/Functor/Monoidal/Instance/Nat/System.agda
@@ -29,7 +29,7 @@ open import Categories.Category.Cartesian using (Cartesian)
 open import Categories.Category.Cocartesian using (Cocartesian)
 open import Categories.Category.Instance.Nat using (Nat; Nat-Cocartesian; Natop)
 open import Categories.Category.Instance.Setoids using (Setoids)
-open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ)
+open import Data.Setoid.Unit using (⊤ₛ)
 open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
 open import Categories.Category.Product using (Product)
 open import Categories.Category.Product using (_⁂_)
diff --git a/NaturalTransformation/Instance/EmptyList.agda b/NaturalTransformation/Instance/EmptyList.agda
index 0e069d2..9f94955 100644
--- a/NaturalTransformation/Instance/EmptyList.agda
+++ b/NaturalTransformation/Instance/EmptyList.agda
@@ -4,12 +4,12 @@ open import Level using (Level; _⊔_)
 
 module NaturalTransformation.Instance.EmptyList {c ℓ : Level} where
 
-open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ)
 open import Categories.Functor using (Functor)
 open import Categories.Functor.Construction.Constant using (const)
 open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
 open import Data.Opaque.List using (Listₛ; []ₛ; mapₛ)
 open import Data.Setoid using (_⇒ₛ_)
+open import Data.Setoid.Unit using (⊤ₛ)
 open import Function using (_⟶ₛ_)
 open import Function.Construct.Constant using () renaming (function to Const)
 open import Function.Construct.Setoid using (_∙_)