--- a/pullback.agda	Mon Oct 30 18:18:36 2017 +0900
+++ b/pullback.agda	Thu Nov 02 09:00:01 2017 +0900
@@ -28,14 +28,14 @@
 
 open Equalizer
 open IsEqualizer
-open Product
+open IsProduct
 open Pullback
 
 pullback-from :  (a b c ab d : Obj A)
       ( f : Hom A a c )    ( g : Hom A b c )
       ( π1 : Hom A ab a )  ( π2 : Hom A ab b ) ( e : Hom A d ab )
       ( eqa : {a b c : Obj A} → (f g : Hom A a b)  → {e : Hom A c a }  → IsEqualizer A e f g )
-      ( prod : Product A a b ab π1 π2 ) → Pullback A a b c d f g
+      ( prod : IsProduct A a b ab π1 π2 ) → Pullback A a b c d f g
           ( 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 ab d f g π1 π2 e eqa prod =  record {
@@ -118,7 +118,7 @@
                  e o p'
              ≈⟨⟩
                   equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p'
-             ≈↑⟨ Product.uniqueness prod ⟩
+             ≈↑⟨ IsProduct.uniqueness prod ⟩
                 (prod × (  π1 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p') ) ( π2 o (equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p'))
              ≈⟨ ×-cong prod (assoc) (assoc) ⟩
                  (prod × (A [ A [ π1 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]))
@@ -289,13 +289,13 @@
         ∎
 
 
-lemma-p0 :   (a b ab : Obj A) ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( prod : Product A a b ab π1 π2 ) →
+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
              _×_ prod π1 π2
          ≈↑⟨ ×-cong prod idR idR ⟩
              _×_ prod (A [ π1 o id1 A ab ]) (A [ π2 o id1 A ab ])
-         ≈⟨ Product.uniqueness prod ⟩
+         ≈⟨ IsProduct.uniqueness prod ⟩
              id1 A ab 
          ∎