From 38e5da80b651a073b49505a92d71b15ca11e1b35 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Tue, 13 Jan 2026 17:35:37 -0600 Subject: Fix modules broken by addition of strong SymMonCat --- Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'Functor/Instance/Underlying/SymmetricMonoidal') 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 -- cgit v1.2.3