# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1489710346 -32400
# Node ID bd33096c189b1d8e25ed4d28ff1c42c99d55a61f
# Parent  01a0dda67a8bd0a787cf1727ec7f0909c97691cd
on going ...

diff -r 01a0dda67a8b -r bd33096c189b SetsCompleteness.agda
--- a/SetsCompleteness.agda	Thu Mar 16 21:43:10 2017 +0900
+++ b/SetsCompleteness.agda	Fri Mar 17 09:25:46 2017 +0900
@@ -10,16 +10,23 @@
 open import cat-utility
 open import Relation.Binary.Core
 open import Function
-open import Data.Product
+
+record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
+  constructor _,_
+  field
+    proj₁ : A
+    proj₂ : B proj₁
+
+open Σ public
 
 
 SetsProduct :  {  c₂ : Level} → CreateProduct ( Sets  {  c₂} )
 SetsProduct { c₂ } = record { 
-         product =  λ a b →  a × b
+         product =  λ a b →    Σ a  (λ _ → b)
        ; π1 = λ a b → λ ab → (proj₁ ab)
        ; π2 = λ a b → λ ab → (proj₂ ab)
        ; isProduct =  λ a b → record {
-              _×_  = λ f g  x →  ( f x , g x )
+              _×_  = λ f g  x →   record { proj₁ = f  x ;  proj₂ =  g  x }     -- ( f x ,  g x ) 
               ; π1fxg=f = refl
               ; π2fxg=g  = refl
               ; uniqueness = refl