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
|
{-# 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; module CocartesianMonoidal; 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 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 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 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 Natop-Cocartesian
Natop,×,1 .symmetric = +-symmetric Natop Natop-Cocartesian
open Symmetric public
|
