--- a/pullback.agda	Wed Sep 26 20:17:09 2018 +0900
+++ b/pullback.agda	Sat Oct 06 13:42:27 2018 +0900
@@ -320,16 +320,16 @@
 --
 --              Γu
 --            → Γj → Γk ←   
---           /   ↑   ↑    \     
--- proj j   /    |   |     \ proj k
---         /   μu|   |μu    \           Equalizer have to be independent from j and 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
+--        |      }   |      |                       
+--        | 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                   |               |