# HG changeset patch # User Shinji KONO # Date 1510448466 -32400 # Node ID 3ca3b5a4ab45a61a93b7d38391978a529a7e4fc9 # Parent 917e51be9bbf55f0d92696b83b473b4a6ff5f243 fix comment diff -r 917e51be9bbf -r 3ca3b5a4ab45 pullback.agda --- 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 | |