blob: 8bf567dfc49d29444661a0bbfcbfe92246479f9d (
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.Lax where
import Functor.Free.Instance.MonoidalPreorder.Lax as MP
open import Categories.Category using (Category)
open import Category.Instance.SymMonCat using (SymMonCat)
open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
open import Categories.Functor using (Functor)
open import Categories.Functor.Monoidal.Symmetric using () renaming (module Lax to Lax₁)
open import Categories.Functor.Monoidal.Symmetric.Properties using (∘-SymmetricMonoidal)
open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric using () renaming (module Lax to Lax₂)
open import Category.Instance.Preorder.Primitive.Monoidals.Symmetric.Lax 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.Lax using (SymmetricMonoidalMonotone)
open Lax₁ using (SymmetricMonoidalFunctor)
open Lax₂ 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 (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 (∘-SymmetricMonoidal h f)}
; F-resp-≈ = pointwiseIsomorphism
}
where
open Category (SymMonPre _ _) using (id)
module Free {o ℓ e} = Functor (Free {o} {ℓ} {e})
|
