diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-13 17:35:37 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-13 17:35:37 -0600 |
| commit | 38e5da80b651a073b49505a92d71b15ca11e1b35 (patch) | |
| tree | cf0779c8afb48d7c5b9e82eb2c2816be5860032d | |
| parent | 4e85ade36a25151021a74b51442dca999e1b48e2 (diff) | |
Fix modules broken by addition of strong SymMonCatmain
| -rw-r--r-- | Category/Cartesian/Instance/SymMonCat.agda | 4 | ||||
| -rw-r--r-- | Category/Instance/Properties/SymMonCat.agda | 3 | ||||
| -rw-r--r-- | Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda | 4 |
3 files changed, 8 insertions, 3 deletions
diff --git a/Category/Cartesian/Instance/SymMonCat.agda b/Category/Cartesian/Instance/SymMonCat.agda index 7d91d52..1b4af4a 100644 --- a/Category/Cartesian/Instance/SymMonCat.agda +++ b/Category/Cartesian/Instance/SymMonCat.agda @@ -4,10 +4,12 @@ open import Level using (Level; suc; _⊔_) module Category.Cartesian.Instance.SymMonCat {o ℓ e : Level} where -open import Category.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat) +open import Category.Instance.SymMonCat {o} {ℓ} {e} using (module Lax) open import Category.Instance.Properties.SymMonCat {o} {ℓ} {e} using (SymMonCat-Cartesian) open import Categories.Category.Cartesian.Bundle using (CartesianCategory) +open Lax using (SymMonCat) + SymMonCat-CC : CartesianCategory (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) SymMonCat-CC = record { U = SymMonCat diff --git a/Category/Instance/Properties/SymMonCat.agda b/Category/Instance/Properties/SymMonCat.agda index 3b49b26..2afde0a 100644 --- a/Category/Instance/Properties/SymMonCat.agda +++ b/Category/Instance/Properties/SymMonCat.agda @@ -9,7 +9,8 @@ import Categories.Morphism.Reasoning as ⇒-Reasoning import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric as SMNI import Categories.Functor.Monoidal.Symmetric {o} {o} {ℓ} {ℓ} {e} {e} as SMF -open import Category.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat) +open import Category.Instance.SymMonCat {o} {ℓ} {e} using (module Lax) +open Lax using (SymMonCat) open import Categories.Category using (Category; _[_≈_]; _[_∘_]) open import Categories.Object.Product.Core SymMonCat using (Product) diff --git a/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda b/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda index 77064ba..8fabddd 100644 --- a/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda +++ b/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda @@ -26,13 +26,15 @@ open import Data.Product.Base using (_,_) open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes) open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) -open import Category.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat) +open import Category.Instance.SymMonCat {o} {ℓ} {e} using () renaming (module Lax to Lax′) open import Functor.Exact using (RightExactFunctor; idREF; ∘-RightExactFunctor) open FinitelyCocompleteCategory using () renaming (symmetricMonoidalCategory to smc) open SymmetricMonoidalCategory using (unit) renaming (braidedMonoidalCategory to bmc) open BraidedMonoidalCategory using () renaming (monoidalCategory to mc) +open Lax′ using (SymMonCat) + private variable A B C : FinitelyCocompleteCategory o ℓ e |