-
Notifications
You must be signed in to change notification settings - Fork 1
/
Universality.agda
130 lines (99 loc) · 4.68 KB
/
Universality.agda
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
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
-- vim: nowrap
open import Order.Instances.Discrete
open import Order.Instances.Coproduct
open import Cat.Prelude
open import Cat.Functor.Base
open import Cat.Functor.Compose
open import Cat.Functor.Properties
open import Cat.Diagram.Monad
import Cat.Reasoning as Cat
import Cat.Functor.Reasoning as FR
open import Mugen.Prelude
open import Mugen.Algebra.Displacement
open import Mugen.Algebra.Displacement.Instances.Endomorphism
open import Mugen.Cat.Instances.Endomorphisms
open import Mugen.Cat.Instances.Indexed
open import Mugen.Cat.Instances.StrictOrders
open import Mugen.Cat.Monad
open import Mugen.Cat.HierarchyTheory
open import Mugen.Cat.HierarchyTheory.McBride
import Mugen.Order.Reasoning as Reasoning
--------------------------------------------------------------------------------
-- The Universal Embedding Theorem
-- Section 3.4, Theorem 3.10
module Mugen.Cat.HierarchyTheory.Universality {o o' r}
(H : Hierarchy-theory (o ⊔ o') (r ⊔ o')) {I : Type o'} ⦃ Discrete-I : Discrete I ⦄
(Δ₋ : ⌞ I ⌟ → Poset (o ⊔ o') (r ⊔ o')) (Ψ : Set (lsuc (o ⊔ r ⊔ o'))) where
private
import Mugen.Cat.HierarchyTheory.Universality.SubcategoryEmbedding as SubcategoryEmbedding
module SE = SubcategoryEmbedding {o = o} {r = r} H Δ₋
import Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding as EndomorphismEmbedding
module EE = EndomorphismEmbedding H SE.Δ Ψ
import Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality as EndomorphismEmbeddingNaturality
module EEN = EndomorphismEmbeddingNaturality H SE.Δ Ψ
--------------------------------------------------------------------------------
-- Notation
private
open Algebra-hom
module H = Monad H
SOrd : Precategory (lsuc (o ⊔ r ⊔ o')) (o ⊔ r ⊔ o')
SOrd = Strict-orders (o ⊔ o') (r ⊔ o')
open Cat SOrd
SOrdᴴ : Precategory (lsuc (o ⊔ r ⊔ o')) (lsuc (o ⊔ r ⊔ o'))
SOrdᴴ = Eilenberg-Moore SOrd H
module SOrdᴴ = Cat SOrdᴴ
-- '↑' for lifting
SOrd↑ : Precategory (lsuc (lsuc (o ⊔ r ⊔ o'))) (lsuc (o ⊔ r ⊔ o'))
SOrd↑ = Strict-orders (lsuc (o ⊔ r ⊔ o')) (lsuc (o ⊔ r ⊔ o'))
module SOrd↑ = Cat SOrd↑
SOrdᴹᴰ : Precategory (lsuc (lsuc (o ⊔ r ⊔ o'))) (lsuc (lsuc (o ⊔ r ⊔ o')))
SOrdᴹᴰ = Eilenberg-Moore SOrd↑ (McBride (Endomorphism H EE.Δ⁺))
module SOrdᴹᴰ = Cat SOrdᴹᴰ
Uᴴ : Functor SOrdᴴ SOrd
Uᴴ = Forget SOrd H
Fᴴ : Functor SOrd SOrdᴴ
Fᴴ = Free SOrd H
Fᴴ₀ : Poset (o ⊔ o') (r ⊔ o') → Algebra SOrd H
Fᴴ₀ = Fᴴ .Functor.F₀
Fᴴ₁ : {X Y : Poset (o ⊔ o') (r ⊔ o')} → Hom X Y → SOrdᴴ.Hom (Fᴴ₀ X) (Fᴴ₀ Y)
Fᴴ₁ = Fᴴ .Functor.F₁
Fᴹᴰ : Functor SOrd↑ SOrdᴹᴰ
Fᴹᴰ = Free SOrd↑ (McBride (Endomorphism H EE.Δ⁺))
Fᴹᴰ₀ : Poset (lsuc (o ⊔ r ⊔ o')) (lsuc (o ⊔ r ⊔ o')) → Algebra SOrd↑ (McBride (Endomorphism H EE.Δ⁺))
Fᴹᴰ₀ = Fᴹᴰ .Functor.F₀
Uᴹᴰ : Functor SOrdᴹᴰ SOrd↑
Uᴹᴰ = Forget SOrd↑ (McBride (Endomorphism H EE.Δ⁺))
--------------------------------------------------------------------------------
-- Constructing the natural transformation T
-- Section 3.4, Theorem 3.10
T : Functor (Indexed SOrdᴴ λ i → Fᴴ₀ (Δ₋ i)) (Endos SOrdᴹᴰ (Fᴹᴰ₀ (Disc Ψ)))
T = EE.T F∘ SE.T
--------------------------------------------------------------------------------
-- Constructing the natural transformation ν
-- Section 3.4, Theorem 3.10
ν : ∣ Ψ ∣
→ liftᶠ-strict-orders F∘ Uᴴ F∘ Indexed-include
=> Uᴹᴰ F∘ Endos-include F∘ T
ν pt = lemma-assoc₂
∘nt (EEN.ν pt ◂ SE.T)
∘nt lemma-assoc₁
∘nt (liftᶠ-strict-orders ▸ (Uᴴ ▸ SE.ν))
where
lemma-assoc₁
: liftᶠ-strict-orders F∘ Uᴴ F∘ Endos-include F∘ SE.T
=> (liftᶠ-strict-orders F∘ Uᴴ F∘ Endos-include) F∘ SE.T
lemma-assoc₁ ._=>_.η _ = SOrd↑.id
lemma-assoc₁ ._=>_.is-natural _ _ _ = SOrd↑.id-comm-sym
lemma-assoc₂
: (Uᴹᴰ F∘ Endos-include F∘ EE.T) F∘ SE.T
=> Uᴹᴰ F∘ Endos-include F∘ EE.T F∘ SE.T
lemma-assoc₂ ._=>_.η _ = SOrd↑.id
lemma-assoc₂ ._=>_.is-natural _ _ _ = SOrd↑.id-comm-sym
--------------------------------------------------------------------------------
-- Faithfulness of T
-- Section 3.4, Lemma 3.9
abstract
T-faithful : ∣ Ψ ∣ → preserves-monos H → is-faithful T
T-faithful pt H-preserves-monos eq =
SE.T-faithful H-preserves-monos $
EE.T-faithful pt H-preserves-monos eq