# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1510098011 -32400
# Node ID f5f582ae20bbeb4d3d534257edf36e3ca38837b6
# Parent  5d9d7c2f2718d7b08096c590814d5fecf09b57d4
...

diff -r 5d9d7c2f2718 -r f5f582ae20bb pullback.agda
--- a/pullback.agda	Wed Nov 08 00:09:21 2017 +0900
+++ b/pullback.agda	Wed Nov 08 08:40:11 2017 +0900
@@ -318,8 +318,8 @@
 --
 -- limit from equalizer and product
 --
---      
---         Γ j  =    Γ k
+--              Γu
+--         Γ j ----→ Γ k
 --        ↑  ^       ↑ ↑   
 --        |  |       | |proj k
 --        |  |mu u   |mu u
@@ -356,9 +356,9 @@
       → Limit A I Γ 
 limit-from prod eqa = record {
      a0 = d ;
-     t0 = limit-ε ; 
+     t0 = cone-ε ; 
      isLimit = record {
-             limit = λ a t → limit1 a t ;
+             limit = λ a t → cone1 a t ;
              t0f=t = λ {a t i } → t0f=t1  {a} {t} {i} ;
              limit-uniqueness =  λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
      }
@@ -385,8 +385,8 @@
          -- projection of the product of Hom I
          mu : {j k : Obj I} → (u : Hom I j k ) → Hom A (iprod (prod Fcod)) (Fcod (Homprod u))
          mu u = pi (prod Fcod ) (Homprod u) 
-         limit-ε :  NTrans I A (K A I (equalizer-c equ-ε ) ) Γ
-         limit-ε = record {
+         cone-ε :  NTrans I A (K A I (equalizer-c equ-ε ) ) Γ
+         cone-ε = record {
                TMap = λ i → tmap i ; 
                isNTrans = record { commute = commute1 }
            } where
@@ -452,12 +452,12 @@
                 ≈⟨ ip-uniqueness (isIProduct (prod Fcod)) ⟩
                   f o h t
                 ∎
-         limit1 :  (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a d
-         limit1 a t =  k equ (h t) ( fh=gh a t )
+         cone1 :  (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a d
+         cone1 a t =  k equ (h t) ( fh=gh a t )
          t0f=t1 :  {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} →
-                A [ A [ TMap limit-ε  i o limit1 a t ] ≈ TMap t i ]
+                A [ A [ TMap cone-ε  i o cone1 a t ] ≈ TMap t i ]
          t0f=t1 {a} {t} {i} = let  open ≈-Reasoning (A) in begin
-                   TMap limit-ε  i o limit1 a t 
+                   TMap cone-ε  i o cone1 a t 
                 ≈⟨⟩
                    ( ( proj i )  o e ) o  k equ (h t) (fh=gh a t)
                 ≈↑⟨ assoc  ⟩
@@ -468,10 +468,10 @@
                    TMap t i 
                 ∎
          limit-uniqueness1 :  {a : Obj A} {t : NTrans I A (K A I a) Γ} {f : Hom A a d} 
-                → ({i : Obj I} → A [ A [ TMap limit-ε  i o f ] ≈ TMap t i ]) →
-                A [ limit1 a t ≈ f ]
+                → ({i : Obj I} → A [ A [ TMap cone-ε  i o f ] ≈ TMap t i ]) →
+                A [ cone1 a t ≈ f ]
          limit-uniqueness1 {a} {t} {f} lim=t = let  open ≈-Reasoning (A) in begin
-                    limit1 a t
+                    cone1 a t
                 ≈⟨⟩
                     k equ (h t) (fh=gh a t)
                 ≈⟨ IsEqualizer.uniqueness  equ ( begin