Add trivial and graph decoration functorsmain

1 files changed, 87 insertions, 0 deletions

diff --git a/DecorationFunctor/Trivial.agda b/DecorationFunctor/Trivial.agda
new file mode 100644
index 0000000..dee7c2e
--- /dev/null
+++ b/DecorationFunctor/Trivial.agda
@@ -0,0 +1,87 @@
+{-# OPTIONS --without-K --safe #-}
+
+module DecorationFunctor.Trivial where
+
+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)
+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 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 Relation.Binary.PropositionalEquality.Core using (refl)
+
+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 (_≅_)
+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 })
+    ; identity = const refl
+    ; homomorphism = const refl
+    ; F-resp-≈ = const (const refl)
+    }
+
+ε : Func (SingletonSetoid {0ℓ} {0ℓ}) ⊤-setoid
+ε = record
+    { to = const tt
+    ; cong = const refl
+    }
+
+⊗-homomorphism : NaturalTransformation (-×- ∘ (F ⁂ F)) (F ∘ -+-)
+⊗-homomorphism = record
+    { η = const (record { to = const tt ; cong = const refl })
+    ; commute = const (const refl)
+    ; sym-commute = const (const refl)
+    }
+
+trivial : SymmetricMonoidalFunctor Nat-smc (Setoids-× {0ℓ})
+trivial = record
+    { F = F
+    ; isBraidedMonoidal = record
+        { isMonoidal = record
+            { ε = ε
+            ; ⊗-homo = ⊗-homomorphism
+            ; associativity = const refl
+            ; unitaryˡ = const refl
+            ; unitaryʳ = const refl
+            }
+        ; braiding-compat = const refl
+        }
+    }
+
+and-gate : Func (SingletonSetoid {0ℓ} {0ℓ}) ⊤-setoid
+and-gate = record
+    { to = const tt
+    ; cong = const refl
+    }