Mercurial > hg > Members > kono > Proof > category
comparison pullback.agda @ 684:5d9d7c2f2718
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 08 Nov 2017 00:09:21 +0900 |
| parents | 88e8a1290dc4 |
| children | f5f582ae20bb |
comparison
equal
deleted
inserted
replaced
| 683:88e8a1290dc4 | 684:5d9d7c2f2718 |
|---|---|
| 318 -- | 318 -- |
| 319 -- limit from equalizer and product | 319 -- limit from equalizer and product |
| 320 -- | 320 -- |
| 321 -- | 321 -- |
| 322 -- Γ j = Γ k | 322 -- Γ j = Γ k |
| 323 -- ↑ ^ ↑ | 323 -- ↑ ^ ↑ ↑ |
| 324 -- | | | | 324 -- | | | |proj k |
| 325 -- | |mu u |mu u | 325 -- | |mu u |mu u |
| 326 -- | | | | 326 -- | | | | |
| 327 -- | product of Hom i | 327 -- | product of Hom i |
| 328 -- | ↑ ↑ K u = id lim | 328 -- | ↑ ↑ | K u = id lim |
| 329 -- | | | | 329 -- | | | | |
| 330 -- | f|id g|λ u → Γ u d = K j -----------→ K k = d | 330 -- | f|id g|λ u → Γ u d = K j -----------→ K k = d |
| 331 -- proj u | | | | u | | 331 -- proj j | | | | | u | |
| 332 -- | | | proj j o e = ε j | | ε k = proj k o e | 332 -- | | | | proj j o e = ε j | | ε k = proj k o e |
| 333 -- product of Obj i -+ mu u o g o e | | mu u o f o e | 333 -- product of Obj i -+ mu u o g o e | | mu u o f o e |
| 334 -- ^ | | | 334 -- ^ | | |
| 335 -- | e = equalizer f g | | | 335 -- | e = equalizer f g | | |
| 336 -- | ↓ ↓ | 336 -- | ↓ ↓ |
| 337 -- lim ←---------------- d' a j = Γ j -----------→ Γ k = a j | 337 -- lim ←---------------- d' a j = Γ j -----------→ Γ k = a j |