diff options
Diffstat (limited to 'Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda')
| -rw-r--r-- | Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda b/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda index 8bf567d..ebb3dc0 100644 --- a/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda +++ b/Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda @@ -5,7 +5,7 @@ module Functor.Free.Instance.SymmetricMonoidalPreorder.Lax where import Functor.Free.Instance.MonoidalPreorder.Lax as MP open import Categories.Category using (Category) -open import Category.Instance.SymMonCat using (SymMonCat) +open import Category.Instance.SymMonCat using (module Lax) open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) open import Categories.Functor using (Functor) open import Categories.Functor.Monoidal.Symmetric using () renaming (module Lax to Lax₁) @@ -54,7 +54,7 @@ module _ {o ℓ e : Level} where → symmetricMonoidalMonotone F ≃ symmetricMonoidalMonotone G pointwiseIsomorphism F≃G = MP.Free.F-resp-≈ ⌊ F≃G ⌋ -Free : {o ℓ e : Level} → Functor (SymMonCat {o} {ℓ} {e}) (SymMonPre o ℓ) +Free : {o ℓ e : Level} → Functor (Lax.SymMonCat {o} {ℓ} {e}) (SymMonPre o ℓ) Free = record { F₀ = symmetricMonoidalPreorder ; F₁ = symmetricMonoidalMonotone |