# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1557992847 -32400
# Node ID 6d9fdd1dfa79dd7cd5990da1f6437e3f883c814c
# Parent  31626f36cd94a502376c5e5c87c2f0006bab151e
add transfinite

diff -r 31626f36cd94 -r 6d9fdd1dfa79 constructible-set.agda
--- 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 = {!!}