Mercurial > hg > Members > kono > Proof > category

comparison equalizer.agda @ 253:24e83b8b81be

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 11 Sep 2013 20:26:48 +0900
parents e0835b8dd51b
children 45b81fcb8a64
comparison
equal deleted inserted replaced
252:e0835b8dd51b 253:24e83b8b81be
27 ek=h : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ e o k {d} h eq ] ≈ h ] 27 ek=h : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ e o k {d} h eq ] ≈ h ]
28 uniqueness : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → 28 uniqueness : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } →
29 A [ A [ e o k' ] ≈ h ] → A [ k {d} h eq ≈ k' ] 29 A [ A [ e o k' ] ≈ h ] → A [ k {d} h eq ≈ k' ]
30 equalizer : Hom A c a 30 equalizer : Hom A c a
31 equalizer = e 31 equalizer = e
32
32 33
33 -- 34 --
34 -- Burroni's Flat Equational Definition of Equalizer 35 -- Burroni's Flat Equational Definition of Equalizer
35 -- 36 --
36 record Burroni { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (f g : Hom A a b) (e : Hom A c a) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where 37 record Burroni { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (f g : Hom A a b) (e : Hom A c a) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
114 ≈↑⟨ assoc ⟩ 115 ≈↑⟨ assoc ⟩
115 e o ( h-1 o ( h o k eqa j eq ) ) 116 e o ( h-1 o ( h o k eqa j eq ) )
116 ≈⟨ cdr assoc ⟩ 117 ≈⟨ cdr assoc ⟩
117 e o (( h-1 o h) o k eqa j eq ) 118 e o (( h-1 o h) o k eqa j eq )
118 ≈⟨ cdr (car h-1h=1 ) ⟩ 119 ≈⟨ cdr (car h-1h=1 ) ⟩
119 e o (id1 A c o k eqa j eq ) 120 e o (id c o k eqa j eq )
120 ≈⟨ cdr idL ⟩ 121 ≈⟨ cdr idL ⟩
121 e o k eqa j eq 122 e o k eqa j eq
122 ≈⟨ ek=h eqa ⟩ 123 ≈⟨ ek=h eqa ⟩
123 j 124 j
124 ∎ 125 ∎
137 ∎ )) ⟩ 138 ∎ )) ⟩
138 h o ( h-1 o j ) 139 h o ( h-1 o j )
139 ≈⟨ assoc ⟩ 140 ≈⟨ assoc ⟩
140 (h o h-1 ) o j 141 (h o h-1 ) o j
141 ≈⟨ car hh-1=1 ⟩ 142 ≈⟨ car hh-1=1 ⟩
142 id1 A c' o j 143 id c' o j
143 ≈⟨ idL ⟩ 144 ≈⟨ idL ⟩
144 j 145 j
145 ∎ 146 ∎
146 147
147 -------------------------------- 148 --------------------------------
192 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) ) 193 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) )
193 → A [ A [ e o c-iso-r eqa eqa' keqa ] ≈ e' ] 194 → A [ A [ e o c-iso-r eqa eqa' keqa ] ≈ e' ]
194 e'←e {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa = let open ≈-Reasoning (A) in begin 195 e'←e {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa = let open ≈-Reasoning (A) in begin
195 e o c-iso-r eqa eqa' keqa 196 e o c-iso-r eqa eqa' keqa
196 ≈⟨⟩ 197 ≈⟨⟩
197 e o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) 198 e o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') )
198 ≈↑⟨ car (ek=h eqa' ) ⟩ 199 ≈↑⟨ car (ek=h eqa' ) ⟩
199 ( equalizer eqa' o k eqa' e (fe=ge eqa) ) o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) 200 ( equalizer eqa' o k eqa' e (fe=ge eqa) ) o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') )
200 ≈⟨⟩ 201 ≈⟨⟩
201 ( e' o k eqa' e (fe=ge eqa) ) o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) 202 ( e' o k eqa' e (fe=ge eqa) ) o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') )
202 ≈↑⟨ assoc ⟩ 203 ≈↑⟨ assoc ⟩
203 e' o (( k eqa' e (fe=ge eqa) ) o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) ) 204 e' o (( k eqa' e (fe=ge eqa) ) o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) )
204 ≈⟨⟩ 205 ≈⟨⟩
205 e' o (equalizer keqa o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) ) 206 e' o (equalizer keqa o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) )
206 ≈⟨ cdr ( ek=h keqa ) ⟩ 207 ≈⟨ cdr ( ek=h keqa ) ⟩
207 e' o id1 A c' 208 e' o id c'
208 ≈⟨ idR ⟩ 209 ≈⟨ idR ⟩
209 e' 210 e'
210 ∎ 211 ∎
211 212
212 -- e←e' e'←e = e 213 -- e←e' e'←e e = e
213 -- e'←e e←e = e' is enough for isomorphism but we want to prove l o r = id also. 214 -- e'←e e←e e' = e' is enough for isomorphism but we can prove l o r = id also.
214 215
215 c-iso→ : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g ) 216 c-iso→ : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g )
216 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) ) 217 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) )
217 → A [ A [ c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa ] ≈ id1 A c' ] 218 → A [ A [ c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa ] ≈ id1 A c' ]
218 c-iso→ {c} {c'} {a} {b} {f} {g} eqa eqa' keqa = let open ≈-Reasoning (A) in begin 219 c-iso→ {c} {c'} {a} {b} {f} {g} eqa eqa' keqa = let open ≈-Reasoning (A) in begin
219 c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa 220 c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa
220 ≈⟨⟩ 221 ≈⟨⟩
221 equalizer keqa o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) 222 equalizer keqa o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') )
222 ≈⟨ ek=h keqa ⟩ 223 ≈⟨ ek=h keqa ⟩
223 id1 A c' 224 id c'
224 ∎ 225 ∎
225 226
226 c-iso← : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g ) 227 c-iso← : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g )
227 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa )) (A [ f o e' ]) (A [ g o e' ]) ) 228 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa )) (A [ f o e' ]) (A [ g o e' ]) )
228 → ( keqa' : Equalizer A (k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )) (A [ f o e ]) (A [ g o e ]) ) 229 → ( keqa' : Equalizer A (k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )) (A [ f o e ]) (A [ g o e ]) )
229 → A [ A [ c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa ] ≈ id1 A c ] 230 → A [ A [ c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa ] ≈ id1 A c ]
230 c-iso← {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa keqa' = let open ≈-Reasoning (A) in begin 231 c-iso← {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa keqa' = let open ≈-Reasoning (A) in begin
231 c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa 232 c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa
232 ≈⟨⟩ 233 ≈⟨⟩
233 k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) o k eqa' e (fe=ge eqa ) 234 k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) o k eqa' e (fe=ge eqa )
234 ≈⟨⟩ 235 ≈⟨⟩
235 equalizer keqa' o k eqa' e (fe=ge eqa ) 236 equalizer keqa' o k eqa' e (fe=ge eqa )
236 ≈⟨ cdr ( begin 237 ≈⟨ cdr ( begin
237 k eqa' e (fe=ge eqa ) 238 k eqa' e (fe=ge eqa )
238 ≈⟨ uniqueness eqa' ( begin 239 ≈⟨ uniqueness eqa' ( begin
239 e' o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c)) 240 e' o k keqa' (id c) (f1=g1 (fe=ge eqa) (id c))
240 ≈↑⟨ car (e'←e eqa eqa' keqa ) ⟩ 241 ≈↑⟨ car (e'←e eqa eqa' keqa ) ⟩
241 ( e o equalizer keqa' ) o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c)) 242 ( e o equalizer keqa' ) o k keqa' (id c) (f1=g1 (fe=ge eqa) (id c))
242 ≈↑⟨ assoc ⟩ 243 ≈↑⟨ assoc ⟩
243 e o ( equalizer keqa' o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c))) 244 e o ( equalizer keqa' o k keqa' (id c) (f1=g1 (fe=ge eqa) (id c)))
244 ≈⟨ cdr ( ek=h keqa' ) ⟩ 245 ≈⟨ cdr ( ek=h keqa' ) ⟩
245 e o id1 A c 246 e o id c
246 ≈⟨ idR ⟩ 247 ≈⟨ idR ⟩
247 e 248 e
248 ∎ )⟩ 249 ∎ )⟩
249 k keqa' (id1 A c) ( f1=g1 (fe=ge eqa) (id1 A c) ) 250 k keqa' (id c) ( f1=g1 (fe=ge eqa) (id c) )
250 ∎ )⟩ 251 ∎ )⟩
251 equalizer keqa' o k keqa' (id1 A c) ( f1=g1 (fe=ge eqa) (id1 A c) ) ≈⟨ ek=h keqa' ⟩ 252 equalizer keqa' o k keqa' (id c) ( f1=g1 (fe=ge eqa) (id c) ) ≈⟨ ek=h keqa' ⟩
252 id1 A c 253 id c
253 ∎ 254 ∎
254 255
255 256
256 257
257 -------------------------------- 258 --------------------------------
290 -- e o id1 ≈ e → k e ≈ id 291 -- e o id1 ≈ e → k e ≈ id
291 292
292 lemma-b3 : {a b d : Obj A} (f : Hom A a b ) { h : Hom A d a } → A [ A [ equalizer (eqa f f ) o k (eqa f f) (id1 A a) (f1=f1 f) ] ≈ id1 A a ] 293 lemma-b3 : {a b d : Obj A} (f : Hom A a b ) { h : Hom A d a } → A [ A [ equalizer (eqa f f ) o k (eqa f f) (id1 A a) (f1=f1 f) ] ≈ id1 A a ]
293 lemma-b3 {a} {b} {d} f {h} = let open ≈-Reasoning (A) in 294 lemma-b3 {a} {b} {d} f {h} = let open ≈-Reasoning (A) in
294 begin 295 begin
295 equalizer (eqa f f) o k (eqa f f) (id1 A a) (f1=f1 f) 296 equalizer (eqa f f) o k (eqa f f) (id a) (f1=f1 f)
296 ≈⟨ ek=h (eqa f f ) ⟩ 297 ≈⟨ ek=h (eqa f f ) ⟩
297 id1 A a 298 id a
298 ∎ 299 ∎
299 lemma-equ4 : {a b c d : Obj A} → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → 300 lemma-equ4 : {a b c d : Obj A} → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) →
300 A [ A [ f o A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ] ] ≈ A [ g o A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ] ] ] 301 A [ A [ f o A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ] ] ≈ A [ g o A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ] ] ]
301 lemma-equ4 {a} {b} {c} {d} f g h = let open ≈-Reasoning (A) in 302 lemma-equ4 {a} {b} {c} {d} f g h = let open ≈-Reasoning (A) in
302 begin 303 begin
327 ∎ 328 ∎
328 cong-δ1 : {a b c : Obj A} {e : Hom A c a } {f f' : Hom A a b} → A [ f ≈ f' ] → A [ k (eqa {a} {b} {c} f f {e} ) (id1 A a) (f1=f1 f) ≈ 329 cong-δ1 : {a b c : Obj A} {e : Hom A c a } {f f' : Hom A a b} → A [ f ≈ f' ] → A [ k (eqa {a} {b} {c} f f {e} ) (id1 A a) (f1=f1 f) ≈
329 k (eqa {a} {b} {c} f' f' {e} ) (id1 A a) (f1=f1 f') ] 330 k (eqa {a} {b} {c} f' f' {e} ) (id1 A a) (f1=f1 f') ]
330 cong-δ1 {a} {b} {c} {e} {f} {f'} f=f' = let open ≈-Reasoning (A) in 331 cong-δ1 {a} {b} {c} {e} {f} {f'} f=f' = let open ≈-Reasoning (A) in
331 begin 332 begin
332 k (eqa {a} {b} {c} f f {e} ) (id1 A a) (f1=f1 f) 333 k (eqa {a} {b} {c} f f {e} ) (id a) (f1=f1 f)
333 ≈⟨ uniqueness (eqa f f) ( begin 334 ≈⟨ uniqueness (eqa f f) ( begin
334 e o k (eqa {a} {b} {c} f' f' {e} ) (id1 A a) (f1=f1 f') 335 e o k (eqa {a} {b} {c} f' f' {e} ) (id a) (f1=f1 f')
335 ≈⟨ ek=h (eqa {a} {b} {c} f' f' {e} ) ⟩ 336 ≈⟨ ek=h (eqa {a} {b} {c} f' f' {e} ) ⟩
336 id1 A a 337 id a
337 ∎ )⟩ 338 ∎ )⟩
338 k (eqa {a} {b} {c} f' f' {e} ) (id1 A a) (f1=f1 f') 339 k (eqa {a} {b} {c} f' f' {e} ) (id a) (f1=f1 f')
339 ∎ 340 ∎
340 341
341 lemma-b2 : {d : Obj A} {h : Hom A d a} → A [ 342 lemma-b2 : {d : Obj A} {h : Hom A d a} → A [
342 A [ equalizer (eqa f g) o k (eqa f g) (A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ]) (lemma-equ4 {a} {b} {c} f g h) ] 343 A [ equalizer (eqa f g) o k (eqa f g) (A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ]) (lemma-equ4 {a} {b} {c} f g h) ]
343 ≈ A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ] ] 344 ≈ A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ] ]
360 (lemma-equ4 {a} {b} {c} f g (( equalizer (eqa f g) o j ))) o 361 (lemma-equ4 {a} {b} {c} f g (( equalizer (eqa f g) o j ))) o
361 k (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) (id1 A d) (f1=f1 (( f o ( equalizer (eqa f g) o j ) ))) ) 362 k (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) (id1 A d) (f1=f1 (( f o ( equalizer (eqa f g) o j ) ))) )
362 ≈⟨ car ((uniqueness (eqa f g) ( begin 363 ≈⟨ car ((uniqueness (eqa f g) ( begin
363 equalizer (eqa f g) o j 364 equalizer (eqa f g) o j
364 ≈↑⟨ idR ⟩ 365 ≈↑⟨ idR ⟩
365 (equalizer (eqa f g) o j ) o id1 A d 366 (equalizer (eqa f g) o j ) o id d
366 ≈⟨⟩ -- here we decide e (fej) (gej)' is id1 A d 367 ≈⟨⟩ -- here we decide e (fej) (gej)' is id d
367 ((equalizer (eqa f g) o j) o equalizer (eqa (f o equalizer (eqa f g {e}) o j) (g o equalizer (eqa f g {e}) o j))) 368 ((equalizer (eqa f g) o j) o equalizer (eqa (f o equalizer (eqa f g {e}) o j) (g o equalizer (eqa f g {e}) o j)))
368 ∎ ))) ⟩ 369 ∎ ))) ⟩
369 j o k (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) (id1 A d) (f1=f1 (( f o ( equalizer (eqa f g) o j ) ))) 370 j o k (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) (id1 A d) (f1=f1 (( f o ( equalizer (eqa f g) o j ) )))
370 ≈⟨ cdr ((uniqueness (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) ( begin 371 ≈⟨ cdr ((uniqueness (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) ( begin
371 equalizer (eqa (f o equalizer (eqa f g {e} ) o j) (f o equalizer (eqa f g {e}) o j)) o id1 A d 372 equalizer (eqa (f o equalizer (eqa f g {e} ) o j) (f o equalizer (eqa f g {e}) o j)) o id d
372 ≈⟨ idR ⟩ 373 ≈⟨ idR ⟩
373 equalizer (eqa (f o equalizer (eqa f g {e}) o j) (f o equalizer (eqa f g {e}) o j)) 374 equalizer (eqa (f o equalizer (eqa f g {e}) o j) (f o equalizer (eqa f g {e}) o j))
374 ≈⟨⟩ -- here we decide e (fej) (fej)' is id1 A d 375 ≈⟨⟩ -- here we decide e (fej) (fej)' is id d
375 id1 A d 376 id d
376 ∎ ))) ⟩ 377 ∎ ))) ⟩
377 j o id1 A d 378 j o id d
378 ≈⟨ idR ⟩ 379 ≈⟨ idR ⟩
379 j 380 j
380 ∎ 381 ∎
381 382
382 -------------------------------- 383 --------------------------------
399 ek=h1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ (α bur f g e) o k1 {d} h eq ] ≈ h ] 400 ek=h1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ (α bur f g e) o k1 {d} h eq ] ≈ h ]
400 ek=h1 {d} {h} {eq} = let open ≈-Reasoning (A) in 401 ek=h1 {d} {h} {eq} = let open ≈-Reasoning (A) in
401 begin 402 begin
402 α bur f g e o k1 h eq 403 α bur f g e o k1 h eq
403 ≈⟨⟩ 404 ≈⟨⟩
404 α bur f g e o ( γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} (id1 A d) (f o h) ) 405 α bur f g e o ( γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} (id d) (f o h) )
405 ≈⟨ assoc ⟩ 406 ≈⟨ assoc ⟩
406 ( α bur f g e o γ bur {a} {b} {c} f g h ) o δ bur {d} {b} {d} (id1 A d) (f o h) 407 ( α bur f g e o γ bur {a} {b} {c} f g h ) o δ bur {d} {b} {d} (id d) (f o h)
407 ≈⟨ car (b2 bur) ⟩ 408 ≈⟨ car (b2 bur) ⟩
408 ( h o ( α bur ( f o h ) ( g o h ) (id1 A d))) o δ bur {d} {b} {d} (id1 A d) (f o h) 409 ( h o ( α bur ( f o h ) ( g o h ) (id d))) o δ bur {d} {b} {d} (id d) (f o h)
409 ≈↑⟨ assoc ⟩ 410 ≈↑⟨ assoc ⟩
410 h o ((( α bur ( f o h ) ( g o h ) (id1 A d) )) o δ bur {d} {b} {d} (id1 A d) (f o h) ) 411 h o ((( α bur ( f o h ) ( g o h ) (id d) )) o δ bur {d} {b} {d} (id d) (f o h) )
411 ≈↑⟨ cdr ( car ( cong-α bur eq)) ⟩ 412 ≈↑⟨ cdr ( car ( cong-α bur eq)) ⟩
412 h o ((( α bur ( f o h ) ( f o h ) (id1 A d)))o δ bur {d} {b} {d} (id1 A d) (f o h) ) 413 h o ((( α bur ( f o h ) ( f o h ) (id d)))o δ bur {d} {b} {d} (id d) (f o h) )
413 ≈⟨ cdr (b3 bur {d} {b} {d} (f o h) {id1 A d} ) ⟩ 414 ≈⟨ cdr (b3 bur {d} {b} {d} (f o h) {id d} ) ⟩
414 h o id1 A d 415 h o id d
415 ≈⟨ idR ⟩ 416 ≈⟨ idR ⟩
416 h 417 h
417 ∎ 418 ∎
418 uniqueness1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → 419 uniqueness1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } →
419 A [ A [ (α bur f g e) o k' ] ≈ h ] → A [ k1 {d} h eq ≈ k' ] 420 A [ A [ (α bur f g e) o k' ] ≈ h ] → A [ k1 {d} h eq ≈ k' ]
420 uniqueness1 {d} {h} {eq} {k'} ek=h = let open ≈-Reasoning (A) in 421 uniqueness1 {d} {h} {eq} {k'} ek=h = let open ≈-Reasoning (A) in
421 begin 422 begin
422 k1 {d} h eq 423 k1 {d} h eq
423 ≈⟨⟩ 424 ≈⟨⟩
424 γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} (id1 A d) (f o h) 425 γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} (id d) (f o h)
425 ≈↑⟨ car (cong-γ bur {a} {b} {c} {d} ek=h ) ⟩ 426 ≈↑⟨ car (cong-γ bur {a} {b} {c} {d} ek=h ) ⟩
426 γ bur f g (A [ α bur f g e o k' ]) o δ bur {d} {b} {d} (id1 A d) (f o h) 427 γ bur f g (A [ α bur f g e o k' ]) o δ bur {d} {b} {d} (id d) (f o h)
427 ≈↑⟨ cdr (cong-δ bur (resp ek=h refl-hom )) ⟩ 428 ≈↑⟨ cdr (cong-δ bur (resp ek=h refl-hom )) ⟩
428 γ bur f g (A [ α bur f g e o k' ]) o δ bur {d} {b} {d} (id1 A d) ( f o ( α bur f g e o k') ) 429 γ bur f g (A [ α bur f g e o k' ]) o δ bur {d} {b} {d} (id d) ( f o ( α bur f g e o k') )
429 ≈⟨ b4 bur ⟩ 430 ≈⟨ b4 bur ⟩
430 k' 431 k'
431 ∎ 432 ∎
432 433
433 434