# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1509778166 -32400
# Node ID 3b23eeecd4f8f4c57313f4be39b7370df5e614b7
# Parent  faf48511f69d6e6b3177c598e3501f8e849a1169
Product of Arrow is necessary ...

diff -r faf48511f69d -r 3b23eeecd4f8 pullback.agda
--- a/pullback.agda	Sat Nov 04 11:49:45 2017 +0900
+++ b/pullback.agda	Sat Nov 04 15:49:26 2017 +0900
@@ -332,27 +332,37 @@
      ( aprod :  ( ai : { j k : Obj I} → (Hom I j k)  → Obj A  ) →  ∀{ i j : Obj I} → IProduct A (Hom I i j) ai )
      ( eqa : {a b : Obj A} → (f g : Hom A a b)  → Equalizer A f g )
           → NTrans I A (K A I (equc prod eqa )) Γ
-limit-ε prod aprod eqa = record {
+limit-ε = {!!}
+
+limit-ε' :
+     ( prod :  ( ai : Obj I → Obj A ) →  IProduct A (Obj I) ai )
+     ( aprod :  ( ai : { j k : Obj I} → (Hom I j k)  → Obj A  ) →  ∀{ i j : Obj I} → IProduct A (Hom I i j) ai )
+     ( eqa : {a b : Obj A} → (f g : Hom A a b)  → Equalizer A f g )
+          → NTrans I A (K A I {!!} ) Γ
+limit-ε' prod aprod eqa = record {
        TMap = λ i → tmap i ; 
-       isNTrans = record { commute = commute1 }
+       isNTrans = record { commute = {!!} }
    } where
-       lim : Obj A
-       lim = equc prod eqa
        p0 : Obj A
        p0 = iprod (prod (FObj Γ))
-       e : Hom A lim p0
-       e = let  open ≈-Reasoning (A) in equalizer ( eqa (id1 A p0 ) ( id1 A p0 ) )
+       Fcod : { j k : Obj I } ( u : Hom I j k ) → Obj A
+       Fcod = λ  u →  FObj Γ (Category.cod I u)
+       equ : ∀{ j k : Obj I } → Equalizer A
+           (iproduct (isIProduct (aprod Fcod {j} {k})) (λ h → A [ FMap Γ h o pi (prod (FObj Γ)) j ] ))
+           (iproduct (isIProduct (aprod Fcod {j} {k})) (λ h → pi (prod (FObj Γ)) k ))
+       equ {j} {k} = let  open ≈-Reasoning (A) in
+           eqa (iproduct (isIProduct (aprod Fcod {j} {k})) (λ h → A [ FMap Γ h o pi (prod (FObj Γ)) j ] ))
+           (iproduct (isIProduct (aprod Fcod {j} {k})) (λ h → pi (prod (FObj Γ)) k ))
+       d : ∀{ j k : Obj I } → Obj A
+       d {j} {k} = equalizer-c (equ {j} {k} )
+       e : ∀{ j k : Obj I } → Hom A d p0
+       e {j} {k} = equalizer (equ {j} {k} )
        proj : (i : Obj I) → Hom A p0 (FObj Γ i)
        proj = pi ( prod  (FObj Γ) )
-       tmap : (i : Obj I) → Hom A (FObj (K A I lim) i) (FObj Γ i)
+       tmap : (i : Obj I) → Hom A (FObj (K A I d) i) (FObj Γ i)
        tmap i = A [ proj i o e ] 
-       e-inv : {i j : Obj I} {f : Hom I i j} → Hom A p0 ( equalizer-c (eqa (A [ FMap Γ f o  proj i ]) ( proj j )) )
-       e-inv = {!!}
-       e-iso : {i j : Obj I} {f : Hom I i j} → A [ A [ equalizer (eqa (A [ FMap Γ f o  proj i ]) ( proj j )) o e-inv ] ≈ id1 A p0 ]
-       e-iso = {!!}
-       Fcod = λ {j} {k} u →  FObj Γ k
        commute1 :  {j k : Obj I} {u : Hom I j k} →
-         A [ A [ FMap Γ u o tmap j ] ≈ A [ tmap k o FMap (K A I lim) u ] ]
+         A [ A [ FMap Γ u o tmap j ] ≈ A [ tmap k o FMap (K A I d) u ] ]
        commute1 {j} {k} {u} =  let  open ≈-Reasoning (A) in begin
               FMap Γ u o tmap j 
          ≈⟨⟩
@@ -362,6 +372,8 @@
          ≈↑⟨ car (car ( pif=q (isIProduct (aprod Fcod )))  ) ⟩
              (( pi (aprod Fcod ) u o iproduct (isIProduct (aprod Fcod)) (FMap Γ)) o  pi (prod (FObj Γ)) j ) o e 
          ≈⟨ {!!} ⟩
+             (( pi (aprod Fcod ) u o iproduct (isIProduct (aprod Fcod)) (FMap Γ)) o  pi (prod (FObj Γ)) j ) o e 
+         ≈⟨ {!!} ⟩
              (( pi (aprod Fcod ) u o iproduct (isIProduct (aprod Fcod)) (λ e → id1 A (FObj Γ (Category.cod I e)))) o  pi (prod (FObj Γ)) k ) o e 
          ≈⟨ car (car ( pif=q (isIProduct (aprod Fcod )))  ) ⟩
               ( id1 A (FObj Γ k) o pi (prod (FObj Γ)) k  ) o e 
@@ -370,10 +382,10 @@
          ≈⟨⟩
               proj k o e 
          ≈↑⟨ idR ⟩
-              (proj k o e ) o id1 A lim
+              (proj k o e ) o id1 A d
          ≈⟨⟩
-              tmap k o FMap (K A I lim) u
-         ∎
+              tmap k o FMap (K A I d) u
+         ∎ 
 
 limit-from :
      ( prod :  ( ai : Obj I → Obj A ) →  IProduct A (Obj I) ai )