# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1510138653 -32400
# Node ID 14ad6ec8a6626ebc641eb5b019dc4c558a326f60
# Parent  f5f582ae20bbeb4d3d534257edf36e3ca38837b6
fix comment

diff -r f5f582ae20bb -r 14ad6ec8a662 pullback.agda
--- a/pullback.agda	Wed Nov 08 08:40:11 2017 +0900
+++ b/pullback.agda	Wed Nov 08 19:57:33 2017 +0900
@@ -46,15 +46,15 @@
               uniqueness = uniqueness1
          }
       } where
-      ab : Obj A
-      ab =  Product.product (prod0 a b) 
-      π1 : Hom A ab a
+      axb : Obj A
+      axb =  Product.product (prod0 a b) 
+      π1 : Hom A axb a
       π1 = Product.π1 (prod0 a b ) 
-      π2 : Hom A ab b
+      π2 : Hom A axb b
       π2 = Product.π2 (prod0 a b ) 
       d : Obj A
       d = equalizer-c (eqa (A [ f o π1 ]) (A [ g o π2 ]))
-      e : Hom A d ab 
+      e : Hom A d axb 
       e = equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]))
       prod = Product.isProduct (prod0 a b)
       commute1 :  A [ A [ f o A [ π1 o e ] ]
@@ -300,6 +300,7 @@
         ∎
 
 
+-- another form of uniqueness of a product
 lemma-p0 :   (a b ab : Obj A) ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( prod : IsProduct A a b ab π1 π2 ) →
       A [ _×_ prod π1 π2 ≈  id1 A ab  ]
 lemma-p0  a b ab π1 π2 prod =  let  open ≈-Reasoning (A) in begin
@@ -319,27 +320,28 @@
 -- limit from equalizer and product
 --
 --              Γu
---         Γ j ----→ Γ k
---        ↑  ^       ↑ ↑   
---        |  |       | |proj k
---        |  |mu u   |mu u
---        |  |       | |
---        | product of Hom i
---        |  ↑       ↑ |                          K u = id lim                        
---        |  |       | |                         
---        | f|id    g|λ u → Γ u           d = K j -----------→ K k = d
--- 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
---        ^                                     |               |
+--        +--→ Γ j → Γ k ←--+
+--        |      ↑   ↑      |   
+-- proj j |      |   |      |proj k
+--        |    μu|   |μu    |
+--        |      |   |      |
+--        |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
+--         product of Obj I       μ  u o g o e  |               | μ  u o f o e
+--        ↑                                     |               |
 --        | e = equalizer f g                   |               |
 --        |                                     ↓               ↓
---       lim ←---------------- d'     a j = Γ j -----------→ Γ k = a j
+--       lim ←---------------- d'              Γ j ----------→ Γ k 
 --              k ( product pi )                     Γ u
 --                                              Γ u o ε j = ε k 
 --
 
 -- homprod should be written by IProduct
+-- If I is locally small, this is iso to a set
 record homprod {c : Level } : Set (suc c₁' ⊔ suc c₂' ) where
    field
       hom-j : Obj I
@@ -383,8 +385,8 @@
          proj = pi ( prod  (FObj Γ) )
          prodΓ = isIProduct ( prod (FObj Γ) ) 
          -- 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) 
+         μ  : {j k : Obj I} → (u : Hom I j k ) → Hom A (iprod (prod Fcod)) (Fcod (Homprod u))
+         μ  u = pi (prod Fcod ) (Homprod u) 
          cone-ε :  NTrans I A (K A I (equalizer-c equ-ε ) ) Γ
          cone-ε = record {
                TMap = λ i → tmap i ; 
@@ -401,13 +403,13 @@
                  ≈⟨ assoc ⟩
                       ( FMap Γ u o  pi (prod (FObj Γ)) j ) o e 
                  ≈↑⟨ car ( pif=q (isIProduct (prod Fcod )) ) ⟩
-                     ( mu u o g ) o e 
+                     ( μ  u o g ) o e 
                  ≈↑⟨ assoc ⟩
-                       mu u o (g  o e )
+                       μ  u o (g  o e )
                  ≈⟨ cdr ( fe=ge (isEqualizer equ-ε )) ⟩
-                       mu u o (f  o e )
+                       μ  u o (f  o e )
                  ≈⟨ assoc ⟩
-                     (mu u o f ) o e 
+                     (μ  u o f ) o e 
                  ≈⟨ car ( pif=q (isIProduct (prod Fcod )))   ⟩
                        pi (prod (FObj Γ)) k o e 
                  ≈⟨⟩