diff options
Diffstat (limited to 'DecorationFunctor/Trivial.agda')
| -rw-r--r-- | DecorationFunctor/Trivial.agda | 85 |
1 files changed, 35 insertions, 50 deletions
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 |