/
freyd.agda
144 lines (131 loc) · 6.12 KB
/
freyd.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
131
132
133
134
135
136
137
138
139
140
141
142
open import Category -- https://github.com/konn/category-agda
open import Level
module freyd where
open import cat-utility
open import HomReasoning
open import Relation.Binary.Core
open Functor
-- C is small full subcategory of A ( C is image of F )
-- but we don't use smallness in this proof
record FullSubcategory {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
: Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
field
FSF : Functor A A
FSFMap← : { a b : Obj A } → Hom A (FObj FSF a) (FObj FSF b ) → Hom A a b
full→ : { a b : Obj A } { x : Hom A (FObj FSF a) (FObj FSF b) } → A [ FMap FSF ( FSFMap← x ) ≈ x ]
full← : { a b : Obj A } { x : Hom A (FObj FSF a) (FObj FSF b) } → A [ FSFMap← ( FMap FSF x ) ≈ x ]
-- pre-initial
record PreInitial {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
(F : Functor A A) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
field
preinitialObj : Obj A
preinitialArrow : ∀{a : Obj A } → Hom A ( FObj F preinitialObj ) a
-- initial object
-- now in cat-utility
-- record HasInitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (i : Obj A) : Set (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
-- field
-- initial : ∀( a : Obj A ) → Hom A i a
-- uniqueness : { a : Obj A } → ( f : Hom A i a ) → A [ f ≈ initial a ]
-- A complete catagory has initial object if it has PreInitial-FullSubcategory
open NTrans
open Limit
open IsLimit
open FullSubcategory
open PreInitial
open Complete
open Equalizer
open IsEqualizer
initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
(comp : Complete A A)
(SFS : FullSubcategory A ) →
(PI : PreInitial A (FSF SFS )) → HasInitialObject A (limit-c comp (FSF SFS))
initialFromPreInitialFullSubcategory A comp SFS PI = record {
initial = initialArrow ;
uniqueness = λ {a} f → lemma1 a f
} where
F : Functor A A
F = FSF SFS
FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b
FMap← = FSFMap← SFS
a00 : Obj A
a00 = limit-c comp F
lim : ( Γ : Functor A A ) → Limit A A Γ
lim Γ = climit comp Γ
u : NTrans A A (K A A a00) F
u = t0 ( lim F )
equ : {a b : Obj A} → (f g : Hom A a b) → IsEqualizer A (equalizer-e comp f g ) f g
equ f g = isEqualizer ( Complete.cequalizer comp f g )
ep : {a b : Obj A} → {f g : Hom A a b} → Obj A
ep {a} {b} {f} {g} = equalizer-p comp f g
ee : {a b : Obj A} → {f g : Hom A a b} → Hom A (ep {a} {b} {f} {g} ) a
ee {a} {b} {f} {g} = equalizer-e comp f g
f : Hom A a00 (FObj F (preinitialObj PI ) )
f = TMap u (preinitialObj PI )
initialArrow : ∀( a : Obj A ) → Hom A a00 a
initialArrow a = A [ preinitialArrow PI {a} o f ]
equ-fi : { a : Obj A} → {f' : Hom A a00 a} →
IsEqualizer A ee ( A [ preinitialArrow PI {a} o f ] ) f'
equ-fi {a} {f'} = equ ( A [ preinitialArrow PI {a} o f ] ) f'
e=id : {e : Hom A a00 a00} → ( {c : Obj A} → A [ A [ TMap u c o e ] ≈ TMap u c ] ) → A [ e ≈ id1 A a00 ]
e=id {e} uce=uc = let open ≈-Reasoning (A) in
begin
e
≈↑⟨ limit-uniqueness (isLimit (lim F)) ( λ {i} → uce=uc ) ⟩
limit (isLimit (lim F)) a00 u
≈⟨ limit-uniqueness (isLimit (lim F)) ( λ {i} → idR ) ⟩
id1 A a00
∎
kfuc=uc : {c k1 : Obj A} → {p : Hom A k1 a00} → A [ A [ TMap u c o
A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ]
≈ TMap u c ]
kfuc=uc {c} {k1} {p} = let open ≈-Reasoning (A) in
begin
TMap u c o ( p o ( preinitialArrow PI {k1} o TMap u (preinitialObj PI) ))
≈⟨ cdr assoc ⟩
TMap u c o ((p o preinitialArrow PI) o TMap u (preinitialObj PI))
≈⟨ assoc ⟩
(TMap u c o ( p o ( preinitialArrow PI {k1} ))) o TMap u (preinitialObj PI)
≈↑⟨ car ( full→ SFS ) ⟩
FMap F (FMap← (TMap u c o p o preinitialArrow PI)) o TMap u (preinitialObj PI)
≈⟨ nat u ⟩
TMap u c o FMap (K A A a00) (FMap← (TMap u c o p o preinitialArrow PI))
≈⟨⟩
TMap u c o id1 A a00
≈⟨ idR ⟩
TMap u c
∎
kfuc=1 : {k1 : Obj A} → {p : Hom A k1 a00} → A [ A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ≈ id1 A a00 ]
kfuc=1 {k1} {p} = e=id ( kfuc=uc )
-- if equalizer has right inverse, f = g
lemma2 : (a b : Obj A) {c : Obj A} ( f g : Hom A a b )
{e : Hom A c a } {e' : Hom A a c } ( equ : IsEqualizer A e f g ) (inv-e : A [ A [ e o e' ] ≈ id1 A a ] )
→ A [ f ≈ g ]
lemma2 a b {c} f g {e} {e'} equ inv-e = let open ≈-Reasoning (A) in
let open Equalizer in
begin
f
≈↑⟨ idR ⟩
f o id1 A a
≈↑⟨ cdr inv-e ⟩
f o ( e o e' )
≈⟨ assoc ⟩
( f o e ) o e'
≈⟨ car ( fe=ge equ ) ⟩ ( g o e ) o e'
≈↑⟨ assoc ⟩
g o ( e o e' )
≈⟨ cdr inv-e ⟩
g o id1 A a
≈⟨ idR ⟩
g
∎
lemma1 : (a : Obj A) (f' : Hom A a00 a) → A [ f' ≈ initialArrow a ]
lemma1 a f' = let open ≈-Reasoning (A) in
sym (
begin
initialArrow a
≈⟨⟩
preinitialArrow PI {a} o f
≈⟨ lemma2 a00 a (A [ preinitialArrow PI {a} o f ]) f' {ee {a00} {a} {A [ preinitialArrow PI {a} o f ]} {f'} } (equ-fi )
(kfuc=1 {ep} {ee} ) ⟩
f'
∎ )