diff options
Diffstat (limited to 'Category/Instance/FinitelyCocompletes.agda')
| -rw-r--r-- | Category/Instance/FinitelyCocompletes.agda | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/Category/Instance/FinitelyCocompletes.agda b/Category/Instance/FinitelyCocompletes.agda index 2766df2..9bee58e 100644 --- a/Category/Instance/FinitelyCocompletes.agda +++ b/Category/Instance/FinitelyCocompletes.agda @@ -1,29 +1,31 @@ {-# OPTIONS --without-K --safe #-} -open import Level using (Level) + +open import Level using (Level; suc; _⊔_) + module Category.Instance.FinitelyCocompletes {o ℓ e : Level} where +import Category.Instance.One.Properties as OneProps + open import Categories.Category using (_[_,_]) open import Categories.Category.BinaryProducts using (BinaryProducts) open import Categories.Category.Cartesian using (Cartesian) -open import Categories.Category.Helper using (categoryHelper) -open import Categories.Category.Monoidal.Instance.Cats using () renaming (module Product to Products) open import Categories.Category.Core using (Category) +open import Categories.Category.Helper using (categoryHelper) open import Categories.Category.Instance.Cats using (Cats) open import Categories.Category.Instance.One using (One; One-⊤) +open import Categories.Category.Monoidal.Instance.Cats using () renaming (module Product to Products) open import Categories.Category.Product using (πˡ; πʳ; _※_; _⁂_) renaming (Product to ProductCat) open import Categories.Diagram.Coequalizer using (IsCoequalizer) open import Categories.Functor using (Functor) renaming (id to idF) +open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; associator; unitorˡ; unitorʳ; module ≃; _ⓘₕ_) open import Categories.Object.Coproduct using (IsCoproduct) open import Categories.Object.Initial using (IsInitial) open import Categories.Object.Product.Core using (Product) -open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; associator; unitorˡ; unitorʳ; module ≃; _ⓘₕ_) open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) open import Category.Cocomplete.Finitely.Product using (FinitelyCocomplete-×) -open import Category.Instance.One.Properties using (One-FinitelyCocomplete) open import Data.Product.Base using (_,_; proj₁; proj₂; map; dmap; zip′) -open import Functor.Exact using (∘-RightExactFunctor; RightExactFunctor; idREF; IsRightExact; rightexact) open import Function.Base using (id; flip) -open import Level using (Level; suc; _⊔_) +open import Functor.Exact using (∘-RightExactFunctor; RightExactFunctor; idREF; IsRightExact; rightexact) FinitelyCocompletes : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) FinitelyCocompletes = categoryHelper record @@ -48,7 +50,7 @@ FinitelyCocompletes = categoryHelper record One-FCC : FinitelyCocompleteCategory o ℓ e One-FCC = record { U = One - ; finCo = One-FinitelyCocomplete + ; finCo = OneProps.finitelyCocomplete } _×_ @@ -62,7 +64,6 @@ _×_ 𝒞 𝒟 = record where module 𝒞 = FinitelyCocompleteCategory 𝒞 module 𝒟 = FinitelyCocompleteCategory 𝒟 -{-# INJECTIVE_FOR_INFERENCE _×_ #-} module _ (𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e) where |