changeset 21:6d9fdd1dfa79

add transfinite
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 16 May 2019 16:47:27 +0900
parents 31626f36cd94
children 3da2c00bd24d
files constructible-set.agda
diffstat 1 files changed, 26 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/constructible-set.agda	Thu May 16 16:08:34 2019 +0900
+++ b/constructible-set.agda	Thu May 16 16:47:27 2019 +0900
@@ -35,6 +35,31 @@
 open import Relation.Binary
 open import Relation.Binary.Core
 
+o∅ : Ordinal
+o∅  = record { lv = Zero ; ord = Φ }
+
+TransFinite : ( ψ : Ordinal  → Set n ) 
+  → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } )) 
+  → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ } ) )
+  → ( ∀ (lx : Nat ) → (x : OrdinalD lx )  → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc x } ) )
+  →  ∀ (x : Ordinal)  → ψ x
+TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ } = caseΦ lv
+TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc ord₁ } = caseOSuc lv ord₁
+    ( TransFinite ψ caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
+TransFinite ψ caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁
+
+record SupR (ψ : Ordinal → Ordinal ) : Set n where
+  field
+    sup : Ordinal
+    smax : { x : Ordinal } → ψ x o< sup
+
+open SupR
+
+Sup : (ψ : Ordinal → Ordinal )  → SupR ψ
+sup (Sup ψ) = {!!}
+smax (Sup ψ) = {!!}
+     
+
 ≡→¬d< : {lv : Nat} → {x  : OrdinalD  lv }  → x d< x → ⊥
 ≡→¬d<  {lx} {OSuc y} (s< t) = ≡→¬d< t
 
@@ -145,7 +170,7 @@
     ZFSet = ConstructibleSet 
     ; _∋_ = λ a b → Lift (suc (suc n)) ( a ∋ b )
     ; _≈_ = _≡_ 
-    ; ∅  = record {α = record { lv = Zero ; ord = Φ } ; constructible = λ x → Lift (suc n) ⊥ }
+    ; ∅  = record {α = o∅ ; constructible = λ x → Lift (suc n) ⊥ }
     ; _,_ = _,_
     ; Union = Union
     ; Power = {!!}