# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1593439754 -32400
# Node ID d5c5d87b72df5c2fa7539fd9b3c4ccc2a4751130
# Parent  b07fc3ef5aab86ff71994a29d4361d28cee0233e
...

diff -r b07fc3ef5aab -r d5c5d87b72df OD.agda
--- a/OD.agda	Mon Jun 29 20:33:19 2020 +0900
+++ b/OD.agda	Mon Jun 29 23:09:14 2020 +0900
@@ -226,7 +226,7 @@
 ZFSubset A x =  record { od = record { def = λ y → odef A y ∧  odef x y } ; odmax = {!!} ; <odmax = {!!} }  --   roughly x = A → Set 
 
 OPwr :  (A :  HOD ) → HOD 
-OPwr  A = Ord ( sup-o {!!} {!!} ) --  ( λ x → od→ord ( ZFSubset A x) ) )   
+OPwr  A = Ord ( sup-o A {!!} ) --  ( λ x → od→ord ( ZFSubset A x) ) )   
 
 -- _⊆_ :  ( A B : HOD   ) → ∀{ x : HOD  } →  Set n
 -- _⊆_ A B {x} = A ∋ x →  B ∋ x
@@ -277,7 +277,7 @@
     Select : (X : HOD  ) → ((x : HOD  ) → Set n ) → HOD 
     Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( ord→od x )) } ; odmax = {!!} ; <odmax = {!!} }
     Replace : HOD  → (HOD  → HOD  ) → HOD 
-    Replace X ψ = record { od = record { def = λ x → (x o< sup-o  {!!} {!!} ) ∧ odef (in-codomain X ψ) x } ; odmax = {!!} ; <odmax = {!!} } -- ( λ x → od→ord (ψ x))
+    Replace X ψ = record { od = record { def = λ x → (x o< sup-o X {!!} ) ∧ 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 = {!!} ; <odmax = {!!} }
     Union : HOD  → HOD   
@@ -403,7 +403,7 @@
               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 ))
-              lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o {!!} {!!} --  (λ x → od→ord (ZFSubset (Ord a) x))
+              lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (Ord a) {!!} --  (λ x → od→ord (ZFSubset (Ord a) x))
               lemma = {!!} -- sup-o<  
 
          -- 
@@ -441,8 +441,8 @@
                  ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩
                     t
                  ∎
-              lemma1 : od→ord t o< sup-o  {!!} {!!} -- (λ x → od→ord (A ∩ x))
-              lemma1 = subst (λ k → od→ord k o< sup-o  {!!} {!!}) --  (λ x → od→ord (A ∩ x)))
+              lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) {!!} -- (λ x → od→ord (A ∩ x))
+              lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A)))  {!!}) --  (λ x → od→ord (A ∩ x)))
                   lemma4 {!!} -- (sup-o<  {λ x → od→ord (A ∩ x)}  )
               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