Mercurial > hg > Members > kono > Proof > category
annotate pullback.agda @ 272:5f2b8a5cc115
adjunction to limit
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 22 Sep 2013 21:27:03 +0900 |
parents | 28278175d696 |
children | fae4bb967d76 |
rev | line source |
---|---|
260 | 1 -- Pullback from product and equalizer |
2 -- | |
3 -- | |
4 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> | |
5 ---- | |
6 | |
7 open import Category -- https://github.com/konn/category-agda | |
8 open import Level | |
266 | 9 module pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ') ( Γ : Functor I A ) where |
260 | 10 |
11 open import HomReasoning | |
12 open import cat-utility | |
13 | |
14 -- | |
264 | 15 -- Pullback from equalizer and product |
260 | 16 -- f |
17 -- a -------> c | |
18 -- ^ ^ | |
19 -- π1 | |g | |
20 -- | | | |
21 -- ab -------> b | |
22 -- ^ π2 | |
23 -- | | |
264 | 24 -- | e = equalizer (f π1) (g π1) |
25 -- | | |
26 -- d <------------------ d' | |
27 -- k (π1' × π2' ) | |
260 | 28 |
261 | 29 open Equalizer |
30 open Product | |
31 open Pullback | |
32 | |
33 pullback-from : (a b c ab d : Obj A) | |
260 | 34 ( f : Hom A a c ) ( g : Hom A b c ) |
261 | 35 ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( e : Hom A d ab ) |
260 | 36 ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g ) |
261 | 37 ( prod : Product A a b ab π1 π2 ) → Pullback A a b c d f g |
38 ( A [ π1 o equalizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ){e} ) ] ) | |
39 ( A [ π2 o equalizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ){e} ) ] ) | |
40 pullback-from a b c ab d f g π1 π2 e eqa prod = record { | |
260 | 41 commute = commute1 ; |
42 p = p1 ; | |
261 | 43 π1p=π1 = λ {d} {π1'} {π2'} {eq} → π1p=π11 {d} {π1'} {π2'} {eq} ; |
44 π2p=π2 = λ {d} {π1'} {π2'} {eq} → π2p=π21 {d} {π1'} {π2'} {eq} ; | |
260 | 45 uniqueness = uniqueness1 |
46 } where | |
261 | 47 commute1 : A [ A [ f o A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ≈ A [ g o A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ] |
262 | 48 commute1 = let open ≈-Reasoning (A) in |
49 begin | |
50 f o ( π1 o equalizer (eqa ( f o π1 ) ( g o π2 )) ) | |
51 ≈⟨ assoc ⟩ | |
52 ( f o π1 ) o equalizer (eqa ( f o π1 ) ( g o π2 )) | |
53 ≈⟨ fe=ge (eqa (A [ f o π1 ]) (A [ g o π2 ])) ⟩ | |
54 ( g o π2 ) o equalizer (eqa ( f o π1 ) ( g o π2 )) | |
55 ≈↑⟨ assoc ⟩ | |
56 g o ( π2 o equalizer (eqa ( f o π1 ) ( g o π2 )) ) | |
57 ∎ | |
58 lemma1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → | |
59 A [ A [ A [ f o π1 ] o (prod × π1') π2' ] ≈ A [ A [ g o π2 ] o (prod × π1') π2' ] ] | |
60 lemma1 {d'} { π1' } { π2' } eq = let open ≈-Reasoning (A) in | |
61 begin | |
62 ( f o π1 ) o (prod × π1') π2' | |
63 ≈↑⟨ assoc ⟩ | |
64 f o ( π1 o (prod × π1') π2' ) | |
65 ≈⟨ cdr (π1fxg=f prod) ⟩ | |
66 f o π1' | |
67 ≈⟨ eq ⟩ | |
68 g o π2' | |
69 ≈↑⟨ cdr (π2fxg=g prod) ⟩ | |
70 g o ( π2 o (prod × π1') π2' ) | |
71 ≈⟨ assoc ⟩ | |
72 ( g o π2 ) o (prod × π1') π2' | |
73 ∎ | |
261 | 74 p1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → Hom A d' d |
262 | 75 p1 {d'} { π1' } { π2' } eq = |
76 let open ≈-Reasoning (A) in k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) ( lemma1 eq ) | |
77 π1p=π11 : {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → | |
78 A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π1' ] | |
79 π1p=π11 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in | |
80 begin | |
81 ( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq | |
82 ≈⟨⟩ | |
83 ( π1 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) | |
84 ≈↑⟨ assoc ⟩ | |
85 π1 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) ) | |
86 ≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩ | |
87 π1 o (_×_ prod π1' π2' ) | |
88 ≈⟨ π1fxg=f prod ⟩ | |
89 π1' | |
90 ∎ | |
263 | 91 π2p=π21 : {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → |
92 A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π2' ] | |
262 | 93 π2p=π21 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in |
94 begin | |
95 ( π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq | |
96 ≈⟨⟩ | |
97 ( π2 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) | |
98 ≈↑⟨ assoc ⟩ | |
99 π2 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) ) | |
100 ≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩ | |
101 π2 o (_×_ prod π1' π2' ) | |
102 ≈⟨ π2fxg=g prod ⟩ | |
103 π2' | |
104 ∎ | |
261 | 105 uniqueness1 : {d₁ : Obj A} (p' : Hom A d₁ d) {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → |
106 {eq1 : A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} → | |
107 {eq2 : A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]} → | |
108 A [ p1 eq ≈ p' ] | |
264 | 109 uniqueness1 {d'} p' {π1'} {π2'} {eq} {eq1} {eq2} = let open ≈-Reasoning (A) in |
263 | 110 begin |
111 p1 eq | |
112 ≈⟨⟩ | |
113 k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) | |
264 | 114 ≈⟨ Equalizer.uniqueness (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e}) ( begin |
115 e o p' | |
116 ≈⟨⟩ | |
117 equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p' | |
118 ≈↑⟨ Product.uniqueness prod ⟩ | |
119 (prod × ( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p') ) ( π2 o (equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p')) | |
120 ≈⟨ ×-cong prod (assoc) (assoc) ⟩ | |
121 (prod × (A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ])) | |
122 (A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]) | |
123 ≈⟨ ×-cong prod eq1 eq2 ⟩ | |
124 ((prod × π1') π2') | |
125 ∎ ) ⟩ | |
263 | 126 p' |
127 ∎ | |
128 | |
266 | 129 ------ |
130 -- | |
131 -- Limit | |
132 -- | |
133 ----- | |
134 | |
135 -- Constancy Functor | |
136 | |
137 K : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) → ( a : Obj A ) → Functor I A | |
138 K I a = record { | |
265 | 139 FObj = λ i → a ; |
140 FMap = λ f → id1 A a ; | |
141 isFunctor = let open ≈-Reasoning (A) in record { | |
142 ≈-cong = λ f=g → refl-hom | |
143 ; identity = refl-hom | |
144 ; distr = sym idL | |
145 } | |
146 } | |
147 | |
148 open NTrans | |
149 | |
150 record Limit { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) | |
266 | 151 ( a0 : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where |
265 | 152 field |
266 | 153 limit : ( a : Obj A ) → ( t : NTrans I A ( K I a ) Γ ) → Hom A a a0 |
154 t0f=t : { a : Obj A } → { t : NTrans I A ( K I a ) Γ } → ∀ { i : Obj I } → | |
265 | 155 A [ A [ TMap t0 i o limit a t ] ≈ TMap t i ] |
271 | 156 limit-uniqueness : { a : Obj A } → { t : NTrans I A ( K I a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } → |
157 A [ A [ TMap t0 i o f ] ≈ TMap t i ] ) → A [ limit a t ≈ f ] | |
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
158 A0 : Obj A |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
159 A0 = a0 |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
160 T0 : NTrans I A ( K I a0 ) Γ |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
161 T0 = t0 |
265 | 162 |
266 | 163 -------------------------------- |
164 -- | |
165 -- If we have two limits on c and c', there are isomorphic pair h, h' | |
166 | |
167 open Limit | |
168 | |
169 iso-l : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) | |
170 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) ( t0' : NTrans I A ( K I a0' ) Γ ) | |
171 ( lim : Limit I Γ a0 t0 ) → ( lim' : Limit I Γ a0' t0' ) | |
172 → Hom A a0 a0' | |
173 iso-l I Γ a0 a0' t0 t0' lim lim' = limit lim' a0 t0 | |
174 | |
175 iso-r : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) | |
176 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) ( t0' : NTrans I A ( K I a0' ) Γ ) | |
177 ( lim : Limit I Γ a0 t0 ) → ( lim' : Limit I Γ a0' t0' ) | |
178 → Hom A a0' a0 | |
179 iso-r I Γ a0 a0' t0 t0' lim lim' = limit lim a0' t0' | |
180 | |
181 | |
182 iso-lr : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) | |
183 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) ( t0' : NTrans I A ( K I a0' ) Γ ) | |
184 ( lim : Limit I Γ a0 t0 ) → ( lim' : Limit I Γ a0' t0' ) → ∀{ i : Obj I } → | |
185 A [ A [ iso-l I Γ a0 a0' t0 t0' lim lim' o iso-r I Γ a0 a0' t0 t0' lim lim' ] ≈ id1 A a0' ] | |
186 iso-lr I Γ a0 a0' t0 t0' lim lim' {i} = let open ≈-Reasoning (A) in begin | |
187 limit lim' a0 t0 o limit lim a0' t0' | |
271 | 188 ≈↑⟨ limit-uniqueness lim' ( λ {i} → ( begin |
266 | 189 TMap t0' i o ( limit lim' a0 t0 o limit lim a0' t0' ) |
190 ≈⟨ assoc ⟩ | |
191 ( TMap t0' i o limit lim' a0 t0 ) o limit lim a0' t0' | |
192 ≈⟨ car ( t0f=t lim' ) ⟩ | |
193 TMap t0 i o limit lim a0' t0' | |
194 ≈⟨ t0f=t lim ⟩ | |
195 TMap t0' i | |
271 | 196 ∎) ) ⟩ |
266 | 197 limit lim' a0' t0' |
271 | 198 ≈⟨ limit-uniqueness lim' idR ⟩ |
266 | 199 id a0' |
200 ∎ | |
201 | |
202 | |
267 | 203 open import CatExponetial |
204 | |
205 open Functor | |
206 | |
207 -------------------------------- | |
208 -- | |
209 -- Contancy Functor | |
266 | 210 |
268 | 211 KI : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) → Functor A ( A ^ I ) |
212 KI { c₁'} {c₂'} {ℓ'} I = record { | |
267 | 213 FObj = λ a → K I a ; |
214 FMap = λ f → record { -- NTrans I A (K I a) (K I b) | |
215 TMap = λ a → f ; | |
216 isNTrans = record { | |
217 commute = λ {a b f₁} → commute1 {a} {b} {f₁} f | |
218 } | |
219 } ; | |
266 | 220 isFunctor = let open ≈-Reasoning (A) in record { |
267 | 221 ≈-cong = λ f=g {x} → f=g |
266 | 222 ; identity = refl-hom |
267 | 223 ; distr = refl-hom |
266 | 224 } |
267 | 225 } where |
226 commute1 : {a b : Obj I} {f₁ : Hom I a b} → {a' b' : Obj A} → (f : Hom A a' b' ) → | |
227 A [ A [ FMap (K I b') f₁ o f ] ≈ A [ f o FMap (K I a') f₁ ] ] | |
228 commute1 {a} {b} {f₁} {a'} {b'} f = let open ≈-Reasoning (A) in begin | |
229 FMap (K I b') f₁ o f | |
230 ≈⟨ idL ⟩ | |
231 f | |
232 ≈↑⟨ idR ⟩ | |
233 f o FMap (K I a') f₁ | |
234 ∎ | |
235 | |
236 | |
268 | 237 open import Function |
267 | 238 |
272 | 239 --------- |
240 -- | |
241 -- limit gives co universal mapping ( i.e. adjunction ) | |
242 -- | |
243 -- F = KI I : Functor A (A ^ I) | |
244 -- U = λ b → A0 (lim b {a0 b} {t0 b} | |
245 -- ε = λ b → T0 ( lim b {a0 b} {t0 b} ) | |
246 | |
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
247 limit2adjoint : |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
248 ( lim : ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K I a0 ) Γ } → Limit I Γ a0 t0 ) |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
249 → ( a0 : ( b : Functor I A ) → Obj A ) ( t0 : ( b : Functor I A ) → NTrans I A ( K I (a0 b) ) b ) |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
250 → coUniversalMapping A ( A ^ I ) (KI I) (λ b → A0 (lim b {a0 b} {t0 b} ) ) ( λ b → T0 ( lim b {a0 b} {t0 b} ) ) |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
251 limit2adjoint lim a0 t0 = record { |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
252 _*' = λ {b} {a} k → limit (lim b {a0 b} {t0 b} ) a k ; |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
253 iscoUniversalMapping = record { |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
254 couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ; |
271 | 255 couniquness = couniquness2 |
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
256 } |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
257 } where |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
258 couniversalMapping1 : {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} → |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
259 A ^ I [ A ^ I [ T0 (lim b {a0 b} {t0 b}) o FMap (KI I) (limit (lim b {a0 b} {t0 b}) a f) ] ≈ f ] |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
260 couniversalMapping1 {b} {a} {f} {i} = let open ≈-Reasoning (A) in begin |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
261 TMap (T0 (lim b {a0 b} {t0 b})) i o TMap ( FMap (KI I) (limit (lim b {a0 b} {t0 b}) a f) ) i |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
262 ≈⟨⟩ |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
263 TMap (t0 b) i o (limit (lim b) a f) |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
264 ≈⟨ t0f=t (lim b) ⟩ |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
265 TMap f i -- i comes from ∀{i} → B [ TMap f i ≈ TMap g i ] |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
266 ∎ |
271 | 267 couniquness2 : {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} {g : Hom A a (A0 (lim b {a0 b} {t0 b} ))} → |
272 | 268 ( ∀ { i : Obj I } → A [ A [ TMap (T0 (lim b {a0 b} {t0 b} )) i o TMap ( FMap (KI I) g) i ] ≈ TMap f i ] ) |
269 → A [ limit (lim b {a0 b} {t0 b} ) a f ≈ g ] | |
271 | 270 couniquness2 {b} {a} {f} {g} lim-g=f = let open ≈-Reasoning (A) in begin |
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
271 limit (lim b {a0 b} {t0 b} ) a f |
271 | 272 ≈⟨ limit-uniqueness ( lim b {a0 b} {t0 b} ) lim-g=f ⟩ |
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
273 g |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
274 ∎ |
268 | 275 |
272 | 276 open import Category.Cat |
277 | |
278 adjoint2limit : | |
279 ( U : Functor (A ^ I) A ) ( η : NTrans A A identityFunctor ( U ○ (KI I) ) ) | |
280 ( ε : NTrans (A ^ I) (A ^ I) ( (KI I) ○ U ) identityFunctor ) | |
281 ( adj : Adjunction A (A ^ I) U (KI I) η ε ) → | |
282 ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K I a0 ) Γ } → Limit I Γ a0 t0 | |
283 adjoint2limit U η ε adj Γ {a0} {t0} = record { | |
284 limit = λ a t → limit1 a t ; | |
285 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ; | |
286 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f | |
287 } where | |
288 limit1 : ( a : Obj A ) → ( t : NTrans I A ( K I a ) Γ ) → Hom A a a0 | |
289 limit1 a t = {!!} | |
290 t0f=t1 : { a : Obj A } → { t : NTrans I A ( K I a ) Γ } → ∀ { i : Obj I } → | |
291 A [ A [ TMap t0 i o limit1 a t ] ≈ TMap t i ] | |
292 t0f=t1 = {!!} | |
293 limit-uniqueness1 : { a : Obj A } → { t : NTrans I A ( K I a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } → | |
294 A [ A [ TMap t0 i o f ] ≈ TMap t i ] ) → A [ limit1 a t ≈ f ] | |
295 limit-uniqueness1 = {!!} | |
269 | 296 |
271 | 297 |
272 | 298 |