diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-10-28 12:26:54 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-10-28 12:26:54 -0500 |
| commit | 8ac913160fcb3e6ec6af2b0f4cb25f45edd8212b (patch) | |
| tree | ea0ed1ba72624f8f654a820c10521c8acac9ffec /Functor/Monoidal/Instance/Nat/Push.agda | |
| parent | 117ecc76cb40ad6367d8fe6d5b854cbe13a613bf (diff) | |
Add symmetric monoidal structure to Pull and System
Diffstat (limited to 'Functor/Monoidal/Instance/Nat/Push.agda')
| -rw-r--r-- | Functor/Monoidal/Instance/Nat/Push.agda | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Functor/Monoidal/Instance/Nat/Push.agda b/Functor/Monoidal/Instance/Nat/Push.agda index 2ccfc27..30ed745 100644 --- a/Functor/Monoidal/Instance/Nat/Push.agda +++ b/Functor/Monoidal/Instance/Nat/Push.agda @@ -9,7 +9,7 @@ open import Function.Base using (_∘_; case_of_; _$_; id) 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 (Values; Push; Push₁; Push-identity) +open import Functor.Instance.Nat.Push using (Push; Push₁; Push-identity) open import Categories.Category.Instance.SingletonSet using (SingletonSetoid) open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) open import Data.Vec.Functional using (Vector; []; _++_; head; tail) @@ -52,7 +52,7 @@ open import Data.Fin.Permutation using (Permutation; _⟨$⟩ʳ_; _⟨$⟩ˡ_) open Dual.op-binaryProducts using () renaming (assocˡ∘⟨⟩ to []∘assocʳ; swap∘⟨⟩ to []∘swap) open import Relation.Nullary.Decidable using (does; does-⇔; dec-false) - +open import Data.System.Values Value using (Values) open Func Push-ε : SingletonSetoid {0ℓ} {0ℓ} ⟶ₛ Values 0 |