diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-07 10:52:51 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-07 10:52:51 -0600 |
| commit | b2c2426959715260f57153b91ce11d12c7fdb298 (patch) | |
| tree | 2c40fe1b8d79732dedb4a9ddce957559c67fe05e /Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda | |
| parent | 8ec259bb32b4339b27560f5ea13afa81b9b8febc (diff) | |
Add strong variants of cats to preorders functors
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 |