# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1379679708 -32400
# Node ID 78ce12f8e6b613c84fe6b8672189ff133ff43415
# Parent  c1b3193097ce6577fc32fac0b9ea6afe9d624541
pullback done

diff -r c1b3193097ce -r 78ce12f8e6b6 cat-utility.agda
--- a/cat-utility.agda	Fri Sep 20 19:03:57 2013 +0900
+++ b/cat-utility.agda	Fri Sep 20 21:21:48 2013 +0900
@@ -152,12 +152,12 @@
         -- 
         -- Product
         --
-        --
-        --                 
-        --
-        --
-        --
-        --
+        --                c
+        --        f       |        g
+        --                |f×g
+        --                v
+        --    a <-------- ab ----------> b
+        --         π1            π2
 
 
         record Product { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  (a b ab : Obj A) 
@@ -169,6 +169,7 @@
               π1fxg=f : {c : Obj A} { f : Hom A c a } → { g : Hom A c b } → A [ A [ π1  o ( f × g )  ] ≈  f ]
               π2fxg=g : {c : Obj A} { f : Hom A c a } → { g : Hom A c b } → A [ A [ π2  o ( f × g )  ] ≈  g ]
               uniqueness : {c : Obj A} { h : Hom A c ab }  → A [  ( A [ π1  o h  ] ) × ( A [ π2  o h  ] ) ≈  h ]
+              ×-cong : {c : Obj A} { f f' : Hom A c a } → { g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ f × g ≈ f' × g' ] 
            axb : Obj A
            axb = ab
 
diff -r c1b3193097ce -r 78ce12f8e6b6 pullback.agda
--- a/pullback.agda	Fri Sep 20 19:03:57 2013 +0900
+++ b/pullback.agda	Fri Sep 20 21:21:48 2013 +0900
@@ -12,7 +12,7 @@
 open import cat-utility
 
 -- 
--- Pullback
+-- Pullback from equalizer and product
 --         f
 --     a -------> c
 --     ^          ^                 
@@ -21,9 +21,10 @@
 --    ab -------> b
 --     ^   π2
 --     |
---     | equalizer (f π1) (g π1) = ( π1' × π2' )
---     d   
---
+--     | e = equalizer (f π1) (g π1)  
+--     |
+--     d <------------------ d'
+--         k (π1' × π2' )
 
 open Equalizer
 open Product
@@ -105,14 +106,23 @@
         {eq1 : A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} →
         {eq2 : A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]} →
         A [ p1 eq ≈ p' ]
-      uniqueness1 {d'} p' {π1'} {π2'} {eq} {eq1} = let open ≈-Reasoning (A) in
+      uniqueness1 {d'} p' {π1'} {π2'} {eq} {eq1} {eq2} = let open ≈-Reasoning (A) in
              begin
                  p1 eq
              ≈⟨⟩
                  k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod  π1'  π2' ) (lemma1 eq)
-             ≈⟨ Equalizer.uniqueness (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e}) {!!} ⟩
-                 {!!} o {!!}
-             ≈⟨ {!!} ⟩
+             ≈⟨ Equalizer.uniqueness (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e}) ( begin
+                 e o p'
+             ≈⟨⟩
+                  equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p'
+             ≈↑⟨ Product.uniqueness prod ⟩
+                (prod × (  π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p') ) ( π2 o (equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p'))
+             ≈⟨ ×-cong prod (assoc) (assoc) ⟩
+                 (prod × (A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]))
+                         (A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]) 
+             ≈⟨ ×-cong prod eq1 eq2 ⟩
+                ((prod × π1') π2')
+             ∎ ) ⟩
                  p'
              ∎