Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 10:8022e14fce74

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add constructible set
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 13 May 2019 18:25:38 +0900
parents 5ed16e2d8eb7
children 2df90eb0896c
files zf.agda
diffstat 1 files changed, 78 insertions(+), 46 deletions(-) [+]
line wrap: on
line diff
--- a/zf.agda	Sun May 12 21:18:38 2019 +0900
+++ b/zf.agda	Mon May 13 18:25:38 2019 +0900
@@ -32,7 +32,6 @@
 
 record Func {n m : Level } (ZFSet : Set n) (_≈_ : Rel ZFSet m) : Set (n ⊔ suc m) where
   field
-     Restrict : ZFSet 
      rel : Rel ZFSet m
      dom : ( y : ZFSet ) → ∀ { x : ZFSet } → rel x y
      fun-eq : { x y z : ZFSet } →  ( rel  x  y  ∧ rel  x  z  ) → y ≈ z 
@@ -48,6 +47,8 @@
      (_×_ : ( A B : ZFSet  ) → ZFSet)
      (Union : ( A : ZFSet  ) → ZFSet)
      (Power : ( A : ZFSet  ) → ZFSet)
+     (Select : ( ZFSet → Set m ) → ZFSet )
+     (Replace : ( ZFSet → ZFSet ) → ZFSet )
      (infinite : ZFSet)
        : Set (suc (n ⊔ m)) where
   field
@@ -61,12 +62,10 @@
   A ∈ B = B ∋ A
   _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } → ∀{ A∋x : Set m } → Set m
   _⊆_ A B {x} {A∋x} = B ∋ x
-  Repl : ( ψ : ZFSet → Set m ) → Func ZFSet _≈_ 
-  Repl ψ = record { Restrict = {!!} ; rel = {!!} ; dom = {!!} ; fun-eq = {!!} }
   _∩_ : ( A B : ZFSet  ) → ZFSet
-  A ∩ B = Restrict ( Repl ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) )
+  A ∩ B = Select (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
   _∪_ : ( A B : ZFSet  ) → ZFSet
-  A ∪ B = Restrict ( Repl ( λ x → ( A ∋ x ) ∨ ( B ∋ x ) ) )
+  A ∪ B = Select (  λ x → ( A ∋ x ) ∨ ( B ∋ x )  )
   infixr  200 _∈_
   infixr  230 _∩_ _∪_
   infixr  220 _⊆_ 
@@ -78,14 +77,14 @@
      -- extentionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
      extentionality :  ( A B z  : ZFSet  ) → (( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B
      -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
-     smaller : ZFSet → ZFSet
-     regularity : ∀( x : ZFSet  ) → ¬ (x ≈ ∅) → (  smaller x ∈ x ∧  ( smaller x  ∩ x  ≈ ∅ ) )
+     minimul : ZFSet → ZFSet
+     regularity : ∀( x : ZFSet  ) → ¬ (x ≈ ∅) → (  minimul x ∈ x ∧  ( minimul x  ∩ x  ≈ ∅ ) )
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
      infinity∅ :  ∅ ∈ infinite
-     infinity :  ∀( x : ZFSet  ) → x ∈ infinite →  ( x ∪ Restrict ( Repl ( λ y → x ≈ y ))) ∈ infinite 
+     infinity :  ∀( x : ZFSet  ) → x ∈ infinite →  ( x ∪ Select (  λ y → x ≈ y )) ∈ infinite 
+     selection : { ψ : ZFSet → Set m } → ∀ ( y : ZFSet  ) →  ( y  ∈  Select ψ )  → ψ y
      -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
-     -- this form looks like specification
-     replacement : ( ψ : Func ZFSet _≈_ ) → ∀ ( y : ZFSet  ) →  ( y  ∈  Restrict ψ )  → {!!} -- dom ψ y 
+     replacement : {ψ : ZFSet → ZFSet} → ∀ ( x : ZFSet  ) →  ( ψ x ∈  Replace ψ )  
 
 record ZF {n m : Level } : Set (suc (n ⊔ m)) where
   infixr  210 _×_
@@ -100,46 +99,79 @@
      _×_ : ( A B : ZFSet  ) → ZFSet
      Union : ( A : ZFSet  ) → ZFSet
      Power : ( A : ZFSet  ) → ZFSet
+     Select : ( ZFSet → Set m ) → ZFSet
+     Replace : ( ZFSet → ZFSet ) → ZFSet
      infinite : ZFSet
-     isZF : IsZF ZFSet _∋_ _≈_ ∅ _×_ Union Power infinite 
+     isZF : IsZF ZFSet _∋_ _≈_ ∅ _×_ Union Power Select Replace infinite 
 
-module reguraliry-m {n m : Level } ( zf : ZF {m} {n} ) where
-
-   open import Relation.Nullary
-   open import Data.Empty
-   open import  Relation.Binary.PropositionalEquality
+module zf-exapmle {n m : Level } ( zf : ZF {m} {n} ) where
 
-   _≈_ =  ZF._≈_ zf
-   ZFSet =  ZF.ZFSet 
-   ∅ =  ZF.∅ zf
-   _∩_ =  ( IsZF._∩_  ) (ZF.isZF zf)
-   _∋_ =   ZF._∋_  zf
-   replacement =   IsZF.replacement  ( ZF.isZF zf )
+  _≈_ =  ZF._≈_ zf
+  ZFSet =  ZF.ZFSet  zf
+  Select =  ZF.Select  zf
+  ∅ =  ZF.∅ zf
+  _∩_ =  ( IsZF._∩_  ) (ZF.isZF zf)
+  _∋_ =   ZF._∋_  zf
+  replacement =   IsZF.replacement  ( ZF.isZF zf )
+  selection =   IsZF.selection  ( ZF.isZF zf )
+  minimul =   IsZF.minimul  ( ZF.isZF zf )
+  regularity =   IsZF.regularity  ( ZF.isZF zf )
 
---   russel : ( x : ZFSet zf ) → x ≈ Restrict ( λ x → ¬ ( x ∋ x ) ) → ⊥
---   russel x eq with  x ∋ x 
---   ... | x∋x  with replacement ( λ x → ¬ ( x ∋ x )) x {!!}
---   ... | r1 = {!!}
+  russel : Select ( λ x →  x ∋ x  ) ≈ ∅
+  russel with Select ( λ x →  x ∋ x  ) 
+  ... | s = {!!}
 
+module constructible-set  where
 
-
-
-data Nat : Set zero where
-  Zero : Nat
-  Suc : Nat → Nat
-
-prev : Nat → Nat
-prev (Suc n) = n
-prev Zero = Zero
+  data Nat : Set zero where
+    Zero : Nat
+    Suc : Nat → Nat
+  
+  prev : Nat → Nat
+  prev (Suc n) = n
+  prev Zero = Zero
+  
+  open import  Relation.Binary.PropositionalEquality
+  
+  data Transtive {n : Level }  : ( lv : Nat) → Set n where
+     Φ : {lv : Nat} → Transtive {n} lv
+     T-suc : {lv : Nat} → Transtive {n} lv → Transtive lv
+     ℵ_ :  (lv : Nat) → Transtive (Suc lv)
+  
+  data Constructible {n : Level } {lv : Nat} ( α : Transtive {n} lv )  :  Set (suc n) where
+     fsub : ( ψ : Transtive {n} lv → Set n ) → Constructible  α
+     xself : Transtive {n} lv → Constructible  α
+  
+  record ConstructibleSet {n : Level } : Set (suc n) where
+   field
+      level : Nat
+      α : Transtive {n} level 
+      constructible : Constructible α
+  
+  open ConstructibleSet
+  
+  data _c∋_ {n : Level } {lv lv' : Nat} {α : Transtive {n} lv } {α' : Transtive {n} lv' } :
+        Constructible {n} {lv} α → Constructible {n} {lv'} α' → Set n where
+     xself-fsub  : (ta : Transtive {n} lv ) ( ψ : Transtive {n} lv' → Set n ) → (xself ta ) t∋ ( fsub ψ)  
+     xself-xself :  (ta : Transtive {n} lv ) (tx : Transtive {n} lv' )  → (xself ta ) t∋ ( xself tx) 
+     fsub-fsub :  ( ψ : Transtive {n} lv → Set n ) ( ψ₁ : Transtive {n} lv' → Set n ) →(  fsub ψ )  t∋ ( fsub ψ₁) 
+     fsub-xself  :   ( ψ : Transtive {n} lv → Set n ) (tx : Transtive {n} lv' ) → (fsub ψ )  t∋ ( xself tx) 
 
-open import  Relation.Binary.PropositionalEquality
-
-
-data Transtive {n : Level }  : ( lv : Nat) → Set n where
-   Φ : {lv : Nat} → lv ≡ Zero → Transtive lv
-   T-suc : {lv : Nat} → lv ≡ Zero → Transtive {n} lv → Transtive lv
-   ℵ :  {lv : Nat} → Transtive {n} lv → Transtive (Suc lv)
-
-
-
-
+  _∋_  : {n m : Level} → (ConstructibleSet {n}) → (ConstructibleSet {n} ) → Set m 
+  _∋_ = {!!}
+      
+  
+  Transtive→ZF : {n m : Level } → ZF {suc n} {m}
+  Transtive→ZF {n} {m} = record {
+       ZFSet = ConstructibleSet 
+     ; _∋_ = _∋_
+     ; _≈_ = {!!}
+     ; ∅  = record { level = Zero ; α = Φ ; constructible = xself Φ }
+     ; _×_ = {!!}
+     ; Union = {!!}
+     ; Power = {!!}
+     ; Select = {!!}
+     ; Replace = {!!}
+     ; infinite = {!!}
+     ; isZF = {!!}
+    } where