blob: 8af8633ec3026af1e22aa95c85591b76f19b59af (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
{-# OPTIONS --without-K --safe #-}
module Category.Cocomplete.Finitely.Bundle where
open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory)
open import Categories.Category.Core using (Category)
open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete)
open import Category.Cocomplete.Finitely.SymmetricMonoidal using (module FinitelyCocompleteSymmetricMonoidal)
open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
open import Level using (_⊔_; suc)
record FinitelyCocompleteCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
field
U : Category o ℓ e
finCo : FinitelyCocomplete U
open Category U public
open FinitelyCocomplete finCo public
open FinitelyCocompleteSymmetricMonoidal finCo
using ()
renaming (+-monoidal to monoidal; +-symmetric to symmetric)
public
symmetricMonoidalCategory : SymmetricMonoidalCategory o ℓ e
symmetricMonoidalCategory = record
{ U = U
; monoidal = monoidal
; symmetric = symmetric
}
{-# INJECTIVE_FOR_INFERENCE symmetricMonoidalCategory #-}
cocartesianCategory : CocartesianCategory o ℓ e
cocartesianCategory = record
{ U = U
; cocartesian = cocartesian
}
|
