# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1509930655 -32400
# Node ID 5d894993477f228823919cb5a267c9878ab4de80
# Parent  20bdd2f5f708bff9da7a776d85914bc0abb6101d
fh=gh done. limit from product and equalizer done

diff -r 20bdd2f5f708 -r 5d894993477f pullback.agda
--- a/pullback.agda	Sun Nov 05 16:33:37 2017 +0900
+++ b/pullback.agda	Mon Nov 06 10:10:55 2017 +0900
@@ -328,6 +328,9 @@
       hom : Hom I hom-j hom-k
 open homprod
 
+Homprod : {j k : Obj I} (u : Hom I j k) → homprod {c₁}
+Homprod {j} {k} u = record {hom-j = j ; hom-k = k ; hom = u}
+
 Fcod : homprod {c₁} → Obj A
 Fcod = λ  u →  FObj Γ ( hom-k u )
 
@@ -372,13 +375,13 @@
          ≈⟨ assoc ⟩
               ( FMap Γ u o  pi (prod (FObj Γ)) j ) o e 
          ≈↑⟨ car ( pif=q (isIProduct (prod Fcod )) ) ⟩
-             ( pi (prod Fcod ) (record {hom-j = j ; hom-k = k ; hom = u} ) o g ) o e 
+             ( pi (prod Fcod ) (Homprod u) o g ) o e 
          ≈↑⟨ assoc ⟩
-               pi (prod Fcod ) (record {hom-j = j ; hom-k = k ; hom = u} ) o (g  o e )
+               pi (prod Fcod ) (Homprod u) o (g  o e )
          ≈⟨ cdr ( fe=ge (isEqualizer (equ-ε prod eqa ))) ⟩
-               pi (prod Fcod ) (record {hom-j = j ; hom-k = k ; hom = u} ) o (f  o e )
+               pi (prod Fcod ) (Homprod u) o (f  o e )
          ≈⟨ assoc ⟩
-             ( pi (prod Fcod ) (record {hom-j = j ; hom-k = k ; hom = u} ) o f ) o e 
+             ( pi (prod Fcod ) (Homprod u) o f ) o e 
          ≈⟨ car ( pif=q (isIProduct (prod Fcod )))   ⟩
                pi (prod (FObj Γ)) k o e 
          ≈⟨⟩
@@ -404,38 +407,50 @@
     }  where
          lim : Obj A 
          lim = equalizer-c ( equ-ε prod eqa )
+         p0 : Obj A 
          p0 = iprod (prod (FObj Γ))
+         e : Hom A lim p0
          e = let  open ≈-Reasoning (A) in equalizer ( equ-ε prod eqa )
          equ = isEqualizer  ( equ-ε prod eqa )
          proj = pi ( prod  (FObj Γ) )
          prodΓ = isIProduct ( prod (FObj Γ) ) 
          f : Hom A p0 (iprod (prod Fcod))
-         f =  (iproduct (isIProduct (prod Fcod)) (λ u → pi (prod (FObj Γ)) (hom-k u )))
+         f =  iproduct (isIProduct (prod Fcod)) (λ u → pi (prod (FObj Γ)) (hom-k u ))
          g : Hom A p0 (iprod (prod Fcod))
-         g =  (iproduct (isIProduct (prod Fcod)) (λ u → A [ FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u ) ] ))
-         comm1 : (a : Obj A) → (t : NTrans I A (K A I a) Γ ) → (u : homprod)
-            → A [ A [ FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u) ] ≈ pi (prod (FObj Γ)) (hom-k u) ]
-         comm1 a t u = let  open ≈-Reasoning (A) in begin
-                   FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u) 
-                ≈⟨ {!!} ⟩
-                   FMap Γ (hom u) o ( TMap t (hom-j u) o {!!} )
+         g =  iproduct (isIProduct (prod Fcod)) (λ u → A [ FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u ) ] )
+         comm3 : (a : Obj A) → (t : NTrans I A (K A I a) Γ ) → (u : homprod {c₁} )
+            → A [ A [ pi (prod Fcod) u o A [ g o iproduct prodΓ (TMap t) ] ] ≈
+                  A [ pi (prod Fcod) u o A [ f o iproduct prodΓ (TMap t) ] ] ]
+         comm3 a t u =  let  open ≈-Reasoning (A) in begin
+                    pi (prod Fcod) u o ( g o iproduct prodΓ (TMap t)  )
                 ≈⟨ assoc ⟩
-                   (FMap Γ (hom u) o  TMap t (hom-j u) ) o {!!} 
-                ≈⟨ car (IsNTrans.commute (isNTrans t )) ⟩
-                   (TMap t  (hom-k u) o id1 A a ) o {!!}
-                ≈⟨ car idR ⟩
-                   TMap t  (hom-k u)  o {!!}
-                ≈⟨ {!!} ⟩
-                   pi (prod (FObj Γ)) (hom-k u) 
+                    ( pi (prod Fcod) u o  g ) o iproduct prodΓ (TMap t)  
+                ≈⟨ car (pif=q  (isIProduct (prod Fcod ))) ⟩
+                    (FMap Γ (hom u) o  pi (prod (FObj Γ)) (hom-j u) )  o iproduct prodΓ (TMap t)
+                ≈↑⟨ assoc ⟩
+                    FMap Γ (hom u) o (pi (prod (FObj Γ)) (hom-j u)   o iproduct prodΓ (TMap t) )
+                ≈⟨ cdr ( pif=q prodΓ ) ⟩
+                    FMap Γ (hom u) o TMap t (hom-j u)
+                ≈⟨ IsNTrans.commute (isNTrans t) ⟩
+                    TMap t (hom-k u) o id1 A a
+                ≈⟨ idR ⟩
+                    TMap t (hom-k u) 
+                ≈↑⟨  pif=q prodΓ  ⟩
+                   pi (prod (FObj Γ)) (hom-k u) o iproduct prodΓ (TMap t)
+                ≈↑⟨ car (pif=q  (isIProduct (prod Fcod ))) ⟩
+                    (pi (prod Fcod) u o  f ) o iproduct prodΓ (TMap t)  
+                ≈↑⟨ assoc ⟩
+                    pi (prod Fcod) u o ( f o iproduct prodΓ (TMap t)  )
                 ∎
-         comm2 : (a : Obj A) → (t : NTrans I A (K A I a) Γ ) → (u : homprod {c₁} )
-            → A [ A [ FMap Γ (hom u) o TMap t (hom-j u) ] ≈ A [ TMap t  (hom-k u) o id1 A a ] ]
-         comm2 a t u = IsNTrans.commute (isNTrans 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) ] ]
          fh=gh a t = let  open ≈-Reasoning (A) in begin
                   g o iproduct prodΓ (TMap t) 
-                ≈⟨ car ( ip-cong (isIProduct (prod Fcod)) (comm1 a t ) ) ⟩
+                ≈↑⟨ ip-uniqueness (isIProduct (prod Fcod)) ⟩
+                  iproduct (isIProduct (prod Fcod)) (λ u →  pi (prod Fcod) u o ( g o iproduct prodΓ (TMap t) ))
+                ≈⟨ ip-cong  (isIProduct (prod Fcod)) (comm3 a t ) ⟩
+                  iproduct (isIProduct (prod Fcod)) (λ u →  pi (prod Fcod) u o ( f o iproduct prodΓ (TMap t)) )
+                ≈⟨ ip-uniqueness (isIProduct (prod Fcod)) ⟩
                   f o iproduct prodΓ (TMap t) 
                 ∎
          limit1 :  (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a lim