--- a/pullback.agda	Wed Nov 08 00:05:50 2017 +0900
+++ b/pullback.agda	Wed Nov 08 00:09:21 2017 +0900
@@ -320,16 +320,16 @@
 --
 --      
 --         Γ j  =    Γ k
---        ↑  ^       ↑   
---        |  |       |
+--        ↑  ^       ↑ ↑   
+--        |  |       | |proj k
 --        |  |mu u   |mu u
---        |  |       |
+--        |  |       | |
 --        | product of Hom i
---        |  ↑       ↑                            K u = id lim                        
---        |  |       |                           
+--        |  ↑       ↑ |                          K u = id lim                        
+--        |  |       | |                         
 --        | f|id    g|λ u → Γ u           d = K j -----------→ K k = d
--- proj u |  |       |                          |      u        |
---        |  |       |         proj j o e = ε j |               | ε k = proj k o e
+-- proj j |  |       | |                        |      u        |
+--        |  |       | |       proj j o e = ε j |               | ε k = proj k o e
 -- product of Obj i -+         mu u o g o e     |               | mu u o f o e
 --        ^                                     |               |
 --        | e = equalizer f g                   |               |