Mercurial > hg > Members > kono > Proof > category

changeset 503:bd33096c189b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 17 Mar 2017 09:25:46 +0900
parents 01a0dda67a8b
children b489f27317fb
files SetsCompleteness.agda
diffstat 1 files changed, 10 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- 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