blob: b5bf13525ee9b15856184490c84ee369c95ea4dc (
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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
{-# OPTIONS --without-K --safe #-}
open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
module Category.Construction.SymmetricMonoidalFunctors
{o ℓ e o′ ℓ′ e′}
(C : SymmetricMonoidalCategory o ℓ e)
(D : SymmetricMonoidalCategory o′ ℓ′ e′)
where
-- The functor category for a given pair of symmetric monoidal categories
open import Level using (_⊔_)
open import Relation.Binary.Construct.On using (isEquivalence)
open import Categories.Category using (Category)
open import Categories.Category.Helper using (categoryHelper)
open import Categories.Functor.Monoidal.Symmetric using () renaming (module Lax to Lax₁; module Strong to Strong₁)
open import Categories.NaturalTransformation.Monoidal.Symmetric using () renaming (module Lax to Lax₂; module Strong to Strong₂)
open import Categories.NaturalTransformation.Equivalence using (_≃_; ≃-isEquivalence)
open SymmetricMonoidalCategory D
module Lax where
open Lax₂.SymmetricMonoidalNaturalTransformation using (U)
SymmetricMonoidalFunctors
: Category (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) (o ⊔ e′)
SymmetricMonoidalFunctors = categoryHelper record
{ Obj = Lax₁.SymmetricMonoidalFunctor C D
; _⇒_ = Lax₂.SymmetricMonoidalNaturalTransformation
; _≈_ = λ α β → U α ≃ U β
; id = Lax₂.id
; _∘_ = Lax₂._∘ᵥ_
; assoc = assoc
; identityˡ = identityˡ
; identityʳ = identityʳ
; equiv = isEquivalence U ≃-isEquivalence
; ∘-resp-≈ = λ α₁≈β₁ α₂≈β₂ → ∘-resp-≈ α₁≈β₁ α₂≈β₂
}
module Strong where
open Strong₂.SymmetricMonoidalNaturalTransformation using (U)
SymmetricMonoidalFunctors
: Category (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) (o ⊔ e′)
SymmetricMonoidalFunctors = categoryHelper record
{ Obj = Strong₁.SymmetricMonoidalFunctor C D
; _⇒_ = Strong₂.SymmetricMonoidalNaturalTransformation
; _≈_ = λ α β → U α ≃ U β
; id = Strong₂.id
; _∘_ = Strong₂._∘ᵥ_
; assoc = assoc
; identityˡ = identityˡ
; identityʳ = identityʳ
; equiv = isEquivalence U ≃-isEquivalence
; ∘-resp-≈ = λ α₁≈β₁ α₂≈β₂ → ∘-resp-≈ α₁≈β₁ α₂≈β₂
}
|
