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
72
73
74
75
76
77
78
79
80
81
82
83
84
|
{-# OPTIONS --without-K --safe #-}
open import Level using (Level)
module Category.Monoidal.Instance.Posets {c ℓ₁ ℓ₂ : Level} where
open import Categories.Category.Instance.Posets using (Posets)
open import Categories.Category.Monoidal using (Monoidal)
open import Categories.Functor.Bifunctor using (Bifunctor)
open import Categories.Morphism (Posets c ℓ₁ ℓ₂) using (_≅_)
open import Data.Product using (_,_; map; proj₁; proj₂; assocʳ′; assocˡ′)
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (×-poset)
open import Data.Unit.Polymorphic using (⊤; tt)
open import Relation.Binary using (Poset)
open import Relation.Binary.Morphism.Bundles using (PosetHomomorphism; mkPosetHomo)
open Poset using (module Eq)
open PosetHomomorphism using (⟦_⟧; mono)
private
⊗ : Bifunctor (Posets c ℓ₁ ℓ₂) (Posets c ℓ₁ ℓ₂) (Posets c ℓ₁ ℓ₂)
⊗ = record
{ F₀ = λ (P , Q) → ×-poset P Q
; F₁ = λ (f , g) → mkPosetHomo _ _ (map ⟦ f ⟧ ⟦ g ⟧) (map (mono f) (mono g))
; identity = λ { {x , y} → Eq.refl x , Eq.refl y }
; homomorphism = λ { {_} {_} {e , f} → Eq.refl e , Eq.refl f }
; F-resp-≈ = λ (x , y) → x , y
}
unit : Poset c ℓ₁ ℓ₂
unit = record
{ Carrier = ⊤
; _≈_ = λ _ _ → ⊤
; _≤_ = λ _ _ → ⊤
; isPartialOrder = _
}
unitorˡ : {X : Poset c ℓ₁ ℓ₂} → ×-poset unit X ≅ X
unitorˡ {X} = record
{ from = mkPosetHomo _ _ proj₂ proj₂
; to = mkPosetHomo _ _ (tt ,_) (tt ,_)
; iso = record
{ isoˡ = tt , Eq.refl X
; isoʳ = Eq.refl X
}
}
unitorʳ : {X : Poset c ℓ₁ ℓ₂} → ×-poset X unit ≅ X
unitorʳ {X} = record
{ from = mkPosetHomo _ _ proj₁ proj₁
; to = mkPosetHomo _ _ (_, tt) (_, tt)
; iso = record
{ isoˡ = Eq.refl X , tt
; isoʳ = Eq.refl X
}
}
associator : {X Y Z : Poset c ℓ₁ ℓ₂} → ×-poset (×-poset X Y) Z ≅ ×-poset X (×-poset Y Z)
associator {X} {Y} {Z} = record
{ from = mkPosetHomo _ _ assocʳ′ assocʳ′
; to = mkPosetHomo _ _ assocˡ′ assocˡ′
; iso = record
{ isoˡ = (Eq.refl X , Eq.refl Y) , Eq.refl Z
; isoʳ = Eq.refl X , (Eq.refl Y , Eq.refl Z)
}
}
Posets-Monoidal : Monoidal (Posets c ℓ₁ ℓ₂)
Posets-Monoidal = record
{ ⊗ = ⊗
; unit = unit
; unitorˡ = unitorˡ
; unitorʳ = unitorʳ
; associator = associator
; unitorˡ-commute-from = λ {_ X} → Eq.refl X
; unitorˡ-commute-to = λ {_ Y} → tt , Eq.refl Y
; unitorʳ-commute-from = λ {_ X} → Eq.refl X
; unitorʳ-commute-to = λ {_ Y} → Eq.refl Y , tt
; assoc-commute-from = λ {_ A _ _ B _ _ C} → Eq.refl A , Eq.refl B , Eq.refl C
; assoc-commute-to = λ {_ A _ _ B _ _ C} → (Eq.refl A , Eq.refl B) , Eq.refl C
; triangle = λ {X Y} → Eq.refl X , Eq.refl Y
; pentagon = λ {W X Y Z} → Eq.refl W , Eq.refl X , Eq.refl Y , Eq.refl Z
}
|
