From b2c2426959715260f57153b91ce11d12c7fdb298 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Wed, 7 Jan 2026 10:52:51 -0600 Subject: Add strong variants of cats to preorders functors --- Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Functor/Free/Instance/SymmetricMonoidalPreorder/Lax.agda') 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 -- cgit v1.2.3