# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1557279301 -32400
# Node ID e8adb0eb4243b62c0a0c3490a271063dd5e5f052

Set theory in Agda

diff -r 000000000000 -r e8adb0eb4243 set-of-agda.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/set-of-agda.agda	Wed May 08 10:35:01 2019 +0900
@@ -0,0 +1,40 @@
+module set-of-agda where
+
+open import Level
+open import Relation.Binary.HeterogeneousEquality
+
+infix  50 _∧_
+
+record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   constructor _×_
+   field 
+      proj1 : A
+      proj2 : B
+
+open _∧_
+
+infix  50 _∨_
+
+data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   case1 : A → A ∨ B
+   case2 : B → A ∨ B
+
+infix  60 _∋_ _∈_
+
+_∋_  : {n : Level} ( A : Set n ) → {a : A}  → { B : Set n} → ( b : B ) →  Set n
+_∋_ A {a} {B} b = a ≅ b
+
+_∈_  : {n : Level} { B : Set n } →  (b : B ) → ( A : Set n )  → {a : A}   →  Set n
+_∈_ {_} {B} b A {a} = b ≅ a
+
+infix  40 _⇔_
+
+_⇔_ : {n : Level} (A  B : Set n)  → Set  n 
+A ⇔ B = ( ∀ {x : A } → x ∈ B  ) ∧  ( ∀ {x : B } → x ∈ A )
+
+-- Axiom of extentionality
+-- ∀ x ∀ y [ ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) ]
+
+set-extentionality : {n : Level } {x y : Set n }  → { z : x } → ( z ∈ x ⇔ z ∈ y ) → ∀ (w : Set (suc n))  → ( x ∈ w ⇔ y ∈ w ) 
+set-extentionality = {!!}
+