From a408cbee9abbe2dbeee09bd36afc678efe7b6557 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Fri, 10 Jul 2026 17:21:14 -0700 Subject: Use latest agda-categories --- .../Underlying/SymmetricMonoidal/FinitelyCocomplete.agda | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) (limited to 'Functor/Cartesian/Instance/Underlying/SymmetricMonoidal') diff --git a/Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda b/Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda index 346999b..537ac38 100644 --- a/Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda +++ b/Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda @@ -26,16 +26,8 @@ open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategor open import Category.Cartesian.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat-CC) open import Functor.Instance.Underlying.SymmetricMonoidal.FinitelyCocomplete {o} {ℓ} {e} using () renaming (Underlying to U) -module CartesianCategory′ {o ℓ e : Level} (C : CartesianCategory o ℓ e) where - module CC = CartesianCategory C - open import Categories.Object.Terminal using (Terminal) - open Terminal CC.terminal public - open import Categories.Category.BinaryProducts using (BinaryProducts) - open BinaryProducts CC.products public - open CC public - -module FC = CartesianCategory′ FinitelyCocompletes-CC -module SMC = CartesianCategory′ SymMonCat-CC +module FC = CartesianCategory FinitelyCocompletes-CC +module SMC = CartesianCategory SymMonCat-CC module U = Functor U F-resp-⊤ : IsTerminal SMC.U (U.₀ FC.⊤) -- cgit v1.2.3