# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1558247404 -32400
# Node ID bade0a35fdd9bb3c1a88306a88a8a92baf631e99
# Parent  a53ba59c5bdaeb50cea43e5c5a895e854b3c8e03
OD, HOD, TC

diff -r a53ba59c5bda -r bade0a35fdd9 constructible-set.agda
--- a/constructible-set.agda	Sat May 18 22:40:06 2019 +0900
+++ b/constructible-set.agda	Sun May 19 15:30:04 2019 +0900
@@ -25,7 +25,7 @@
 
 open Ordinal
 
-_o<_ : {n : Level} ( x y : Ordinal ) → Set (suc n)
+_o<_ : {n : Level} ( x y : Ordinal ) → Set n
 _o<_ x y =  (lv x < lv y )  ∨ ( ord x d< ord y )
 
 open import Data.Nat.Properties 
@@ -104,6 +104,16 @@
 _o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n)
 a o≤ b  = (a ≡ b)  ∨ ( a o< b )
 
+ordtrans : {n : Level} {x y z : Ordinal {n} }   → x o< y → y o< z → x o< z
+ordtrans {n} {x} {y} {z} (case1 x₁) (case1 x₂) = case1 ( <-trans x₁ x₂ )
+ordtrans {n} {x} {y} {z} (case1 x₁) (case2 x₂) with d<→lv x₂
+... | refl = case1 x₁
+ordtrans {n} {x} {y} {z} (case2 x₁) (case1 x₂) with d<→lv x₁
+... | refl = case1 x₂
+ordtrans {n} {x} {y} {z} (case2 x₁) (case2 x₂) with d<→lv x₁ | d<→lv x₂
+... | refl | refl = case2 ( orddtrans x₁ x₂ )
+
+
 trio< : {n : Level } → Trichotomous {suc n} _≡_  _o<_ 
 trio< a b with <-cmp (lv a) (lv b)
 trio< a b | tri< a₁ ¬b ¬c = tri< (case1  a₁) (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) lemma1 where
@@ -169,80 +179,38 @@
 
 -- X' = { x ∈ X |  ψ  x } ∪ X , Mα = ( ∪ (β < α) Mβ ) '
 
-record ConstructibleSet {n : Level} : Set (suc n) where
-  field
-    α : Ordinal {suc n}
-    constructible : Ordinal {suc n} → Set n
-    -- constructible : (x : Ordinal {suc n} ) → x o< α → Set n
-
-open ConstructibleSet
+-- Ordinal Definable Set
 
-_∋_  : {n : Level} →  (ConstructibleSet {n}) → (ConstructibleSet {n} ) → Set (suc n)
-a ∋ x  = ( α x o< α a ) ∧ constructible a ( α x )
-
-c∅ : {n : Level} → ConstructibleSet
-c∅ {n} = record {α = o∅ ; constructible = λ x → Lift n ⊥ }
-
-record SupR {n m : Level} {S : Set n} ( _≤_ : S → S → Set m  ) (ψ : S → S ) (X : S) : Set ((suc n) ⊔ m)  where
+record OD {n : Level}  : Set (suc n) where
   field
-    sup : S
-    smax  : ∀ { x : S } → x ≤ X  → ψ x ≤ sup 
-    suniq : {max : S} → ( ∀ { x :  S } → x ≤ X  → ψ x ≤ max ) → max ≤ sup 
+    α :  Ordinal {n}
+    def : (x : Ordinal {n} ) → x o< α → Set n
 
-open SupR
+open OD
+open import Data.Unit
 
-record dom-ψ {n m : Level} (X : ConstructibleSet {n}) (ψ : ConstructibleSet {n} → ConstructibleSet {n} ) :  Set (suc (suc n) ⊔ suc m) where
-  field
-    αψ : Ordinal {suc n}
-    inψ : (x : Ordinal {suc n} ) → Set m
-    X∋x : (x : ConstructibleSet {n} ) → inψ (α x) → X ∋ x
-    vψ : (x : Ordinal {suc n} ) → inψ x  → ConstructibleSet {n}
-    cset≡ψ : (x : ConstructibleSet {n} ) → (t : inψ (α x) ) → x ≡ ψ ( vψ (α x) t )
+postulate      -- this is proved by Godel numbering of def
+   _c<_ : {n : Level } → (x y : OD {n} ) → Set n
+   ODpre : {n : Level} →  IsPreorder {suc n} {suc n} {n} _≡_ _c<_ 
 
-open dom-ψ
-
-postulate 
-    ψ→C : {n m : Level} (X : ConstructibleSet {n})  (ψ : ConstructibleSet {n} → ConstructibleSet {n} ) → dom-ψ {n} {m} X ψ
-
-_⊆_ : {n : Level} → ( A B : ConstructibleSet  ) → ∀{ x : ConstructibleSet } →  Set (suc n)
-_⊆_ A B {x} = A ∋ x →  B ∋ x
+-- o∋  : {n : Level} → {A : Ordinal {n}} → (OrdinalDefinable {n} A ) → (x : Ordinal {n} ) → (x o< A) → Set n
+-- o∋ a x x<A  = def a x x<A
 
-suptraverse : {n : Level} → (X : ConstructibleSet {n}) ( max : ConstructibleSet {n}) ( ψ : ConstructibleSet  {n} → ConstructibleSet  {n}) → ConstructibleSet {n}
-suptraverse X max ψ  = {!!} 
-
-Sup : {n : Level } → (ψ : ConstructibleSet → ConstructibleSet )  → (X : ConstructibleSet)  → SupR (λ x a → (α a ≡ α x) ∨ (a ∋ x)) ψ X
-sup  (Sup {n} ψ X ) = suptraverse X (c∅ {n}) ψ 
-smax (Sup ψ X ) = {!!} 
-suniq (Sup ψ X ) = {!!}
-     
-open import Data.Unit
-open SupR
+-- TC u : Transitive Closure of OD u
+--
+--    all elements of u or elements of elements of u, etc...
+--
+-- TC Zero = u
+-- TC (suc n) = ∪ (TC n)
+--
+-- TC u = TC ω u = ∪ ( TC n ) n ∈ ω
+-- 
+--     u ∪ ( ∪ u ) ∪ ( ∪ (∪ u ) ) ....
+--
+--    HOD = {x | TC x ⊆ OD }  ⊆ OD
+-- 
 
-ConstructibleSet→ZF : {n : Level} → ZF {suc n} {suc n}
-ConstructibleSet→ZF {n}  = record { 
-    ZFSet = ConstructibleSet 
-    ; _∋_ = _∋_ 
-    ; _≈_ = _≡_ 
-    ; ∅  = c∅
-    ; _,_ = _,_
-    ; Union = Union
-    ; Power = {!!}
-    ; Select = Select
-    ; Replace = Replace
-    ; infinite = {!!}
-    ; isZF = {!!}
- } where
-    Select : (X : ConstructibleSet {n}) → (ConstructibleSet {n} → Set (suc n)) → ConstructibleSet {n}
-    Select X ψ = record { α = α X ; constructible = λ x →  select x } where 
-       select : Ordinal → Set n
-       select x with  ψ (record { α = x ; constructible = λ x → constructible X x })
-       ... | t = Lift n ⊤
-    Replace : (X : ConstructibleSet {n} ) → (ConstructibleSet → ConstructibleSet) → ConstructibleSet
-    Replace X ψ  = record { α = αψ {n} {suc (suc n)} (ψ→C X ψ)  ; constructible = λ x → inψ (ψ→C X ψ) x }  
-    _,_ : ConstructibleSet {n} → ConstructibleSet → ConstructibleSet
-    a , b  = record { α = maxα (α a) (α b) ; constructible =  a∨b }  where
-       a∨b : Ordinal {suc n} → Set n
-       a∨b x with (x ≡ α a ) ∨ ( x ≡ α b )
-       ... | t = Lift n  ⊤
-    Union : ConstructibleSet → ConstructibleSet
-    Union a = {!!}
+record HOD {n : Level}  : Set (suc n) where
+  field
+      hod : OD {n}
+      tc : ?