Mercurial > hg > Members > kono > Proof > category
changeset 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 |
| files | pullback.agda |
| diffstat | 1 files changed, 6 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/pullback.agda Sun Nov 12 09:56:40 2017 +0900 +++ b/pullback.agda Sun Nov 12 10:01:06 2017 +0900 @@ -322,17 +322,17 @@ -- limit from equalizer and product -- -- Γu --- +--→ Γ j → Γ k ←--+ --- | ↑ ↑ | --- proj j | | | |proj k --- | μu| |μu | --- | | | | +-- → Γj → Γk ← +-- / ↑ ↑ \ +-- proj j / | | \ proj k +-- / μu| |μu \ Equalizer have to be independent from j and k +-- | | | | so we need products of Obj I and Hom I -- |product of Hom I | -- | ↑ ↑ | K u = id lim -- | f(id)} | | -- | | |g(Γ) | lim = K j -----------→ K k = lim -- | | | | | u | --- | | | | proj j o e = ε j | | ε k = proj k o e +-- \ | | / proj j o e = ε j | | ε k = proj k o e -- product of Obj I μ u o g o e | | μ u o f o e -- ↑ | | -- | e = equalizer f g | |