blob: 2fceccec84a0c490785882b7e0bb9fb8322a5621 (
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
|
{-# OPTIONS --without-K --safe #-}
module Functor.Free.Instance.SymmetricMonoidalPreorder where
import Functor.Free.Instance.MonoidalPreorder 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.SymMonPre.Primitive using (SymMonPre; _≃_; module ≃)
open import Data.Product using (_,_)
open import Level using (Level)
open import Preorder.Primitive.Monoidal using (MonoidalPreorder; SymmetricMonoidalPreorder; 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})
|
