# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1593423116 -32400
# Node ID 2c111bfcc89ad6c9ea8a6739c7228a631c8deab3
# Parent  7963b76df6e13a1703759ef7b56d546370c77275
HOD using <maxod

diff -r 7963b76df6e1 -r 2c111bfcc89a OD.agda
--- a/OD.agda	Mon Jun 29 17:56:06 2020 +0900
+++ b/OD.agda	Mon Jun 29 18:31:56 2020 +0900
@@ -77,7 +77,8 @@
 record HOD : Set (suc n) where
   field
     od : OD
-    ¬odmax : ¬ (od ≡ Ords)
+    odmax : Ordinal
+    <odmax : {x : Ordinal} → def od x → x o< odmax
 
 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
   field
@@ -89,12 +90,9 @@
 
 open HOD
 
--- HOD→OD : {x : Ordinal} → HOD x → OD
--- HOD→OD hod = record { def = hdef {!!} }
-
 record ODAxiom : Set (suc n) where      
-  -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
  field
+  -- HOD is isomorphic to Ordinal (by means of Goedel number)
   od→ord : HOD  → Ordinal 
   ord→od : Ordinal  → HOD  
   c<→o<  :  {x y : HOD  }   → def (od y) ( od→ord x ) → od→ord x o< od→ord y
@@ -114,22 +112,23 @@
 -- maxod : {x : OD} → od→ord x o< od→ord Ords
 -- maxod {x} = c<→o< OneObj
 
--- we have to avoid this contradiction
-
+-- we have not this contradiction
 -- bad-bad : ⊥
--- bad-bad = osuc-< <-osuc (c<→o< { record { def = λ x → One }} OneObj)
+-- bad-bad = osuc-< <-osuc (c<→o< { record { od = record { def = λ x → One };  <odmax = {!!} } } OneObj)
 
 -- Ordinal in OD ( and ZFSet ) Transitive Set
 Ord : ( a : Ordinal  ) → HOD 
-Ord  a = record { od = record { def = λ y → y o< a } ; ¬odmax = ? }
+Ord  a = record { od = record { def = λ y → y o< a } ; odmax = a ; <odmax = lemma } where
+   lemma :  {x : Ordinal} → x o< a → x o< a
+   lemma {x} lt = lt
 
 od∅ : HOD  
 od∅  = Ord o∅ 
 
 sup-o  :  ( HOD → Ordinal ) →  Ordinal 
-sup-o  = ?
+sup-o  = {!!}
 sup-o< :  { ψ : HOD →  Ordinal } → ∀ {x : HOD } → ψ x  o<  sup-o ψ 
-sup-o< = ?
+sup-o< = {!!}
 
 odef : HOD → Ordinal → Set n
 odef A x = def ( od A ) x
@@ -148,7 +147,7 @@
 x c< a = a ∋ x 
 
 cseq : {n : Level} →  HOD  →  HOD 
-cseq x = record { od = record { def = λ y → odef x (osuc y) } ; ¬odmax = ? } where
+cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = {!!} ; <odmax = {!!} } where
 
 odef-subst :  {Z : HOD } {X : Ordinal  }{z : HOD } {x : Ordinal  }→ odef Z X → Z ≡ z  →  X ≡ x  →  odef z x
 odef-subst df refl refl = df
@@ -216,18 +215,18 @@
 is-o∅ x | tri> ¬a ¬b c = no ¬b
 
 _,_ : HOD  → HOD  → HOD 
-x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; ¬odmax = ? }  --  Ord (omax (od→ord x) (od→ord y))
+x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = {!!} ; <odmax = {!!} }  --  Ord (omax (od→ord x) (od→ord y))
 
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
 
 in-codomain : (X : HOD  ) → ( ψ : HOD  → HOD  ) → HOD 
-in-codomain  X ψ = record { od = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ( x ≡ od→ord (ψ (ord→od y )))))  } ; ¬odmax = ? }
+in-codomain  X ψ = record { od = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ( x ≡ od→ord (ψ (ord→od y )))))  } ; odmax = {!!} ; <odmax = {!!} }
 
 -- Power Set of X ( or constructible by λ y → odef X (od→ord y )
 
 ZFSubset : (A x : HOD  ) → HOD 
-ZFSubset A x =  record { od = record { def = λ y → odef A y ∧  odef x y } ; ¬odmax = ? }  --   roughly x = A → Set 
+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) ) )   
@@ -279,13 +278,13 @@
  } where
     ZFSet = HOD             -- is less than Ords because of maxod
     Select : (X : HOD  ) → ((x : HOD  ) → Set n ) → HOD 
-    Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( ord→od x )) } ; ¬odmax = ? }
+    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  ( λ x → od→ord (ψ x))) ∧ odef (in-codomain X ψ) x } ; ¬odmax = ? }
+    Replace X ψ = record { od = record { def = λ x → (x o< sup-o  ( λ x → od→ord (ψ x))) ∧ odef (in-codomain X ψ) x } ; odmax = {!!} ; <odmax = {!!} }
     _∩_ : ( A B : ZFSet  ) → ZFSet
-    A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x }  ; ¬odmax = ? }
+    A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x }  ; odmax = {!!} ; <odmax = {!!} }
     Union : HOD  → HOD   
-    Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x)))  } ; ¬odmax = ? }
+    Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x)))  } ; odmax = {!!} ; <odmax = {!!} }
     _∈_ : ( A B : ZFSet  ) → Set n
     A ∈ B = B ∋ A
     Power : HOD  → HOD 
@@ -299,7 +298,7 @@
                 infinite-d  (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
 
     infinite : HOD 
-    infinite = record { od = record { def = λ x → infinite-d x } ; ¬odmax = ? }
+    infinite = record { od = record { def = λ x → infinite-d x } ; odmax = {!!} ; <odmax = {!!} }
 
     _=h=_ : (x y : HOD) → Set n
     x =h= y  = od x == od y
@@ -364,7 +363,7 @@
             ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
            }
          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 =  {!!} ; proj2 = lemma } where -- sup-c< ψ {x} 
              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))