diff zf.agda @ 269:30e419a2be24

disjunction and conjunction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 06 Oct 2019 16:42:42 +0900
parents 63df67b6281c
children 29a85a427ed2
line wrap: on
line diff
--- a/zf.agda	Mon Sep 30 21:22:07 2019 +0900
+++ b/zf.agda	Sun Oct 06 16:42:42 2019 +0900
@@ -35,7 +35,7 @@
   _∩_ : ( A B : ZFSet  ) → ZFSet
   A ∩ B = Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
   _∪_ : ( A B : ZFSet  ) → ZFSet
-  A ∪ B = Union (A , B)    -- Select A (  λ x → ( A ∋ x ) ∨ ( B ∋ x )  ) is easier
+  A ∪ B = Union (A , B)    
   {_} : ZFSet → ZFSet
   { x } = ( x ,  x )
   infixr  200 _∈_