# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1593482902 -32400
# Node ID bf01e924e62e7f0c2d5a2f6d5cd993940a1a00a5
# Parent  73a2a8ec9603b855edf89cac181c6151427223d3
...

diff -r 73a2a8ec9603 -r bf01e924e62e OD.agda
--- a/OD.agda	Tue Jun 30 08:55:12 2020 +0900
+++ b/OD.agda	Tue Jun 30 11:08:22 2020 +0900
@@ -222,9 +222,6 @@
 OPwr :  (A :  HOD ) → HOD 
 OPwr  A = Ord ( sup-o A ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) )   
 
--- _⊆_ :  ( A B : HOD   ) → ∀{ x : HOD  } →  Set n
--- _⊆_ A B {x} = A ∋ x →  B ∋ x
-
 record _⊆_ ( A B : HOD   ) : Set (suc n) where
   field 
      incl : { x : HOD } → A ∋ x →  B ∋ x
@@ -250,9 +247,6 @@
      ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
      ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy
 
--- minimal-2 : (x : HOD  ) → ( ne : ¬ (x == od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord  y) )
--- minimal-2 x ne y = contra-position ( ε-induction (λ {z} ind → {!!} ) x ) ( λ p → {!!} )
-
 HOD→ZF : ZF  
 HOD→ZF   = record { 
     ZFSet = HOD 
@@ -271,7 +265,7 @@
     Select : (X : HOD  ) → ((x : HOD  ) → Set n ) → HOD 
     Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
     Replace : HOD  → (HOD  → HOD) → HOD 
-    Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋x → od→ord (ψ (ord→od x)))) ∧ odef (in-codomain X ψ) x } ; odmax = {!!} ; <odmax = {!!} } -- ( λ x → od→ord (ψ x))
+    Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) ∧ odef (in-codomain X ψ) x } ; odmax = {!!} ; <odmax = {!!} } -- ( λ x → od→ord (ψ x))
     _∩_ : ( A B : ZFSet  ) → ZFSet
     A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x }  ; odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y))}
     Union : HOD  → HOD   
@@ -353,12 +347,10 @@
               proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso)  }
             ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
            }
-         sup-od : ( HOD → HOD ) →  HOD 
-         sup-od = {!!}
-         sup-c< :  ( ψ : HOD  →  HOD ) → ∀ {x : HOD } → def (od ( sup-od ψ )) (od→ord ( ψ x ))
-         sup-c< = {!!}
+         sup-c< :  (ψ : HOD → HOD) → {X x : HOD} → X ∋ x  → od→ord (ψ x) o< (sup-o X (λ y X∋y → od→ord (ψ (ord→od y))))
+         sup-c< ψ {X} {x} lt = subst (λ k → od→ord (ψ k) o< _ ) oiso (sup-o< X lt )
          replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
-         replacement← {ψ} X x lt = record { proj1 =  {!!} ; proj2 = lemma } where -- sup-c< ψ {x} 
+         replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {X} {x} lt ; proj2 = lemma } where 
              lemma : odef (in-codomain X ψ) (od→ord (ψ x))
              lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ))
          replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
@@ -401,8 +393,10 @@
               lemma1 :  {a : Ordinal } { t : HOD }
                  → (eq : ZFSubset (Ord a) t =h= t)  → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
               lemma1  {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
+              lemma2 : def (od (Ord a)) (od→ord t)
+              lemma2 = {!!}
               lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (Ord a) (λ x lt → od→ord (ZFSubset (Ord a) (ord→od x)))
-              lemma = {!!} -- sup-o<  
+              lemma = sup-o< _ lemma2
 
          -- 
          -- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first
@@ -425,7 +419,7 @@
               lemma5 {y} eq not = (lemma3 (ord→od y) eq) not
 
          power← :  (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
-         power← A t t→A = record { proj1 = {!!} ; proj2 = lemma2 } where 
+         power← A t t→A = record { proj1 = lemma1 ; proj2 = lemma2 } where 
               a = od→ord A
               lemma0 : {x : HOD} → t ∋ x → Ord a ∋ x
               lemma0 {x} t∋x = c<→o< (t→A t∋x)
@@ -439,14 +433,17 @@
                  ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩
                     t
                  ∎
+              lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t)
+              lemma7 = {!!}
               lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))
               lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A)))  (λ x lt → od→ord (A ∩ (ord→od x))))
-                  lemma4 {!!} -- (sup-o<  {λ x → od→ord (A ∩ x)}  )
+                  lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 )
               lemma2 :  odef (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t)
               lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
                   lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) 
                   lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym oiso) ( ∩-≡ t→A  )))
 
+
          ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a)) 
          ord⊆power a = record { incl = λ {x} lt →  power← (Ord a) x (lemma lt) } where
                 lemma : {x y : HOD} → od→ord x o< osuc a → x ∋ y →  Ord a ∋ y