# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1561860214 -32400
# Node ID 4d24345132288e34bb2d69117f94e7e46a4071b6
# Parent  453ef0d4ee8a3e252c5bcc7cc6e476feb2f74e81
...

diff -r 453ef0d4ee8a -r 4d2434513228 HOD.agda
--- a/HOD.agda	Thu Jun 27 19:26:45 2019 +0900
+++ b/HOD.agda	Sun Jun 30 11:03:34 2019 +0900
@@ -129,11 +129,6 @@
 transitive  {n} {z} {y} {x} z∋y x∋y  with  ordtrans ( c<→o< {suc n} {x} {y} x∋y ) (  c<→o< {suc n} {y} {z} z∋y ) 
 ... | t = otrans z z∋y (c<→o< {suc n} {x} {y} x∋y ) 
 
-record Minimumo {n : Level } (x : Ordinal {n}) : Set (suc n) where
-  field
-     mino : Ordinal {n}
-     min<x :  mino o< x
-
 ∅5 : {n : Level} →  { x : Ordinal {n} }  → ¬ ( x  ≡ o∅ {n} ) → o∅ {n} o< x
 ∅5 {n} {record { lv = Zero ; ord = (Φ .0) }} not = ⊥-elim (not refl) 
 ∅5 {n} {record { lv = Zero ; ord = (OSuc .0 ord) }} not = case2 Φ<
@@ -216,7 +211,7 @@
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
 
 csuc :  {n : Level} →  HOD {suc n} → HOD {suc n}
-csuc x = ord→od ( osuc ( od→ord x ))
+csuc x = Ord ( osuc ( od→ord x ))
 
 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
 
@@ -229,12 +224,40 @@
 Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )  
 
 -- Constructible Set on α
+-- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y <  od→ord x } 
+-- L (Φ 0) = Φ
+-- L (OSuc lv n) = { Def ( L n )  } 
+-- L (Φ (Suc n)) = Union (L α) (α < Φ (Suc n) )
 L : {n : Level} → (α : Ordinal {suc n}) → HOD {suc n}
 L {n}  record { lv = Zero ; ord = (Φ .0) } = od∅
 L {n}  record { lv = lx ; ord = (OSuc lv ox) } = Def ( L {n} ( record { lv = lx ; ord = ox } ) ) 
 L {n}  record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
     cseq ( Ord (od→ord (L {n}  (record { lv = lx ; ord = Φ lx }))))
 
+LS :  {n : Level} → {la : Nat } → {oa : OrdinalD {suc n} la }
+        → L {n} (record { lv = la; ord = OSuc la oa })  ∋ L {n} (record { lv = la; ord = oa })
+LS {n} {la} {oa} = {!!} where
+      lemma0 :  {n : Level} → (ox : Ordinal {suc n}) →  od→ord (ZFSubset (Ord ox) (ord→od ox)) ≡ ox
+      lemma0 = {!!}
+      lemma :   {n : Level} → (ox : Ordinal {suc n}) → ox o<  sup-o ( λ x → od→ord ( ZFSubset (Ord ox) (ord→od x )))
+      lemma {n} ox =  o<-subst {suc n} {_} {_} {ox} {sup-o ( λ x → od→ord ( ZFSubset (Ord ox) (ord→od x )))}
+          (sup-o< {suc n} {λ x → od→ord ( ZFSubset (Ord ox) (ord→od x ))} {ox} ) (lemma0 ox) refl
+
+L0 :  {n : Level} → {la : Nat } → {oa : OrdinalD {suc n} (Suc la) }{ob : OrdinalD {suc n} la }
+   → L (record { lv = Suc la; ord = oa })  ∋ L (record { lv = la; ord = ob })
+L0 = {!!}
+
+L1 :  {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : HOD {suc n})  → L α ∋ x → L β ∋ x 
+L1 {n} record { lv = .0 ; ord = (Φ .0) } record { lv = .(Suc _) ; ord = ord₁ } (case1 (s≤s z≤n)) x (case1 ())
+L1 {n} record { lv = .0 ; ord = (Φ .0) } record { lv = .(Suc _) ; ord = ord₁ } (case1 (s≤s z≤n)) x (case2 ())
+L1 {n} record { lv = .0 ; ord = (OSuc .0 ord₂) } record { lv = (Suc lx) ; ord = ord₁ } (case1 (s≤s z≤n)) x α∋x = lemma α∋x where
+   lemma : (od→ord x) o< (sup-o (λ x₁ → od→ord (ZFSubset (L (record { lv = 0 ; ord = ord₂ })) (ord→od x₁))))
+       → L (record { lv = Suc lx ; ord = ord₁ }) ∋ x
+   lemma lt = {!!}
+L1 {n} record { lv = (Suc _) ; ord = ord₂ } record { lv = (Suc (Suc _)) ; ord = ord₁ } (case1 (s≤s (s≤s x₁))) x α∋x = {!!}
+L1 {n} record { lv = lx ; ord = (Φ lx) } record { lv = lx ; ord = (OSuc lx _) } (case2 Φ<) x α∋x = {!!}
+L1 {n} record { lv = lx ; ord = (OSuc lx _) } record { lv = lx ; ord = (OSuc lx _) } (case2 (s< x₁)) x α∋x = {!!}
+
 omega : { n : Level } → Ordinal {n}
 omega = record { lv = Suc Zero ; ord = Φ 1 }
 
@@ -301,8 +324,6 @@
        ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
        ;   replacement = replacement
      } where
-         open _∧_ 
-         open Minimumo
          pair : (A B : HOD {suc n} ) → ((A , B) ∋ A) ∧  ((A , B) ∋ B)
          proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B)
          proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B)
@@ -324,7 +345,7 @@
               lemma-t : csuc minsup ∋ t
               lemma-t = {!!} -- o<→c< (o<-subst (sup-lb (o<-subst (c<→o< P∋t) refl diso )) refl refl ) 
               lemma-s : ZFSubset A ( Ord ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x)))))  ∋ x
-              lemma-s with osuc-≡< ( o<-subst (c<→o< lemma-t ) refl diso  )
+              lemma-s with osuc-≡< ( o<-subst (c<→o< lemma-t ) refl (sym ord-Ord) )
               lemma-s | case1 eq = {!!}
               lemma-s | case2 lt = transitive {n} {minsup} {t} {x} {!!} t∋x
          -- 
@@ -348,7 +369,7 @@
          union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z ))
          union→ X z u xx | tri< a ¬b ¬c with  osuc-< a (c<→o< (proj2 xx))
          union→ X z u xx | tri< a ¬b ¬c | ()
-         union→ X z u xx | tri≈ ¬a b ¬c = def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (proj1 xx) refl b where
+         union→ X z u xx | tri≈ ¬a b ¬c = def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (proj1 xx) refl b 
          union→ X z u xx | tri> ¬a ¬b c = otrans X (proj1 xx) c
          union← :  (X z : HOD) (X∋z : Union X ∋ z) → (X ∋  union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z )
          union← X z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where
diff -r 453ef0d4ee8a -r 4d2434513228 ordinal-definable.agda
--- a/ordinal-definable.agda	Thu Jun 27 19:26:45 2019 +0900
+++ b/ordinal-definable.agda	Sun Jun 30 11:03:34 2019 +0900
@@ -121,11 +121,6 @@
    lemma0 :  def ( ord→od ( od→ord z )) ( od→ord x) →  def z (od→ord x)
    lemma0 dz  = def-subst {suc n} { ord→od ( od→ord z )} { od→ord x} dz (oiso)  refl
 
-record Minimumo {n : Level } (x : Ordinal {n}) : Set (suc n) where
-  field
-     mino : Ordinal {n}
-     min<x :  mino o< x
-
 ∅5 : {n : Level} →  { x : Ordinal {n} }  → ¬ ( x  ≡ o∅ {n} ) → o∅ {n} o< x
 ∅5 {n} {record { lv = Zero ; ord = (Φ .0) }} not = ⊥-elim (not refl) 
 ∅5 {n} {record { lv = Zero ; ord = (OSuc .0 ord) }} not = case2 Φ<
@@ -353,8 +348,6 @@
        ;   selection = λ {X} {ψ} {y} → selection {ψ} {X} {y} 
        ;   replacement = replacement
      } where
-         open _∧_ 
-         open Minimumo
          pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧  ((A , B) ∋ B)
          proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B)
          proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B)