diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-07-10 17:21:14 -0700 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-07-10 17:21:14 -0700 |
| commit | a408cbee9abbe2dbeee09bd36afc678efe7b6557 (patch) | |
| tree | 22d6f05d6ce81357629fa2864305b81d68eed52e /Functor/Cartesian | |
| parent | 7875edd03cce586a8c9f0b95dedffb390bfdbd61 (diff) | |
Use latest agda-categories
Diffstat (limited to 'Functor/Cartesian')
| -rw-r--r-- | Functor/Cartesian/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda | 12 |
1 files changed, 2 insertions, 10 deletions
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.⊤) |