blob: f759f1707fe1ddb7911804589665c0e8d1c728c2 (
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
60
61
62
63
64
65
66
67
68
|
{-# OPTIONS --without-K --safe #-}
module Functor.Free.Instance.SymmetricMonoidalPreorder.Strong where
import Functor.Free.Instance.MonoidalPreorder.Strong as MP
open import Categories.Category using (Category)
open import Category.Instance.SymMonCat using (module Strong)
open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
open import Categories.Functor using (Functor)
open import Categories.Functor.Monoidal.Symmetric using () renaming (module Strong to Strong₁)
open import Categories.Functor.Monoidal.Symmetric.Properties using (∘-StrongSymmetricMonoidal)
open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric using () renaming (module Strong to Strong₂)
open import Category.Instance.Preorder.Primitive.Monoidals.Symmetric.Strong using (SymMonPre; _≃_; module ≃)
open import Data.Product using (_,_)
open import Level using (Level)
open import Preorder.Primitive.Monoidal using (MonoidalPreorder; SymmetricMonoidalPreorder)
open import Preorder.Primitive.MonotoneMap.Monoidal.Strong using (SymmetricMonoidalMonotone)
open Strong₁ using (SymmetricMonoidalFunctor)
open Strong₂ using (SymmetricMonoidalNaturalIsomorphism)
-- The free symmetric monoidal preorder of a symmetric monoidal category
module _ {o ℓ e : Level} where
symmetricMonoidalPreorder : SymmetricMonoidalCategory o ℓ e → SymmetricMonoidalPreorder o ℓ
symmetricMonoidalPreorder C = record
{ M
; symmetric = record
{ symmetric = λ x y → braiding.⇒.η (x , y)
}
}
where
open SymmetricMonoidalCategory C
module M = MonoidalPreorder (MP.Free.₀ monoidalCategory)
module _ {A B : SymmetricMonoidalCategory o ℓ e} where
symmetricMonoidalMonotone
: SymmetricMonoidalFunctor A B
→ SymmetricMonoidalMonotone (symmetricMonoidalPreorder A) (symmetricMonoidalPreorder B)
symmetricMonoidalMonotone F = record
{ monoidalMonotone = MP.Free.₁ F.monoidalFunctor
}
where
module F = SymmetricMonoidalFunctor F
open SymmetricMonoidalNaturalIsomorphism using (⌊_⌋)
pointwiseIsomorphism
: {F G : SymmetricMonoidalFunctor A B}
→ SymmetricMonoidalNaturalIsomorphism F G
→ symmetricMonoidalMonotone F ≃ symmetricMonoidalMonotone G
pointwiseIsomorphism F≃G = MP.Free.F-resp-≈ ⌊ F≃G ⌋
Free : {o ℓ e : Level} → Functor (Strong.SymMonCat {o} {ℓ} {e}) (SymMonPre o ℓ)
Free = record
{ F₀ = symmetricMonoidalPreorder
; F₁ = symmetricMonoidalMonotone
; identity = λ {A} → ≃.refl {A = symmetricMonoidalPreorder A} {x = id}
; homomorphism = λ {f = f} {h} → ≃.refl {x = symmetricMonoidalMonotone (∘-StrongSymmetricMonoidal h f)}
; F-resp-≈ = pointwiseIsomorphism
}
where
open Category (SymMonPre _ _) using (id)
module Free {o ℓ e} = Functor (Free {o} {ℓ} {e})
|
