--- a/SetsCompleteness.agda	Mon Nov 06 10:10:55 2017 +0900
+++ b/SetsCompleteness.agda	Tue Nov 07 17:12:08 2017 +0900
@@ -26,12 +26,12 @@
 open Σ public
 
 
-SetsProduct :  {  c₂ : Level} → Product ( Sets  {  c₂} )
-SetsProduct { c₂ } = record {
-         product =  λ a b →    Σ a  b
-       ; π1 = λ a b → λ ab → (proj₁ ab)
-       ; π2 = λ a b → λ ab → (proj₂ ab)
-       ; isProduct =  λ a b → record {
+SetsProduct :  {  c₂ : Level} → ( a b : Obj (Sets  {c₂})) → Product ( Sets  {  c₂} ) a b
+SetsProduct { c₂ } a b = record {
+         product =  Σ a b
+       ; π1 = λ ab → (proj₁ ab)
+       ; π2 = λ ab → (proj₂ ab)
+       ; isProduct = record {
               _×_  = λ f g  x →   record { proj₁ = f  x ;  proj₂ =  g  x }     -- ( f x ,  g x )
               ; π1fxg=f = refl
               ; π2fxg=g  = refl