Mercurial > hg > Members > kono > Proof > category

comparison src/yoneda.agda @ 995:1d365952dde4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 06 Mar 2021 23:02:33 +0900
parents e7848ad0c6f9
children 6cd40df80dec
comparison
equal deleted inserted replaced
994:485bc7560a75 995:1d365952dde4
309 309
310 -- 310 --
311 -- f ∈ FMap (FObj YonedaFunctor a') a 311 -- f ∈ FMap (FObj YonedaFunctor a') a
312 -- 312 --
313 313
314 -- g f
315 -- b --→ a ------→ a'
316 -- | |
317 -- | |
318 -- ↓ ↓
319 -- H a ------→ H a'
320 -- H f
321 --
314 _^ : {a a' b : Obj A } → (f : Hom A a a' ) → Hom A b a → Hom A b a' 322 _^ : {a a' b : Obj A } → (f : Hom A a a' ) → Hom A b a → Hom A b a'
315 _^ {a} {a'} {b} f g = (FMap (FObj YonedaFunctor a') g) f 323 _^ {a} {a'} {b} f g = (FMap (FObj YonedaFunctor a') g) f
316 324
317 f-unique : {a a' b : Obj A } (f : Hom A a a' ) → f ^ ≡ TMap (FMap YonedaFunctor f) b 325 f-unique : {a a' b : Obj A } (f : Hom A a a' ) → f ^ ≡ TMap (FMap YonedaFunctor f) b
318 f-unique {a} {a'} {b} f = extensionality A (λ g → begin 326 f-unique {a} {a'} {b} f = extensionality A (λ g → begin
321 A [ f o g ] ≡⟨⟩ 329 A [ f o g ] ≡⟨⟩
322 TMap (FMap YonedaFunctor f) b g ∎ ) where open ≡-Reasoning 330 TMap (FMap YonedaFunctor f) b g ∎ ) where open ≡-Reasoning
323 331
324 postulate 332 postulate
325 eqObj0 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a a' b b' : Obj A} → Hom A a b ≡ Hom A a' b' → a ≡ a' 333 eqObj0 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a a' b b' : Obj A} → Hom A a b ≡ Hom A a' b' → a ≡ a'
326 eqObj1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a a' b b' : Obj A} → Hom A a b ≡ Hom A a' b' → b ≡ b'
327 eqHom0 : {a b c : Obj A } {f f' : Hom A b c } {g g' : Hom A a b } → A [ f o g ] ≡ A [ f' o g' ] → f ≡ f' 334 eqHom0 : {a b c : Obj A } {f f' : Hom A b c } {g g' : Hom A a b } → A [ f o g ] ≡ A [ f' o g' ] → f ≡ f'
328 eqHom1 : {a b c : Obj A } {f f' : Hom A b c } {g g' : Hom A a b } → A [ f o g ] ≡ A [ f' o g' ] → g ≡ g' 335 eqHom1 : {a b c : Obj A } {f f' : Hom A b c } {g g' : Hom A a b } → A [ f o g ] ≡ A [ f' o g' ] → g ≡ g'
329 -- eqTMap : { y b : Obj A} { x z : Obj Sets} → {g h : NTrans (Category.op A) Sets (y-obj b) ? } {w : {!!} } → TMap g x {!!} ≡ TMap h x w → g ≡ h 336 -- eqTMap : { y b : Obj A} { x z : Obj Sets} → {g h : NTrans (Category.op A) Sets (y-obj b) ? } {w : {!!} } → TMap g x {!!} ≡ TMap h x w → g ≡ h
337
338 open import Category.Cat
339
340
341 ≃→a=a : {c₁ c₂ ℓ : Level} (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B }
342 → ( f : Hom B a b )
343 → ( g : Hom B a' b' )
344 → [_]_~_ B f g → a ≡ a'
345 ≃→a=a B f g (refl eqv) = refl
346
347 ≃→b=b : {c₁ c₂ ℓ : Level} (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B }
348 → ( f : Hom B a b )
349 → ( g : Hom B a' b' )
350 → [_]_~_ B f g → b ≡ b'
351 ≃→b=b B f g (refl eqv) = refl
352
353 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_)
354
355 eqObj1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a b : Obj A} → Hom A a a ≡ Hom A a b → a ≡ b
356 eqObj1 A {a} {b} eq = lem (subst (λ k → k) eq (id1 A a)) eq where
357 lem : (f : Hom A a b ) → f ≅ id1 A a → Hom A a a ≡ Hom A a b → a ≡ b
358 lem _ HE.refl refl = refl
330 359
331 -- full (injective ) 360 -- full (injective )
332 Yoneda-injective : {a b : Obj A } → {x y : Obj SetsAop} → (g h : Hom SetsAop y (FObj YonedaFunctor a)) (f : Hom A a b ) 361 Yoneda-injective : {a b : Obj A } → {x y : Obj SetsAop} → (g h : Hom SetsAop y (FObj YonedaFunctor a)) (f : Hom A a b )
333 → SetsAop [ SetsAop [ FMap YonedaFunctor f o g ] ≈ SetsAop [ FMap YonedaFunctor f o h ] ] 362 → SetsAop [ SetsAop [ FMap YonedaFunctor f o g ] ≈ SetsAop [ FMap YonedaFunctor f o h ] ]
334 → SetsAop [ g ≈ h ] 363 → SetsAop [ g ≈ h ]
356 ylem12 : {y : Obj A} → { z : Hom A y a } → TMap g y (A [ f o z ]) ≡ TMap h y (A [ f o z ]) 385 ylem12 : {y : Obj A} → { z : Hom A y a } → TMap g y (A [ f o z ]) ≡ TMap h y (A [ f o z ])
357 ylem12 {y} {z} = cong (λ k → k z ) (yg=yh {y} ) 386 ylem12 {y} {z} = cong (λ k → k z ) (yg=yh {y} )
358 ylem10 : {y : Obj A} → (λ z → TMap g y (A [ f o z ])) ≡ (λ z → TMap h y (A [ f o z ] )) 387 ylem10 : {y : Obj A} → (λ z → TMap g y (A [ f o z ])) ≡ (λ z → TMap h y (A [ f o z ] ))
359 ylem10 = yg=yh 388 ylem10 = yg=yh
360 389
361 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_)
362
363 Yoneda-full-embed : {a b : Obj A } → FObj YonedaFunctor a ≡ FObj YonedaFunctor b → a ≡ b 390 Yoneda-full-embed : {a b : Obj A } → FObj YonedaFunctor a ≡ FObj YonedaFunctor b → a ≡ b
364 Yoneda-full-embed {a} {b} eq = eqObj1 A ylem1 where 391 Yoneda-full-embed {a} {b} eq = eqObj1 A ylem1 where
365 ylem1 : Hom A a a ≡ Hom A a b 392 ylem1 : Hom A a a ≡ Hom A a b
366 ylem1 = cong (λ k → FObj k a) eq 393 ylem1 = cong (λ k → FObj k a) eq
367 394