# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1510067150 -32400
# Node ID 88e8a1290dc4ac9525b1f29234018472a44d9a98
# Parent  50a01df1169a6f17ad891ed4a1a6348e65d69e8f
clean up

diff -r 50a01df1169a -r 88e8a1290dc4 pullback.agda
--- a/pullback.agda	Tue Nov 07 23:48:46 2017 +0900
+++ b/pullback.agda	Wed Nov 08 00:05:50 2017 +0900
@@ -30,9 +30,6 @@
 open IsEqualizer
 open IsProduct
 
---          ( A [  π1 o equalizer1 ( eqa ( A [ f  o π1 ] ) ( A [ g  o π2 ] ) )  ] )
---          ( A [  π2 o equalizer1 ( eqa ( A [ f  o π1 ] ) ( A [ g  o π2 ] ) )  ] )
-
 pullback-from :  {a b c : Obj A}
       ( f : Hom A a c )    ( g : Hom A b c )
       ( eqa : {a b : Obj A} → (f g : Hom A a b)  → Equalizer A f g )
@@ -381,9 +378,11 @@
          e : Hom A d p0
          e = equalizer equ-ε 
          equ = isEqualizer  equ-ε 
+         -- projection of the product of Obj I
          proj : (i : Obj I) → Hom A p0 (FObj Γ i)
          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) 
          limit-ε :  NTrans I A (K A I (equalizer-c equ-ε ) ) Γ
@@ -418,20 +417,23 @@
                  ≈⟨⟩
                       tmap k o FMap (K A I d) u
                  ∎ 
+         --  an arrow to our product of Obj I ( is an equalizer because of commutativity of t )
+         h : {a : Obj A} → (t : NTrans I A (K A I a) Γ ) → Hom A a p0
+         h t = iproduct prodΓ (TMap t) 
          fh=gh : (a : Obj A) → (t : NTrans I A (K A I a) Γ ) →
-            A [ A [ g o iproduct prodΓ (TMap t) ] ≈ A [ f o iproduct prodΓ (TMap t) ] ]
+            A [ A [ g o h t ] ≈ A [ f o h t ] ]
          fh=gh a t = let  open ≈-Reasoning (A) in begin
-                  g o iproduct prodΓ (TMap t) 
+                  g o h t
                 ≈↑⟨ ip-uniqueness (isIProduct (prod Fcod)) ⟩
-                  iproduct (isIProduct (prod Fcod)) (λ u →  pi (prod Fcod) u o ( g o iproduct prodΓ (TMap t) ))
+                  iproduct (isIProduct (prod Fcod)) (λ u →  pi (prod Fcod) u o ( g o h t ))
                 ≈⟨ ip-cong  (isIProduct (prod Fcod)) ( λ u →  begin
-                            pi (prod Fcod) u o ( g o iproduct prodΓ (TMap t)  )
+                            pi (prod Fcod) u o ( g o h t )
                         ≈⟨ assoc ⟩
-                            ( pi (prod Fcod) u o  g ) o iproduct prodΓ (TMap t)  
+                            ( pi (prod Fcod) u o  g ) o h t
                         ≈⟨ car (pif=q  (isIProduct (prod Fcod ))) ⟩
-                            (FMap Γ (hom u) o  pi (prod (FObj Γ)) (hom-j u) )  o iproduct prodΓ (TMap t)
+                            (FMap Γ (hom u) o  pi (prod (FObj Γ)) (hom-j u) )  o h t
                         ≈↑⟨ assoc ⟩
-                            FMap Γ (hom u) o (pi (prod (FObj Γ)) (hom-j u)   o iproduct prodΓ (TMap t) )
+                            FMap Γ (hom u) o (pi (prod (FObj Γ)) (hom-j u)   o h t )
                         ≈⟨ cdr ( pif=q prodΓ ) ⟩
                             FMap Γ (hom u) o TMap t (hom-j u)
                         ≈⟨ IsNTrans.commute (isNTrans t) ⟩
@@ -439,29 +441,29 @@
                         ≈⟨ idR ⟩
                             TMap t (hom-k u) 
                         ≈↑⟨  pif=q prodΓ  ⟩
-                           pi (prod (FObj Γ)) (hom-k u) o iproduct prodΓ (TMap t)
+                           pi (prod (FObj Γ)) (hom-k u) o h t
                         ≈↑⟨ car (pif=q  (isIProduct (prod Fcod ))) ⟩
-                            (pi (prod Fcod) u o  f ) o iproduct prodΓ (TMap t)  
+                            (pi (prod Fcod) u o  f ) o h t
                         ≈↑⟨ assoc ⟩
-                            pi (prod Fcod) u o ( f o iproduct prodΓ (TMap t)  )
+                            pi (prod Fcod) u o ( f o h t )
                         ∎
                  ) ⟩
-                  iproduct (isIProduct (prod Fcod)) (λ u →  pi (prod Fcod) u o ( f o iproduct prodΓ (TMap t)) )
+                  iproduct (isIProduct (prod Fcod)) (λ u →  pi (prod Fcod) u o ( f o h t ))
                 ≈⟨ ip-uniqueness (isIProduct (prod Fcod)) ⟩
-                  f o iproduct prodΓ (TMap t) 
+                  f o h t
                 ∎
          limit1 :  (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a d
-         limit1 a t =  k equ (iproduct prodΓ (TMap t) ) ( fh=gh a t )
+         limit1 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 ]
          t0f=t1 {a} {t} {i} = let  open ≈-Reasoning (A) in begin
                    TMap limit-ε  i o limit1 a t 
                 ≈⟨⟩
-                   ( ( proj i )  o e ) o  k equ (iproduct prodΓ (TMap t) ) (fh=gh a t)
+                   ( ( proj i )  o e ) o  k equ (h t) (fh=gh a t)
                 ≈↑⟨ assoc  ⟩
-                    proj i  o ( e  o  k equ (iproduct prodΓ (TMap t) ) (fh=gh a t ) )
+                    proj i  o ( e  o  k equ (h t) (fh=gh a t ) )
                 ≈⟨ cdr ( ek=h equ) ⟩
-                    proj i  o iproduct prodΓ (TMap t)
+                    proj i  o h t
                 ≈⟨ pif=q prodΓ ⟩
                    TMap t i 
                 ∎
@@ -471,7 +473,7 @@
          limit-uniqueness1 {a} {t} {f} lim=t = let  open ≈-Reasoning (A) in begin
                     limit1 a t
                 ≈⟨⟩
-                    k equ (iproduct prodΓ (TMap t) ) (fh=gh a t)
+                    k equ (h t) (fh=gh a t)
                 ≈⟨ IsEqualizer.uniqueness  equ ( begin
                       e o f 
                 ≈↑⟨ ip-uniqueness prodΓ ⟩
@@ -483,7 +485,7 @@
                 ≈⟨ lim=t {i} ⟩
                         TMap t i
                 ∎ ) ⟩
-                      iproduct prodΓ (TMap t)
+                      h t
                 ∎ ) ⟩
                     f
                 ∎