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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
{-# OPTIONS --without-K --safe #-}
module Category.Monoidal.Instance.Nat where
open import Level using (0ℓ)
open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory)
open import Categories.Category.Instance.Nat using (Nat; Nat-Cartesian; Nat-Cocartesian; Natop)
open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.Cocartesian using (Cocartesian)
open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal)
open import Categories.Category.Cocartesian.SymmetricMonoidal using (module CocartesianSymmetricMonoidal)
open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal)
open import Categories.Category.Duality using (coCartesian⇒Cocartesian; Cocartesian⇒coCartesian)
import Categories.Category.Cartesian.SymmetricMonoidal as CartesianSymmetricMonoidal
Natop-Cartesian : Cartesian Natop
Natop-Cartesian = Cocartesian⇒coCartesian Nat Nat-Cocartesian
Natop-Cocartesian : Cocartesian Natop
Natop-Cocartesian = coCartesian⇒Cocartesian Natop Nat-Cartesian
module Monoidal where
open MonoidalCategory
open CartesianMonoidal using () renaming (monoidal to ×-monoidal)
open CocartesianMonoidal using (+-monoidal)
Nat,+,0 : MonoidalCategory 0ℓ 0ℓ 0ℓ
Nat,+,0 .U = Nat
Nat,+,0 .monoidal = +-monoidal Nat-Cocartesian
Nat,×,1 : MonoidalCategory 0ℓ 0ℓ 0ℓ
Nat,×,1 .U = Nat
Nat,×,1 .monoidal = ×-monoidal Nat-Cartesian
Natop,+,0 : MonoidalCategory 0ℓ 0ℓ 0ℓ
Natop,+,0 .U = Natop
Natop,+,0 .monoidal = ×-monoidal Natop-Cartesian
Natop,×,1 : MonoidalCategory 0ℓ 0ℓ 0ℓ
Natop,×,1 .U = Natop
Natop,×,1 .monoidal = +-monoidal Natop-Cocartesian
module Symmetric where
open SymmetricMonoidalCategory
open CartesianMonoidal using () renaming (monoidal to ×-monoidal)
open CocartesianMonoidal using (+-monoidal)
open CartesianSymmetricMonoidal using () renaming (symmetric to ×-symmetric)
open CocartesianSymmetricMonoidal using (+-symmetric)
Nat,+,0 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ
Nat,+,0 .U = Nat
Nat,+,0 .monoidal = +-monoidal Nat-Cocartesian
Nat,+,0 .symmetric = +-symmetric Nat Nat-Cocartesian
Nat,×,1 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ
Nat,×,1 .U = Nat
Nat,×,1 .monoidal = ×-monoidal Nat-Cartesian
Nat,×,1 .symmetric = ×-symmetric Nat Nat-Cartesian
Natop,+,0 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ
Natop,+,0 .U = Natop
Natop,+,0 .monoidal = ×-monoidal Natop-Cartesian
Natop,+,0 .symmetric = ×-symmetric Natop Natop-Cartesian
Natop,×,1 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ
Natop,×,1 .U = Natop
Natop,×,1 .monoidal = +-monoidal Natop-Cocartesian
Natop,×,1 .symmetric = +-symmetric Natop Natop-Cocartesian
open Symmetric public
|
