Mercurial > hg > Members > kono > Proof > category
comparison pullback.agda @ 692:3ca3b5a4ab45
fix comment
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 12 Nov 2017 10:01:06 +0900 |
| parents | 917e51be9bbf |
| children | 984518c56e96 |
comparison
equal
deleted
inserted
replaced
| 691:917e51be9bbf | 692:3ca3b5a4ab45 |
|---|---|
| 320 | 320 |
| 321 -- | 321 -- |
| 322 -- limit from equalizer and product | 322 -- limit from equalizer and product |
| 323 -- | 323 -- |
| 324 -- Γu | 324 -- Γu |
| 325 -- +--→ Γ j → Γ k ←--+ | 325 -- → Γj → Γk ← |
| 326 -- | ↑ ↑ | | 326 -- / ↑ ↑ \ |
| 327 -- proj j | | | |proj k | 327 -- proj j / | | \ proj k |
| 328 -- | μu| |μu | | 328 -- / μu| |μu \ Equalizer have to be independent from j and k |
| 329 -- | | | | | 329 -- | | | | so we need products of Obj I and Hom I |
| 330 -- |product of Hom I | | 330 -- |product of Hom I | |
| 331 -- | ↑ ↑ | K u = id lim | 331 -- | ↑ ↑ | K u = id lim |
| 332 -- | f(id)} | | | 332 -- | f(id)} | | |
| 333 -- | | |g(Γ) | lim = K j -----------→ K k = lim | 333 -- | | |g(Γ) | lim = K j -----------→ K k = lim |
| 334 -- | | | | | u | | 334 -- | | | | | u | |
| 335 -- | | | | proj j o e = ε j | | ε k = proj k o e | 335 -- \ | | / proj j o e = ε j | | ε k = proj k o e |
| 336 -- product of Obj I μ u o g o e | | μ u o f o e | 336 -- product of Obj I μ u o g o e | | μ u o f o e |
| 337 -- ↑ | | | 337 -- ↑ | | |
| 338 -- | e = equalizer f g | | | 338 -- | e = equalizer f g | | |
| 339 -- | ↓ ↓ | 339 -- | ↓ ↓ |
| 340 -- lim ←---------------- d' Γ j ----------→ Γ k | 340 -- lim ←---------------- d' Γ j ----------→ Γ k |