### changeset 334:ba3ebb9a16c6release

HOD
author Shinji KONO Sun, 05 Jul 2020 16:59:13 +0900 9f926b2210bc (current diff) 214a087c78a5 (diff) aa03b9c289c0 .hgtags 10 files changed, 672 insertions(+), 402 deletions(-) [+]
line wrap: on
line diff
```--- a/BAlgbra.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/BAlgbra.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -19,60 +19,66 @@
open OD O
open OD.OD
open ODAxiom odAxiom
+open HOD

open _∧_
open _∨_
open Bool

-_∩_ : ( A B : OD  ) → OD
-A ∩ B = record { def = λ x → def A x ∧ def B x }
-
-_∪_ : ( A B : OD  ) → OD
-A ∪ B = record { def = λ x → def A x ∨ def B x }
+_∩_ : ( A B : HOD  ) → HOD
+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)) }

-_＼_ : ( A B : OD  ) → OD
-A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) }
+_∪_ : ( A B : HOD  ) → HOD
+A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ;
+    odmax = omax (odmax A) (odmax B) ; <odmax = lemma } where
+      lemma :  {y : Ordinal} → odef A y ∨ odef B y → y o< omax (odmax A) (odmax B)
+      lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _)
+      lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _)

-∪-Union : { A B : OD } → Union (A , B) ≡ ( A ∪ B )
+_＼_ : ( A B : HOD  ) → HOD
+A ＼ B = record { od = record { def = λ x → odef A x ∧ ( ¬ ( odef B x ) ) }; odmax = odmax A ; <odmax = λ y → <odmax A (proj1 y) }
+
+∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B )
∪-Union {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } )  where
-    lemma1 :  {x : Ordinal} → def (Union (A , B)) x → def (A ∪ B) x
+    lemma1 :  {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x
lemma1 {x} lt = lemma3 lt where
-        lemma4 : {y : Ordinal} → def (A , B) y ∧ def (ord→od y) x → ¬ (¬ ( def A x ∨ def B x) )
+        lemma4 : {y : Ordinal} → odef (A , B) y ∧ odef (ord→od y) x → ¬ (¬ ( odef A x ∨ odef B x) )
lemma4 {y} z with proj1 z
-        lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → def k x ) oiso (proj2 z)) )
-        lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → def k x ) oiso (proj2 z)) )
-        lemma3 : (((u : Ordinals.ord O) → ¬ def (A , B) u ∧ def (ord→od u) x) → ⊥) → def (A ∪ B) x
+        lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → odef k x ) oiso (proj2 z)) )
+        lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → odef k x ) oiso (proj2 z)) )
+        lemma3 : (((u : Ordinals.ord O) → ¬ odef (A , B) u ∧ odef (ord→od u) x) → ⊥) → odef (A ∪ B) x
lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not)   -- choice
-    lemma2 :  {x : Ordinal} → def (A ∪ B) x → def (Union (A , B)) x
-    lemma2 {x} (case1 A∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A
-       (record { proj1 = case1 refl ; proj2 = subst (λ k → def A k) (sym diso) A∋x}))
-    lemma2 {x} (case2 B∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B
-       (record { proj1 = case2 refl ; proj2 = subst (λ k → def B k) (sym diso) B∋x}))
+    lemma2 :  {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x
+    lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A
+       (record { proj1 = case1 refl ; proj2 = subst (λ k → odef A k) (sym diso) A∋x}))
+    lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B
+       (record { proj1 = case2 refl ; proj2 = subst (λ k → odef B k) (sym diso) B∋x}))

-∩-Select : { A B : OD } →  Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  ) ≡ ( A ∩ B )
+∩-Select : { A B : HOD } →  Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  ) ≡ ( A ∩ B )
∩-Select {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } ) where
-    lemma1 : {x : Ordinal} → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → def (A ∩ B) x
-    lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → def B k ) diso (proj2 (proj2 lt)) }
-    lemma2 : {x : Ordinal} → def (A ∩ B) x → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x
+    lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x
+    lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → odef B k ) diso (proj2 (proj2 lt)) }
+    lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x
lemma2 {x} lt = record { proj1 = proj1 lt ; proj2 =
-        record { proj1 = subst (λ k → def A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → def B k ) (sym diso) (proj2 lt) } }
+        record { proj1 = subst (λ k → odef A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → odef B k ) (sym diso) (proj2 lt) } }

-dist-ord : {p q r : OD } → p ∩ ( q ∪ r ) ≡   ( p ∩ q ) ∪ ( p ∩ r )
+dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡   ( p ∩ q ) ∪ ( p ∩ r )
dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
-    lemma1 :  {x : Ordinal} → def (p ∩ (q ∪ r)) x → def ((p ∩ q) ∪ (p ∩ r)) x
+    lemma1 :  {x : Ordinal} → odef (p ∩ (q ∪ r)) x → odef ((p ∩ q) ∪ (p ∩ r)) x
lemma1 {x} lt with proj2 lt
lemma1 {x} lt | case1 q∋x = case1 ( record { proj1 = proj1 lt ; proj2 = q∋x } )
lemma1 {x} lt | case2 r∋x = case2 ( record { proj1 = proj1 lt ; proj2 = r∋x } )
-    lemma2  : {x : Ordinal} → def ((p ∩ q) ∪ (p ∩ r)) x → def (p ∩ (q ∪ r)) x
+    lemma2  : {x : Ordinal} → odef ((p ∩ q) ∪ (p ∩ r)) x → odef (p ∩ (q ∪ r)) x
lemma2 {x} (case1 p∩q) = record { proj1 = proj1 p∩q ; proj2 = case1 (proj2 p∩q ) }
lemma2 {x} (case2 p∩r) = record { proj1 = proj1 p∩r ; proj2 = case2 (proj2 p∩r ) }

-dist-ord2 : {p q r : OD } → p ∪ ( q ∩ r ) ≡   ( p ∪ q ) ∩ ( p ∪ r )
+dist-ord2 : {p q r : HOD } → p ∪ ( q ∩ r ) ≡   ( p ∪ q ) ∩ ( p ∪ r )
dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
-    lemma1 : {x : Ordinal} → def (p ∪ (q ∩ r)) x → def ((p ∪ q) ∩ (p ∪ r)) x
+    lemma1 : {x : Ordinal} → odef (p ∪ (q ∩ r)) x → odef ((p ∪ q) ∩ (p ∪ r)) x
lemma1 {x} (case1 cp) = record { proj1 = case1 cp ; proj2 = case1 cp }
lemma1 {x} (case2 cqr) = record { proj1 = case2 (proj1 cqr) ; proj2 = case2 (proj2 cqr) }
-    lemma2 : {x : Ordinal} → def ((p ∪ q) ∩ (p ∪ r)) x → def (p ∪ (q ∩ r)) x
+    lemma2 : {x : Ordinal} → odef ((p ∪ q) ∩ (p ∪ r)) x → odef (p ∪ (q ∩ r)) x
lemma2 {x} lt with proj1 lt | proj2 lt
lemma2 {x} lt | case1 cp | _ = case1 cp
lemma2 {x} lt | _ | case1 cp = case1 cp ```
```--- a/LEMC.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/LEMC.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -23,38 +23,42 @@

open import zfc

---- With assuption of OD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
+--- With assuption of HOD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
---
-record choiced  ( X : OD) : Set (suc n) where
+record choiced  ( X : HOD) : Set (suc n) where
field
-     a-choice : OD
+     a-choice : HOD
is-in : X ∋ a-choice

+open HOD
+_=h=_ : (x y : HOD) → Set n
+x =h= y  = od x == od y
+
open choiced

OD→ZFC : ZFC
OD→ZFC   = record {
-    ZFSet = OD
+    ZFSet = HOD
; _∋_ = _∋_
-    ; _≈_ = _==_
+    ; _≈_ = _=h=_
; ∅  = od∅
; Select = Select
; isZFC = isZFC
} where
-- infixr  200 _∈_
-- infixr  230 _∩_ _∪_
-    isZFC : IsZFC (OD )  _∋_  _==_ od∅ Select
+    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ Select
isZFC = record {
choice-func = λ A {X} not A∋X → a-choice (choice-func X not );
choice = λ A {X} A∋X not → is-in (choice-func X not)
} where
-         choice-func :  (X : OD ) → ¬ ( X == od∅ ) → choiced X
+         choice-func :  (X : HOD ) → ¬ ( X =h= od∅ ) → choiced X
choice-func  X not = have_to_find where
ψ : ( ox : Ordinal ) → Set (suc n)
-                 ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ def X x )) ∨ choiced X
+                 ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ odef X x )) ∨ choiced X
lemma-ord : ( ox : Ordinal  ) → ψ ox
-                 lemma-ord  ox = TransFinite {ψ} induction ox where
-                    ∋-p : (A x : OD ) → Dec ( A ∋ x )
+                 lemma-ord  ox = TransFinite1 {ψ} induction ox where
+                    ∋-p : (A x : HOD ) → Dec ( A ∋ x )
∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM
∋-p A x | case1 (lift t)  = yes t
∋-p A x | case2 t  = no (λ x → t (lift x ))
@@ -71,59 +75,61 @@
induction x prev with ∋-p X ( ord→od x)
... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } )
... | no ¬p = lemma where
-                         lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X
+                         lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced X
lemma1 y with ∋-p X (ord→od y)
lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } )
-                         lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) )
-                         lemma :  ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X
+                         lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → odef X k ) (sym diso) y<X ) )
+                         lemma :  ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced X
lemma = ∀-imply-or lemma1
have_to_find : choiced X
have_to_find = dont-or  (lemma-ord (od→ord X )) ¬¬X∋x where
-                     ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥)
+                     ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → odef X x → ⊥)
¬¬X∋x nn = not record {
-                            eq→ = λ {x} lt → ⊥-elim  (nn x (def→o< lt) lt)
+                            eq→ = λ {x} lt → ⊥-elim  (nn x (odef→o< lt) lt)
; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
}
-         record Minimal (x : OD)  : Set (suc n) where
+         record Minimal (x : HOD)  : Set (suc n) where
field
-               min : OD
+               min : HOD
x∋min :   x ∋ min
-               min-empty :  (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
+               min-empty :  (y : HOD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
open Minimal
open _∧_
--
--  from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only
--
-         induction : {x : OD} → ({y : OD} → x ∋ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u )
-              →  (u : OD ) → (u∋x : u ∋ x) → Minimal u
-         induction {x} prev u u∋x with p∨¬p ((y : OD) → ¬ (x ∋ y) ∧ (u ∋ y))
+         induction : {x : HOD} → ({y : HOD} → x ∋ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u )
+              →  (u : HOD ) → (u∋x : u ∋ x) → Minimal u
+         induction {x} prev u u∋x with p∨¬p ((y : HOD) → ¬ (x ∋ y) ∧ (u ∋ y))
... | case1 P =
record { min = x
;     x∋min = u∋x
;     min-empty = P
}
... | case2 NP =  min2 where
-              p : OD
-              p  = record { def = λ y1 → def x  y1 ∧ def u y1 }
-              np : ¬ (p == od∅)
-              np p∅ =  NP (λ y p∋y → ∅< p∋y p∅ )
+              p : HOD
+              p  = record { od = record { def = λ y1 → odef x  y1 ∧ odef u y1 } ; odmax = omin (odmax x) (odmax u) ; <odmax = lemma } where
+                 lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u)
+                 lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt))
+              np : ¬ (p =h= od∅)
+              np p∅ =  NP (λ y p∋y → ∅< {p} {_} p∋y p∅ )
y1choice : choiced p
y1choice = choice-func p np
-              y1 : OD
+              y1 : HOD
y1 = a-choice y1choice
y1prop : (x ∋ y1) ∧ (u ∋ y1)
y1prop = is-in y1choice
min2 : Minimal u
min2 = prev (proj1 y1prop) u (proj2 y1prop)
-         Min2 : (x : OD) → (u : OD ) → (u∋x : u ∋ x) → Minimal u
-         Min2 x u u∋x = (ε-induction {λ y →  (u : OD ) → (u∋x : u ∋ y) → Minimal u  } induction x u u∋x )
-         cx : {x : OD} →  ¬ (x == od∅ ) → choiced x
+         Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u
+         Min2 x u u∋x = (ε-induction1 {λ y →  (u : HOD ) → (u∋x : u ∋ y) → Minimal u  } induction x u u∋x )
+         cx : {x : HOD} →  ¬ (x =h= od∅ ) → choiced x
cx {x} nx = choice-func x nx
-         minimal : (x : OD  ) → ¬ (x == od∅ ) → OD
-         minimal x not = min (Min2 (a-choice (cx not) ) x (is-in (cx not)))
-         x∋minimal : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
-         x∋minimal x ne = x∋min (Min2 (a-choice (cx ne) ) x (is-in (cx ne)))
-         minimal-1 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
+         minimal : (x : HOD  ) → ¬ (x =h= od∅ ) → HOD
+         minimal x ne = min (Min2 (a-choice (cx {x} ne) ) x (is-in (cx ne)))
+         x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) )
+         x∋minimal x ne = x∋min (Min2 (a-choice (cx {x} ne) ) x (is-in (cx ne)))
+         minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord  y) )
minimal-1 x ne y = min-empty (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) y

```
```--- a/OD.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/OD.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -53,28 +53,27 @@
eq← ( ⇔→==  {x} {y}  eq ) {z} m = proj2 eq m

-- next assumptions are our axiom
---  it defines a subset of OD, which is called HOD, usually defined as
+--
+--  OD is an equation on Ordinals, so it contains Ordinals. If these Ordinals have one-to-one
+--  correspondence to the OD then the OD looks like a ZF Set.
+--
+--  If all ZF Set have supreme upper bound, the solutions of OD have to be bounded, i.e.
+--  bbounded ODs are ZF Set. Unbounded ODs are classes.
+--
+--  In classical Set Theory, HOD is used, as a subset of OD,
--     HOD = { x | TC x ⊆ OD }
---  where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x
-
-record ODAxiom : Set (suc n) where
-  -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
- field
-  od→ord : OD  → Ordinal
-  ord→od : Ordinal  → OD
-  c<→o<  :  {x y : OD  }   → def y ( od→ord x ) → od→ord x o< od→ord y
-  oiso   :  {x : OD }      → ord→od ( od→ord x ) ≡ x
-  diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
-  ==→o≡ : { x y : OD  } → (x == y) → x ≡ y
-  -- supermum as Replacement Axiom ( corresponding Ordinal of OD has maximum )
-  sup-o  :  ( OD → Ordinal ) →  Ordinal
-  sup-o< :  { ψ : OD →  Ordinal } → ∀ {x : OD } → ψ x  o<  sup-o ψ
-  -- contra-position of mimimulity of supermum required in Power Set Axiom which we don't use
-  -- sup-x  : {n : Level } → ( OD → Ordinal ) →  Ordinal
-  -- sup-lb : {n : Level } → { ψ : OD →  Ordinal } → {z : Ordinal }  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
-
-postulate  odAxiom : ODAxiom
-open ODAxiom odAxiom
+--  where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x.
+--  This is not possible because we don't have V yet. So we assumes HODs are bounded OD.
+--
+--  We also assumes HODs are isomorphic to Ordinals, which is ususally proved by Goedel number tricks.
+--  There two contraints on the HOD order, one is ∋, the other one is ⊂.
+--  ODs have an ovbious maximum, but Ordinals are not, but HOD has no maximum because there is an aribtrary
+--  bound on each HOD.
+--
+--  In classical Set Theory, sup is defined by Uion, since we are working on constructive logic,
+--  we need explict assumption on sup.
+--
+--  ==→o≡ is necessary to prove axiom of extensionality.

data One : Set n where
OneObj : One
@@ -83,100 +82,125 @@
Ords : OD
Ords = record { def = λ x → One }

-maxod : {x : OD} → od→ord x o< od→ord Ords
-maxod {x} = c<→o< OneObj
+record HOD : Set (suc n) where
+  field
+    od : OD
+    odmax : Ordinal
+    <odmax : {y : Ordinal} → def od y → y o< odmax
+
+open HOD
+
+record ODAxiom : Set (suc n) where
+ 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
+  ⊆→o≤  :   {y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z)
+  oiso   :  {x : HOD }      → ord→od ( od→ord x ) ≡ x
+  diso   :  {x : Ordinal }  → od→ord ( ord→od x ) ≡ x
+  ==→o≡ : { x y : HOD  }    → (od x == od y) → x ≡ y
+  sup-o  :  (A : HOD) → (( x : Ordinal ) → def (od A) x →  Ordinal ) →  Ordinal
+  sup-o< :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o<  sup-o A ψ
+
+postulate  odAxiom : ODAxiom
+open ODAxiom odAxiom
+
+-- maxod : {x : OD} → od→ord x o< od→ord Ords
+-- maxod {x} = c<→o< OneObj
+
+-- we have not this contradiction
+-- bad-bad : ⊥
+-- bad-bad = osuc-< <-osuc (c<→o< { record { od = record { def = λ x → One };  <odmax = {!!} } } OneObj)

-- Ordinal in OD ( and ZFSet ) Transitive Set
-Ord : ( a : Ordinal  ) → OD
-Ord  a = record { def = λ y → y o< a }
+Ord : ( a : Ordinal  ) → HOD
+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∅

-od∅ : OD
-od∅  = Ord o∅
+odef : HOD → Ordinal → Set n
+odef A x = def ( od A ) x
+
+o<→c<→HOD=Ord : ( {x y : Ordinal  } → x o< y → odef (ord→od y) x ) → {x : HOD } →  x ≡ Ord (od→ord x)
+o<→c<→HOD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
+   lemma1 : {y : Ordinal} → odef x y → odef (Ord (od→ord x)) y
+   lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (subst (λ k → odef x k ) (sym diso) lt))
+   lemma2 : {y : Ordinal} → odef (Ord (od→ord x)) y → odef x y
+   lemma2 {y} lt = subst (λ k → odef k y ) oiso (o<→c< {y} {od→ord x} lt )

-o<→c<→OD=Ord : ( {x y : Ordinal  } → x o< y → def (ord→od y) x ) → {x : OD } →  x ≡ Ord (od→ord x)
-o<→c<→OD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
-   lemma1 : {y : Ordinal} → def x y → def (Ord (od→ord x)) y
-   lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (subst (λ k → def x k ) (sym diso) lt))
-   lemma2 : {y : Ordinal} → def (Ord (od→ord x)) y → def x y
-   lemma2 {y} lt = subst (λ k → def k y ) oiso (o<→c< {y} {od→ord x} lt )
+_∋_ : ( a x : HOD  ) → Set n
+_∋_  a x  = odef a ( od→ord x )

-_∋_ : ( a x : OD  ) → Set n
-_∋_  a x  = def a ( od→ord x )
-
-_c<_ : ( x a : OD  ) → Set n
+_c<_ : ( x a : HOD  ) → Set n
x c< a = a ∋ x

-cseq : {n : Level} →  OD  →  OD
-cseq x = record { def = λ y → def x (osuc y) } where
-
-def-subst :  {Z : OD } {X : Ordinal  }{z : OD } {x : Ordinal  }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
-def-subst df refl refl = df
+cseq : {n : Level} →  HOD  →  HOD
+cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
+    lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x)
+    lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc )

-sup-od : ( OD  → OD ) →  OD
-sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ x)) )
+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

-sup-c< :  ( ψ : OD  →  OD ) → ∀ {x : OD } → def ( sup-od ψ ) (od→ord ( ψ x ))
-sup-c<   ψ {x} = def-subst  {_} {_} {Ord ( sup-o  ( λ x → od→ord (ψ x)) )} {od→ord ( ψ x )}
-        lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where
-    lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ x))
-    lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst (sup-o< ) refl (sym diso)  )
-
-otrans : {n : Level} {a x y : Ordinal  } → def (Ord a) x → def (Ord x) y → def (Ord a) y
+otrans : {n : Level} {a x y : Ordinal  } → odef (Ord a) x → odef (Ord x) y → odef (Ord a) y
otrans x<a y<x = ordtrans y<x x<a

-def→o< :  {X : OD } → {x : Ordinal } → def X x → x o< od→ord X
-def→o<  {X} {x} lt = o<-subst  {_} {_} {x} {od→ord X} ( c<→o< ( def-subst  {X} {x}  lt (sym oiso) (sym diso) )) diso diso
-
+odef→o< :  {X : HOD } → {x : Ordinal } → odef X x → x o< od→ord X
+odef→o<  {X} {x} lt = o<-subst  {_} {_} {x} {od→ord X} ( c<→o< ( odef-subst  {X} {x}  lt (sym oiso) (sym diso) )) diso diso

-- avoiding lv != Zero error
-orefl : { x : OD  } → { y : Ordinal  } → od→ord x ≡ y → od→ord x ≡ y
+orefl : { x : HOD  } → { y : Ordinal  } → od→ord x ≡ y → od→ord x ≡ y
orefl refl = refl

-==-iso : { x y : OD  } → ord→od (od→ord x) == ord→od (od→ord y)  →  x == y
+==-iso : { x y : HOD  } → od (ord→od (od→ord x)) == od (ord→od (od→ord y))  →  od x == od y
==-iso  {x} {y} eq = record {
-      eq→ = λ d →  lemma ( eq→  eq (def-subst d (sym oiso) refl )) ;
-      eq← = λ d →  lemma ( eq←  eq (def-subst d (sym oiso) refl ))  }
+      eq→ = λ d →  lemma ( eq→  eq (odef-subst d (sym oiso) refl )) ;
+      eq← = λ d →  lemma ( eq←  eq (odef-subst d (sym oiso) refl ))  }
where
-           lemma : {x : OD  } {z : Ordinal } → def (ord→od (od→ord x)) z → def x z
-           lemma {x} {z} d = def-subst d oiso refl
+           lemma : {x : HOD  } {z : Ordinal } → odef (ord→od (od→ord x)) z → odef x z
+           lemma {x} {z} d = odef-subst d oiso refl

-=-iso :  {x y : OD  } → (x == y) ≡ (ord→od (od→ord x) == y)
-=-iso  {_} {y} = cong ( λ k → k == y ) (sym oiso)
+=-iso :  {x y : HOD  } → (od x == od y) ≡ (od (ord→od (od→ord x)) == od y)
+=-iso  {_} {y} = cong ( λ k → od k == od y ) (sym oiso)

-ord→== : { x y : OD  } → od→ord x ≡  od→ord y →  x == y
+ord→== : { x y : HOD  } → od→ord x ≡  od→ord y →  od x == od y
ord→==  {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq)) where
-   lemma : ( ox oy : Ordinal  ) → ox ≡ oy →  (ord→od ox) == (ord→od oy)
+   lemma : ( ox oy : Ordinal  ) → ox ≡ oy →  od (ord→od ox) == od (ord→od oy)
lemma ox ox  refl = ==-refl

-o≡→== : { x y : Ordinal  } → x ≡  y →  ord→od x == ord→od y
+o≡→== : { x y : Ordinal  } → x ≡  y →  od (ord→od x) == od (ord→od y)
o≡→==  {x} {.x} refl = ==-refl

o∅≡od∅ : ord→od (o∅ ) ≡ od∅
o∅≡od∅  = ==→o≡ lemma where
-     lemma0 :  {x : Ordinal} → def (ord→od o∅) x → def od∅ x
-     lemma0 {x} lt = o<-subst (c<→o<  {ord→od x} {ord→od o∅} (def-subst  {ord→od o∅} {x} lt refl (sym diso)) ) diso diso
-     lemma1 :  {x : Ordinal} → def od∅ x → def (ord→od o∅) x
+     lemma0 :  {x : Ordinal} → odef (ord→od o∅) x → odef od∅ x
+     lemma0 {x} lt = o<-subst (c<→o<  {ord→od x} {ord→od o∅} (odef-subst  {ord→od o∅} {x} lt refl (sym diso)) ) diso diso
+     lemma1 :  {x : Ordinal} → odef od∅ x → odef (ord→od o∅) x
lemma1 {x} lt = ⊥-elim (¬x<0 lt)
-     lemma : ord→od o∅ == od∅
+     lemma : od (ord→od o∅) == od od∅
lemma = record { eq→ = lemma0 ; eq← = lemma1 }

ord-od∅ : od→ord (od∅ ) ≡ o∅
ord-od∅  = sym ( subst (λ k → k ≡  od→ord (od∅ ) ) diso (cong ( λ k → od→ord k ) o∅≡od∅ ) )

-∅0 : record { def = λ x →  Lift n ⊥ } == od∅
+∅0 : record { def = λ x →  Lift n ⊥ } == od od∅
eq→ ∅0 {w} (lift ())
eq← ∅0 {w} lt = lift (¬x<0 lt)

-∅< : { x y : OD  } → def x (od→ord y ) → ¬ (  x  == od∅  )
+∅< : { x y : HOD  } → odef x (od→ord y ) → ¬ (  od x  == od od∅  )
∅<  {x} {y} d eq with eq→ (==-trans eq (==-sym ∅0) ) d
∅<  {x} {y} d eq | lift ()

-∅6 : { x : OD  }  → ¬ ( x ∋ x )    --  no Russel paradox
+∅6 : { x : HOD  }  → ¬ ( x ∋ x )    --  no Russel paradox
∅6  {x} x∋x = o<¬≡ refl ( c<→o<  {x} {x} x∋x )

-def-iso : {A B : OD } {x y : Ordinal } → x ≡ y  → (def A y → def B y)  → def A x → def B x
-def-iso refl t = t
+odef-iso : {A B : HOD } {x y : Ordinal } → x ≡ y  → (odef A y → odef B y)  → odef A x → odef B x
+odef-iso refl t = t

is-o∅ : ( x : Ordinal  ) → Dec ( x ≡ o∅  )
is-o∅ x with trio< x o∅
@@ -184,59 +208,72 @@
is-o∅ x | tri≈ ¬a b ¬c = yes b
is-o∅ x | tri> ¬a ¬b c = no ¬b

-_,_ : OD  → OD  → OD
-x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } --  Ord (omax (od→ord x) (od→ord y))
+_,_ : HOD  → HOD  → HOD
+x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = omax (od→ord x)  (od→ord y) ; <odmax = lemma }  where
+    lemma : {t : Ordinal} → (t ≡ od→ord x) ∨ (t ≡ od→ord y) → t o< omax (od→ord x) (od→ord y)
+    lemma {t} (case1 refl) = omax-x  _ _
+    lemma {t} (case2 refl) = omax-y  _ _
+

-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
-- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)

-in-codomain : (X : OD  ) → ( ψ : OD  → OD  ) → OD
-in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧  ( x ≡ od→ord (ψ (ord→od y )))))  }
+in-codomain : (X : HOD  ) → ( ψ : HOD  → HOD  ) → OD
+in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ( x ≡ od→ord (ψ (ord→od y )))))  }

--- Power Set of X ( or constructible by λ y → def X (od→ord y )
-
-ZFSubset : (A x : OD  ) → OD
-ZFSubset A x =  record { def = λ y → def A y ∧  def x y }  --   roughly x = A → Set
+-- Power Set of X ( or constructible by λ y → odef X (od→ord y )

-Def :  (A :  OD ) → OD
-Def  A = Ord ( sup-o  ( λ x → od→ord ( ZFSubset A x) ) )
+ZFSubset : (A x : HOD  ) → HOD
+ZFSubset A x =  record { od = record { def = λ y → odef A y ∧  odef x y } ; odmax = omin (odmax A) (odmax x) ; <odmax = lemma }  where --   roughly x = A → Set
+     lemma : {y : Ordinal} → def (od A) y ∧ def (od x) y → y o< omin (odmax A) (odmax x)
+     lemma {y} and = min1 (<odmax A (proj1 and)) (<odmax x (proj2 and))

--- _⊆_ :  ( A B : OD   ) → ∀{ x : OD  } →  Set n
--- _⊆_ A B {x} = A ∋ x →  B ∋ x
-
-record _⊆_ ( A B : OD   ) : Set (suc n) where
+record _⊆_ ( A B : HOD   ) : Set (suc n) where
field
-     incl : { x : OD } → A ∋ x →  B ∋ x
+     incl : { x : HOD } → A ∋ x →  B ∋ x

open _⊆_
-
infixr  220 _⊆_

-subset-lemma : {A x : OD  } → ( {y : OD } →  x ∋ y → ZFSubset A x ∋  y ) ⇔  ( x ⊆ A  )
+subset-lemma : {A x : HOD  } → ( {y : HOD } →  x ∋ y → ZFSubset A x ∋  y ) ⇔  ( x ⊆ A  )
subset-lemma  {A} {x} = record {
proj1 = λ lt  → record { incl = λ x∋z → proj1 (lt x∋z)  }
; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt }
}

+od⊆→o≤  : {x y : HOD } → x ⊆ y → od→ord x o< osuc (od→ord y)
+od⊆→o≤ {x} {y} lt  =  ⊆→o≤ {x} {y} (λ {z} x>z  → subst (λ k → def (od y) k ) diso (incl lt (subst (λ k → def (od x) k ) (sym diso) x>z )))
+
+power< : {A x : HOD  } → x ⊆ A → Ord (osuc (od→ord A)) ∋ x
+power< {A} {x} x⊆A = ⊆→o≤  (λ {y} x∋y → subst (λ k →  def (od A) k) diso (lemma y x∋y ) ) where
+    lemma : (y : Ordinal) → def (od x) y → def (od A) (od→ord (ord→od y))
+    lemma y x∋y = incl x⊆A (subst (λ k → def (od x) k ) (sym diso) x∋y )
+
open import Data.Unit

-ε-induction : { ψ : OD  → Set (suc n)}
-   → ( {x : OD } → ({ y : OD } →  x ∋ y → ψ y ) → ψ x )
-   → (x : OD ) → ψ x
+ε-induction : { ψ : HOD  → Set n}
+   → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
+   → (x : HOD ) → ψ x
ε-induction {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc )  where
induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso )))
ε-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 : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
--- minimal-2 x ne y = contra-position ( ε-induction (λ {z} ind → {!!} ) x ) ( λ p → {!!} )
+ε-induction1 : { ψ : HOD  → Set (suc n)}
+   → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
+   → (x : HOD ) → ψ x
+ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc )  where
+     induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
+     induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso )))
+     ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
+     ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy

-OD→ZF : ZF
-OD→ZF   = record {
-    ZFSet = OD
+HOD→ZF : ZF
+HOD→ZF   = record {
+    ZFSet = HOD
; _∋_ = _∋_
-    ; _≈_ = _==_
+    ; _≈_ = _=h=_
; ∅  = od∅
; _,_ = _,_
; Union = Union
@@ -246,19 +283,43 @@
; infinite = infinite
; isZF = isZF
} where
-    ZFSet = OD             -- is less than Ords because of maxod
-    Select : (X : OD  ) → ((x : OD  ) → Set n ) → OD
-    Select X ψ = record { def = λ x →  ( def X x ∧ ψ ( ord→od x )) }
-    Replace : OD  → (OD  → OD  ) → OD
-    Replace X ψ = record { def = λ x → (x o< sup-o  ( λ x → od→ord (ψ x))) ∧ def (in-codomain X ψ) x }
+    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 = 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∋y → od→ord (ψ (ord→od y)))) ∧ def (in-codomain X ψ) x }
+       ; odmax = rmax ; <odmax = rmax<} where
+          rmax : Ordinal
+          rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))
+          rmax< :  {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax
+          rmax< lt = proj1 lt
_∩_ : ( A B : ZFSet  ) → ZFSet
-    A ∩ B = record { def = λ x → def A x ∧ def B x }
-    Union : OD  → OD
-    Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x)))  }
+    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
+    Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x)))  }
+       ; odmax = osuc (od→ord U) ; <odmax = umax< } where
+           umax< :  {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (ord→od u)) y) → y o< osuc (od→ord U)
+           umax< {y} not = lemma (FExists _ lemma1 not ) where
+               lemma0 : {x : Ordinal} → def (od (ord→od x)) y → y o< x
+               lemma0 {x} x<y = subst₂ (λ j k → j o< k ) diso  diso (c<→o< (subst (λ k → def (od (ord→od x)) k) (sym diso) x<y))
+               lemma2 : {x : Ordinal} → def (od U) x → x o< od→ord U
+               lemma2 {x} x<U = subst (λ k → k o< od→ord U ) diso (c<→o< (subst (λ k → def (od U) k) (sym diso) x<U))
+               lemma1 : {x : Ordinal} → def (od U) x ∧ def (od (ord→od x)) y → ¬ (od→ord U o< y)
+               lemma1 {x} lt u<y = o<> u<y (ordtrans (lemma0 (proj2 lt)) (lemma2 (proj1 lt)) )
+               lemma : ¬ ((od→ord U) o< y ) → y o< osuc (od→ord U)
+               lemma not with trio< y (od→ord U)
+               lemma not | tri< a ¬b ¬c = ordtrans a <-osuc
+               lemma not | tri≈ ¬a refl ¬c = <-osuc
+               lemma not | tri> ¬a ¬b c = ⊥-elim (not c)
_∈_ : ( A B : ZFSet  ) → Set n
A ∈ B = B ∋ A
-    Power : OD  → OD
-    Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
+
+    OPwr :  (A :  HOD ) → HOD
+    OPwr  A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) )
+
+    Power : HOD  → HOD
+    Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x )
-- ｛_｝ : ZFSet → ZFSet
-- ｛ x ｝ = ( x ,  x )     -- it works but we don't use

@@ -267,12 +328,25 @@
isuc : {x : Ordinal  } →   infinite-d  x  →
infinite-d  (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))

-    infinite : OD
-    infinite = record { def = λ x → infinite-d x }
+    -- ω can be diverged in our case, since we have no restriction on the corresponding ordinal of a pair.
+    -- We simply assumes nfinite-d y has a maximum.
+    --
+    -- This means that many of OD cannot be HODs because of the od→ord mapping divergence.
+    -- We should have some axioms to prevent this, but it may complicate thins.
+    --
+    postulate
+        ωmax : Ordinal
+        <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax
+
+    infinite : HOD
+    infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax }
+
+    _=h=_ : (x y : HOD) → Set n
+    x =h= y  = od x == od y

infixr  200 _∈_
-- infixr  230 _∩_ _∪_
-    isZF : IsZF (OD )  _∋_  _==_ od∅ _,_ Union Power Select Replace infinite
+    isZF : IsZF (HOD )  _∋_  _=h=_ od∅ _,_ Union Power Select Replace infinite
isZF = record {
isEquivalence  = record { refl = ==-refl ; sym = ==-sym; trans = ==-trans }
;   pair→  = pair→
@@ -288,20 +362,20 @@
;   infinity = infinity
;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
;   replacement← = replacement←
-       ;   replacement→ = replacement→
+       ;   replacement→ = λ {ψ} → replacement→ {ψ}
-- ;   choice-func = choice-func
-- ;   choice = choice
} where

-         pair→ : ( x y t : ZFSet  ) →  (x , y)  ∋ t  → ( t == x ) ∨ ( t == y )
-         pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡x ))
-         pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡y ))
+         pair→ : ( x y t : ZFSet  ) →  (x , y)  ∋ t  → ( t =h= x ) ∨ ( t =h= y )
+         pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j =h= k ) oiso oiso (o≡→== t≡x ))
+         pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j =h= k ) oiso oiso (o≡→== t≡y ))

-         pair← : ( x y t : ZFSet  ) → ( t == x ) ∨ ( t == y ) →  (x , y)  ∋ t
-         pair← x y t (case1 t==x) = case1 (cong (λ k → od→ord k ) (==→o≡ t==x))
-         pair← x y t (case2 t==y) = case2 (cong (λ k → od→ord k ) (==→o≡ t==y))
+         pair← : ( x y t : ZFSet  ) → ( t =h= x ) ∨ ( t =h= y ) →  (x , y)  ∋ t
+         pair← x y t (case1 t=h=x) = case1 (cong (λ k → od→ord k ) (==→o≡ t=h=x))
+         pair← x y t (case2 t=h=y) = case2 (cong (λ k → od→ord k ) (==→o≡ t=h=y))

-         empty : (x : OD  ) → ¬  (od∅ ∋ x)
+         empty : (x : HOD  ) → ¬  (od∅ ∋ x)
empty x = ¬x<0

o<→c< :  {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y)
@@ -314,114 +388,167 @@
⊆→o< {x} {y}  lt | tri> ¬a ¬b c with (incl lt)  (o<-subst c (sym diso) refl )
... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl ))

-         union→ :  (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
+         union→ :  (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
-              ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } ))
-         union← :  (X z : OD) (X∋z : Union X ∋ z) →  ¬  ( (u : OD ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
+              ; proj2 = subst ( λ k → odef k (od→ord z)) (sym oiso) (proj2 xx) } ))
+         union← :  (X z : HOD) (X∋z : Union X ∋ z) →  ¬  ( (u : HOD ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
union← X z UX∋z =  FExists _ lemma UX∋z where
-              lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z))
-              lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx }
+              lemma : {y : Ordinal} → odef X y ∧ odef (ord→od y) (od→ord z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z))
+              lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → odef X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx }

-         ψiso :  {ψ : OD  → Set n} {x y : OD } → ψ x → x ≡ y   → ψ y
+         ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
ψiso {ψ} t refl = t
-         selection : {ψ : OD → Set n} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
+         selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
selection {ψ} {X} {y} = record {
proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso)  }
; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
}
-         replacement← : {ψ : OD → OD} (X x : OD) →  X ∋ x → Replace X ψ ∋ ψ x
-         replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {x} ; proj2 = lemma } where
+         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 =  sup-c< ψ {X} {x} lt ; proj2 = lemma } where
lemma : def (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→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
+         replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
-            lemma2 :  ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y))))
-                    → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (ord→od y)))
+            lemma2 :  ¬ ((y : Ordinal) → ¬ odef X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y))))
+                    → ¬ ((y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y)))
lemma2 not not2  = not ( λ y d →  not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
-                lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od  y))) → (ord→od (od→ord x) == ψ (ord→od y))
-                lemma3 {y} eq = subst (λ k  → ord→od (od→ord x) == k ) oiso (o≡→== eq )
-            lemma :  ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (ord→od y)) )
-            lemma not y not2 = not (ord→od y) (subst (λ k → k == ψ (ord→od y)) oiso  ( proj2 not2 ))
+                lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od  y))) → (ord→od (od→ord x) =h= ψ (ord→od y))
+                lemma3 {y} eq = subst (λ k  → ord→od (od→ord x) =h= k ) oiso (o≡→== eq )
+            lemma :  ( (y : HOD) → ¬ (x =h= ψ y)) → ( (y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y)) )
+            lemma not y not2 = not (ord→od y) (subst (λ k → k =h= ψ (ord→od y)) oiso  ( proj2 not2 ))

---
--- Power Set
---
-         ---    First consider ordinals in OD
+         ---    First consider ordinals in HOD
---
-         --- ZFSubset A x =  record { def = λ y → def A y ∧  def x y }                   subset of A
+         --- ZFSubset A x =  record { def = λ y → odef A y ∧  odef x y }                   subset of A
--
--
-         ∩-≡ :  { a b : OD  } → ({x : OD  } → (a ∋ x → b ∋ x)) → a == ( b ∩ a )
+         ∩-≡ :  { a b : HOD  } → ({x : HOD  } → (a ∋ x → b ∋ x)) → a =h= ( b ∩ a )
∩-≡ {a} {b} inc = record {
eq→ = λ {x} x<a → record { proj2 = x<a ;
-                 proj1 = def-subst  {_} {_} {b} {x} (inc (def-subst  {_} {_} {a} {_} x<a refl (sym diso) )) refl diso  } ;
+                 proj1 = odef-subst  {_} {_} {b} {x} (inc (odef-subst  {_} {_} {a} {_} x<a refl (sym diso) )) refl diso  } ;
eq← = λ {x} x<a∩b → proj2 x<a∩b }
--
-- Transitive Set case
-         -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is ZFSubset (Ord a) t == t
-         -- Def (Ord a) is a sup of ZFSubset (Ord a) t, so Def (Ord a) ∋ t
-         -- Def  A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
+         -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is ZFSubset (Ord a) t =h= t
+         -- OPwr (Ord a) is a sup of ZFSubset (Ord a) t, so OPwr (Ord a) ∋ t
+         -- OPwr  A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
--
-         ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t
-         ord-power← a t t→A  = def-subst  {_} {_} {Def (Ord a)} {od→ord t}
+         ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t
+         ord-power← a t t→A  = odef-subst  {_} {_} {OPwr (Ord a)} {od→ord t}
lemma refl (lemma1 lemma-eq )where
-              lemma-eq :  ZFSubset (Ord a) t == t
+              lemma-eq :  ZFSubset (Ord a) t =h= t
eq→ lemma-eq {z} w = proj2 w
eq← lemma-eq {z} w = record { proj2 = w  ;
-                 proj1 = def-subst  {_} {_} {(Ord a)} {z}
-                    ( t→A (def-subst  {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
-              lemma1 :  {a : Ordinal } { t : OD }
-                 → (eq : ZFSubset (Ord a) t == t)  → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
+                 proj1 = odef-subst  {_} {_} {(Ord a)} {z}
+                    ( t→A (odef-subst  {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
+              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 = sup-o<
+              lemma2 : (od→ord t) o< (osuc (od→ord (Ord a)))
+              lemma2 = ⊆→o≤  {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) diso (t→A (subst (λ k → def (od t) k) (sym diso) x<t)))
+              lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (Ord (osuc (od→ord (Ord a)))) (λ x lt → od→ord (ZFSubset (Ord a) (ord→od x)))
+              lemma = sup-o< _ lemma2

--
-         -- Every set in OD is a subset of Ordinals, so make Def (Ord (od→ord A)) first
+         -- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first
-- then replace of all elements of the Power set by A ∩ y
--
-         -- Power A = Replace (Def (Ord (od→ord A))) ( λ y → A ∩ y )
+         -- Power A = Replace (OPwr (Ord (od→ord A))) ( λ y → A ∩ y )

-- we have oly double negation form because of the replacement axiom
--
-         power→ :  ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
+         power→ :  ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → ¬ ¬ (A ∋ x)
power→ A t P∋t {x} t∋x = FExists _ lemma5 lemma4 where
a = od→ord A
-              lemma2 : ¬ ( (y : OD) → ¬ (t ==  (A ∩ y)))
-              lemma2 = replacement→ (Def (Ord (od→ord A))) t P∋t
-              lemma3 : (y : OD) → t == ( A ∩ y ) → ¬ ¬ (A ∋ x)
+              lemma2 : ¬ ( (y : HOD) → ¬ (t =h=  (A ∩ y)))
+              lemma2 = replacement→ {λ x → A ∩ x} (OPwr (Ord (od→ord A))) t P∋t
+              lemma3 : (y : HOD) → t =h= ( A ∩ y ) → ¬ ¬ (A ∋ x)
lemma3 y eq not = not (proj1 (eq→ eq t∋x))
-              lemma4 : ¬ ((y : Ordinal) → ¬ (t == (A ∩ ord→od y)))
-              lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t == ( A ∩ k )) (sym oiso) not1 ))
-              lemma5 : {y : Ordinal} → t == (A ∩ ord→od y) →  ¬ ¬  (def A (od→ord x))
+              lemma4 : ¬ ((y : Ordinal) → ¬ (t =h= (A ∩ ord→od y)))
+              lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t =h= ( A ∩ k )) (sym oiso) not1 ))
+              lemma5 : {y : Ordinal} → t =h= (A ∩ ord→od y) →  ¬ ¬  (odef A (od→ord x))
lemma5 {y} eq not = (lemma3 (ord→od y) eq) not

-         power← :  (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
+         power← :  (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
power← A t t→A = record { proj1 = lemma1 ; proj2 = lemma2 } where
a = od→ord A
-              lemma0 : {x : OD} → t ∋ x → Ord a ∋ x
+              lemma0 : {x : HOD} → t ∋ x → Ord a ∋ x
lemma0 {x} t∋x = c<→o< (t→A t∋x)
-              lemma3 : Def (Ord a) ∋ t
+              lemma3 : OPwr (Ord a) ∋ t
lemma3 = ord-power← a t lemma0
lemma4 :  (A ∩ ord→od (od→ord t)) ≡ t
lemma4 = let open ≡-Reasoning in begin
A ∩ ord→od (od→ord t)
≡⟨ cong (λ k → A ∩ k) oiso ⟩
A ∩ t
-                 ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩
+                 ≡⟨ sym (==→o≡ ( ∩-≡ {t} {A} 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)))
-                  lemma4 (sup-o<  {λ x → od→ord (A ∩ x)}  )
-              lemma2 :  def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t)
+              sup1 : Ordinal
+              sup1 =  sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord (ZFSubset (Ord (od→ord A)) (ord→od x)))
+              lemma9 : def (od (Ord (Ordinals.osuc O (od→ord (Ord (od→ord A)))))) (od→ord (Ord (od→ord A)))
+              lemma9 = <-osuc
+              lemmab : od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A) )))) o< sup1
+              lemmab = sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9
+              lemmad : Ord (osuc (od→ord A)) ∋ t
+              lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) diso (t→A (subst (λ k → def (od t) k ) (sym diso) lt)))
+              lemmac : ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A) ))) =h= Ord (od→ord A)
+              lemmac = record { eq→ = lemmaf ; eq← = lemmag } where
+                 lemmaf : {x : Ordinal} → def (od (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A)))))) x → def (od (Ord (od→ord A))) x
+                 lemmaf {x} lt = proj1 lt
+                 lemmag :  {x : Ordinal} → def (od (Ord (od→ord A))) x → def (od (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A)))))) x
+                 lemmag {x} lt = record { proj1 = lt ; proj2 = subst (λ k → def (od k) x) (sym oiso) lt }
+              lemmae : od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A))))) ≡ od→ord (Ord (od→ord A))
+              lemmae = cong (λ k → od→ord k ) ( ==→o≡ lemmac)
+              lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t)
+              lemma7 with osuc-≡< lemmad
+              lemma7 | case2 lt = ordtrans (c<→o< lt) (subst (λ k → k o< sup1) lemmae lemmab )
+              lemma7 | case1 eq with osuc-≡< (⊆→o≤ {ord→od (od→ord t)} {ord→od (od→ord (Ord (od→ord t)))} (λ {x} lt → lemmah lt )) where
+                  lemmah : {x : Ordinal } → def (od (ord→od (od→ord t))) x → def (od (ord→od (od→ord (Ord (od→ord t))))) x
+                  lemmah {x} lt = subst (λ k → def (od k) x ) (sym oiso) (subst (λ k → k o< (od→ord t))
+                      diso
+                      (c<→o< (subst₂ (λ j k → def (od j)  k) oiso (sym diso) lt )))
+              lemma7 | case1 eq | case1 eq1 = subst (λ k → k o< sup1) (trans lemmae lemmai) lemmab where
+                  lemmai : od→ord (Ord (od→ord A)) ≡ od→ord t
+                  lemmai = let open ≡-Reasoning in begin
+                           od→ord (Ord (od→ord A))
+                        ≡⟨ sym (cong (λ k → od→ord (Ord k)) eq) ⟩
+                           od→ord (Ord (od→ord t))
+                        ≡⟨ sym diso ⟩
+                           od→ord (ord→od (od→ord (Ord (od→ord t))))
+                        ≡⟨ sym eq1 ⟩
+                           od→ord (ord→od (od→ord t))
+                        ≡⟨ diso ⟩
+                           od→ord t
+                        ∎
+              lemma7 | case1 eq | case2 lt = ordtrans lemmaj (subst (λ k → k o< sup1) lemmae lemmab ) where
+                  lemmak : od→ord (ord→od (od→ord (Ord (od→ord t)))) ≡ od→ord (Ord (od→ord A))
+                  lemmak = let open ≡-Reasoning in begin
+                           od→ord (ord→od (od→ord (Ord (od→ord t))))
+                        ≡⟨ diso ⟩
+                           od→ord (Ord (od→ord t))
+                        ≡⟨ cong (λ k → od→ord (Ord k)) eq ⟩
+                           od→ord (Ord (od→ord A))
+                        ∎
+                  lemmaj : od→ord t o< od→ord (Ord (od→ord A))
+                  lemmaj = subst₂ (λ j k → j o< k ) diso lemmak lt
+              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< (OPwr (Ord (od→ord A))) lemma7 )
+              lemma2 :  def (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 == (A ∩ k)) (sym oiso) ( ∩-≡ t→A  )))
+                  lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym oiso) ( ∩-≡ {t} {A} 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 : OD} → od→ord x o< osuc a → x ∋ y →  Ord a ∋ y
+                lemma : {x y : HOD} → od→ord x o< osuc a → x ∋ y →  Ord a ∋ y
lemma lt y<x with osuc-≡< lt
lemma lt y<x | case1 refl = c<→o< y<x
lemma lt y<x | case2 x<a = ordtrans (c<→o< y<x) x<a
@@ -429,16 +556,16 @@
continuum-hyphotheis : (a : Ordinal) → Set (suc n)
continuum-hyphotheis a = Power (Ord a) ⊆ Ord (osuc a)

-         extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
-         eq→ (extensionality0 {A} {B} eq ) {x} d = def-iso  {A} {B} (sym diso) (proj1 (eq (ord→od x))) d
-         eq← (extensionality0 {A} {B} eq ) {x} d = def-iso  {B} {A} (sym diso) (proj2 (eq (ord→od x))) d
+         extensionality0 : {A B : HOD } → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A =h= B
+         eq→ (extensionality0 {A} {B} eq ) {x} d = odef-iso  {A} {B} (sym diso) (proj1 (eq (ord→od x))) d
+         eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso  {B} {A} (sym diso) (proj2 (eq (ord→od x))) d

-         extensionality : {A B w : OD  } → ((z : OD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B)
+         extensionality : {A B w : HOD  } → ((z : HOD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B)
proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d
proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d

infinity∅ : infinite  ∋ od∅
-         infinity∅ = def-subst  {_} {_} {infinite} {od→ord (od∅ )} iφ refl lemma where
+         infinity∅ = odef-subst  {_} {_} {infinite} {od→ord (od∅ )} iφ refl lemma where
lemma : o∅ ≡ od→ord od∅
lemma =  let open ≡-Reasoning in begin
o∅
@@ -447,15 +574,15 @@
≡⟨ cong ( λ k → od→ord k ) o∅≡od∅ ⟩
od→ord od∅
∎
-         infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
-         infinity x lt = def-subst  {_} {_} {infinite} {od→ord (Union (x , (x , x )))} ( isuc {od→ord x} lt ) refl lemma where
+         infinity : (x : HOD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
+         infinity x lt = odef-subst  {_} {_} {infinite} {od→ord (Union (x , (x , x )))} ( isuc {od→ord x} lt ) refl lemma where
lemma :  od→ord (Union (ord→od (od→ord x) , (ord→od (od→ord x) , ord→od (od→ord x))))
≡ od→ord (Union (x , (x , x)))
lemma = cong (λ k → od→ord (Union ( k , ( k , k ) ))) oiso

-Union = ZF.Union OD→ZF
-Power = ZF.Power OD→ZF
-Select = ZF.Select OD→ZF
-Replace = ZF.Replace OD→ZF
-isZF = ZF.isZF  OD→ZF
+Union = ZF.Union HOD→ZF
+Power = ZF.Power HOD→ZF
+Select = ZF.Select HOD→ZF
+Replace = ZF.Replace HOD→ZF
+isZF = ZF.isZF  HOD→ZF```
```--- a/ODC.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/ODC.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -21,13 +21,20 @@
open OD._==_
open ODAxiom odAxiom

+open HOD
+
+open _∧_
+
+_=h=_ : (x y : HOD) → Set n
+x =h= y  = od x == od y
+
postulate
-- mimimul and x∋minimal is an Axiom of choice
-  minimal : (x : OD  ) → ¬ (x == od∅ )→ OD
-  -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
-  x∋minimal : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
-  -- minimality (may proved by ε-induction )
-  minimal-1 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
+  minimal : (x : HOD  ) → ¬ (x =h= od∅ )→ HOD
+  -- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
+  x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) )
+  -- minimality (may proved by ε-induction with LEM)
+  minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord  y) )

--
@@ -35,20 +42,26 @@
--     https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
--

-ppp :  { p : Set n } { a : OD  } → record { def = λ x → p } ∋ a → p
-ppp  {p} {a} d = d
+pred-od :  ( p : Set n )  → HOD
+pred-od  p  = record { od = record { def = λ x → (x ≡ o∅) ∧ p } ;
+   odmax = osuc o∅; <odmax = λ x → subst (λ k →  k o< osuc o∅) (sym (proj1 x)) <-osuc }
+
+ppp :  { p : Set n } { a : HOD  } → pred-od p ∋ a → p
+ppp  {p} {a} d = proj2 d

p∨¬p : ( p : Set n ) → p ∨ ( ¬ p )         -- assuming axiom of choice
-p∨¬p  p with is-o∅ ( od→ord ( record { def = λ x → p } ))
+p∨¬p  p with is-o∅ ( od→ord (pred-od p ))
p∨¬p  p | yes eq = case2 (¬p eq) where
-   ps = record { def = λ x → p }
-   lemma : ps == od∅ → p → ⊥
-   lemma eq p0 = ¬x<0  {od→ord ps} (eq→ eq p0 )
+   ps = pred-od p
+   eqo∅ : ps =h=  od∅  → od→ord ps ≡  o∅
+   eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq))
+   lemma : ps =h= od∅ → p → ⊥
+   lemma eq p0 = ¬x<0  {od→ord ps} (eq→ eq record { proj1 = eqo∅ eq ; proj2 = p0 } )
¬p : (od→ord ps ≡ o∅) → p → ⊥
-   ¬p eq = lemma ( subst₂ (λ j k → j ==  k ) oiso o∅≡od∅ ( o≡→== eq ))
+   ¬p eq = lemma ( subst₂ (λ j k → j =h=  k ) oiso o∅≡od∅ ( o≡→== eq ))
p∨¬p  p | no ¬p = case1 (ppp  {p} {minimal ps (λ eq →  ¬p (eqo∅ eq))} lemma) where
-   ps = record { def = λ x → p }
-   eqo∅ : ps ==  od∅  → od→ord ps ≡  o∅
+   ps = pred-od p
+   eqo∅ : ps =h=  od∅  → od→ord ps ≡  o∅
eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq))
lemma : ps ∋ minimal ps (λ eq →  ¬p (eqo∅ eq))
lemma = x∋minimal ps (λ eq →  ¬p (eqo∅ eq))
@@ -63,7 +76,7 @@
... | yes p = p
... | no ¬p = ⊥-elim ( notnot ¬p )

-OrdP : ( x : Ordinal  ) ( y : OD  ) → Dec ( Ord x ∋ y )
+OrdP : ( x : Ordinal  ) ( y : HOD  ) → Dec ( Ord x ∋ y )
OrdP  x y with trio< x (od→ord y)
OrdP  x y | tri< a ¬b ¬c = no ¬c
OrdP  x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
@@ -71,26 +84,26 @@

open import zfc

-OD→ZFC : ZFC
-OD→ZFC   = record {
-    ZFSet = OD
+HOD→ZFC : ZFC
+HOD→ZFC   = record {
+    ZFSet = HOD
; _∋_ = _∋_
-    ; _≈_ = _==_
+    ; _≈_ = _=h=_
; ∅  = od∅
; Select = Select
; isZFC = isZFC
} where
-- infixr  200 _∈_
-- infixr  230 _∩_ _∪_
-    isZFC : IsZFC (OD )  _∋_  _==_ od∅ Select
+    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ Select
isZFC = record {
choice-func = choice-func ;
choice = choice
} where
-- Axiom of choice ( is equivalent to the existence of minimal in our case )
-- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
-         choice-func : (X : OD  ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD
+         choice-func : (X : HOD  ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD
choice-func X {x} not X∋x = minimal x not
-         choice : (X : OD  ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A
+         choice : (X : HOD  ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A
choice X {A} X∋A not = x∋minimal A not
```
```--- a/OPair.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/OPair.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -17,6 +17,7 @@
open inOrdinal O
open OD O
open OD.OD
+open OD.HOD
open ODAxiom odAxiom

open _∧_
@@ -25,30 +26,33 @@

open _==_

-<_,_> : (x y : OD) → OD
+_=h=_ : (x y : HOD) → Set n
+x =h= y  = od x == od y
+
+<_,_> : (x y : HOD) → HOD
< x , y > = (x , x ) , (x , y )

-exg-pair : { x y : OD } → (x , y ) == ( y , x )
+exg-pair : { x y : HOD } → (x , y ) =h= ( y , x )
exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
-    left : {z : Ordinal} → def (x , y) z → def (y , x) z
+    left : {z : Ordinal} → odef (x , y) z → odef (y , x) z
left (case1 t) = case2 t
left (case2 t) = case1 t
-    right : {z : Ordinal} → def (y , x) z → def (x , y) z
+    right : {z : Ordinal} → odef (y , x) z → odef (x , y) z
right (case1 t) = case2 t
right (case2 t) = case1 t

-ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y
+ord≡→≡ : { x y : HOD } → od→ord x ≡ od→ord y → x ≡ y
ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq )

od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y
od≡→≡ eq = subst₂ (λ j k → j ≡ k ) diso diso ( cong ( λ k → od→ord k ) eq )

-eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
+eq-prod : { x x' y y' : HOD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
eq-prod refl refl = refl

-prod-eq : { x x' y y' : OD } → < x , y > == < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
+prod-eq : { x x' y y' : HOD } → < x , y > =h= < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where
-    lemma0 : {x y z : OD } → ( x , x ) == ( z , y ) → x ≡ y
+    lemma0 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → x ≡ y
lemma0 {x} {y} eq with trio< (od→ord x) (od→ord y)
lemma0 {x} {y} eq | tri< a ¬b ¬c with eq← eq {od→ord y} (case2 refl)
lemma0 {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a )
@@ -57,15 +61,15 @@
lemma0 {x} {y} eq | tri> ¬a ¬b c  with eq← eq {od→ord y} (case2 refl)
lemma0 {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c )
lemma0 {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c )
-    lemma2 : {x y z : OD } → ( x , x ) == ( z , y ) → z ≡ y
+    lemma2 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → z ≡ y
lemma2 {x} {y} {z} eq = trans (sym (lemma0 lemma3 )) ( lemma0 eq )  where
-        lemma3 : ( x , x ) == ( y , z )
+        lemma3 : ( x , x ) =h= ( y , z )
lemma3 = ==-trans eq exg-pair
-    lemma1 : {x y : OD } → ( x , x ) == ( y , y ) → x ≡ y
+    lemma1 : {x y : HOD } → ( x , x ) =h= ( y , y ) → x ≡ y
lemma1 {x} {y} eq with eq← eq {od→ord y} (case2 refl)
lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s)
lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s)
-    lemma4 : {x y z : OD } → ( x , y ) == ( x , z ) → y ≡ z
+    lemma4 : {x y z : HOD } → ( x , y ) =h= ( x , z ) → y ≡ z
lemma4 {x} {y} {z} eq with eq← eq {od→ord z} (case2 refl)
lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z
... | refl with lemma2 (==-sym eq )
@@ -81,6 +85,9 @@
... | refl with lemma4 eq -- with (x,y)≡(x,y')
... | eq1 = lemma4 (ord→== (cong (λ  k → od→ord k )  eq1 ))

+--
+-- unlike ordered pair, ZFProduct is not a HOD
+
data ord-pair : (p : Ordinal) → Set n where
pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )

@@ -94,35 +101,38 @@
pi1 : { p : Ordinal } →   ord-pair p →  Ordinal
pi1 ( pair x y) = x

-π1 : { p : OD } → ZFProduct ∋ p → OD
+π1 : { p : HOD } → def ZFProduct (od→ord p) → HOD
π1 lt = ord→od (pi1 lt )

pi2 : { p : Ordinal } →   ord-pair p →  Ordinal
pi2 ( pair x y ) = y

-π2 : { p : OD } → ZFProduct ∋ p → OD
+π2 : { p : HOD } → def ZFProduct (od→ord p) → HOD
π2 lt = ord→od (pi2 lt )

-op-cons :  { ox oy  : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy >
+op-cons :  { ox oy  : Ordinal } → def ZFProduct (od→ord ( < ord→od ox , ord→od oy >   ))
op-cons {ox} {oy} = pair ox oy

-p-cons :  ( x y  : OD ) → ZFProduct ∋ < x , y >
-p-cons x y =  def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
-    let open ≡-Reasoning in begin
-        od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
-    ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
-        od→ord < x , y >
-    ∎ )
+def-subst :  {Z : OD } {X : Ordinal  }{z : OD } {x : Ordinal  }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
+def-subst df refl refl = df
+
+p-cons :  ( x y  : HOD ) → def ZFProduct (od→ord ( < x , y >))
+p-cons x y = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
+   let open ≡-Reasoning in begin
+       od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
+   ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
+       od→ord < x , y >
+   ∎ )

op-iso :  { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op
op-iso (pair ox oy) = refl

-p-iso :  { x  : OD } → (p : ZFProduct ∋ x ) → < π1 p , π2 p > ≡ x
+p-iso :  { x  : HOD } → (p : def ZFProduct (od→ord  x) ) → < π1 p , π2 p > ≡ x
p-iso {x} p = ord≡→≡ (op-iso p)

-p-pi1 :  { x y : OD } → (p : ZFProduct ∋ < x , y > ) →  π1 p ≡ x
+p-pi1 :  { x y : HOD } → (p : def ZFProduct (od→ord  < x , y >) ) →  π1 p ≡ x
p-pi1 {x} {y} p = proj1 ( prod-eq ( ord→== (op-iso p) ))

-p-pi2 :  { x y : OD } → (p : ZFProduct ∋ < x , y > ) →  π2 p ≡ y
+p-pi2 :  { x y : HOD } → (p : def ZFProduct (od→ord  < x , y >) ) →  π2 p ≡ y
p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p)))
```
```--- a/Ordinals.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/Ordinals.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -13,14 +13,19 @@
open import Relation.Binary
open import Relation.Binary.Core

-record IsOrdinals {n : Level} (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where
+record IsOrdinals {n : Level} (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
field
Otrans :  {x y z : ord }  → x o< y → y o< z → x o< z
OTri : Trichotomous {n} _≡_  _o<_
¬x<0 :   { x  : ord  } → ¬ ( x o< o∅  )
<-osuc :  { x : ord  } → x o< osuc x
osuc-≡< :  { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)
-     TransFinite : { ψ : ord  → Set (suc n) }
+     not-limit :  ( x : ord  ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) ))
+     next-limit : { y : ord } → (y o< next y ) ∧  ((x : ord) → x o< next y → osuc x o< next y )
+     TransFinite : { ψ : ord  → Set n }
+          → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
+          →  ∀ (x : ord)  → ψ x
+     TransFinite1 : { ψ : ord  → Set (suc n) }
→ ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
→  ∀ (x : ord)  → ψ x

@@ -31,7 +36,8 @@
o∅ : ord
osuc : ord → ord
_o<_ : ord → ord → Set n
-     isOrdinal : IsOrdinals ord o∅ osuc _o<_
+     next :  ord → ord
+     isOrdinal : IsOrdinals ord o∅ osuc _o<_ next

module inOrdinal  {n : Level} (O : Ordinals {n} ) where

@@ -47,11 +53,16 @@
o∅ :   Ordinal
o∅ = Ordinals.o∅ O

+        next :   Ordinal → Ordinal
+        next = Ordinals.next O
+
¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O)
osuc-≡< = IsOrdinals.osuc-≡<  (Ordinals.isOrdinal O)
<-osuc = IsOrdinals.<-osuc  (Ordinals.isOrdinal O)
TransFinite = IsOrdinals.TransFinite  (Ordinals.isOrdinal O)
-
+        TransFinite1 = IsOrdinals.TransFinite1  (Ordinals.isOrdinal O)
+        next-limit = IsOrdinals.next-limit  (Ordinals.isOrdinal O)
+
o<-dom :   { x y : Ordinal } → x o< y → Ordinal
o<-dom  {x} _ = x

@@ -104,7 +115,7 @@
proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy

_o≤_ :  Ordinal → Ordinal → Set  n
-        a o≤ b  = (a ≡ b)  ∨ ( a o< b )
+        a o≤ b  = a o< osuc b -- (a ≡ b)  ∨ ( a o< b )

xo<ab :  {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa  → ox o< ob ) → oa o< osuc ob
@@ -119,13 +130,13 @@
maxα x y | tri> ¬a ¬b c = x
maxα x y | tri≈ ¬a refl ¬c = x

-        minα :    Ordinal  →  Ordinal  → Ordinal
-        minα  x y with trio<  x  y
-        minα x y | tri< a ¬b ¬c = x
-        minα x y | tri> ¬a ¬b c = y
-        minα x y | tri≈ ¬a refl ¬c = x
+        omin :    Ordinal  →  Ordinal  → Ordinal
+        omin  x y with trio<  x  y
+        omin x y | tri< a ¬b ¬c = x
+        omin x y | tri> ¬a ¬b c = y
+        omin x y | tri≈ ¬a refl ¬c = x

-        min1 :   {x y z : Ordinal  } → z o< x → z o< y → z o< minα x y
+        min1 :   {x y z : Ordinal  } → z o< x → z o< y → z o< omin x y
min1  {x} {y} {z} z<x z<y with trio<  x y
min1  {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x
min1  {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x
@@ -176,11 +187,14 @@

open _∧_

+        o≤-refl :  { i  j : Ordinal } → i ≡ j → i o≤ j
+        o≤-refl {i} {j} eq = subst (λ k → i o< osuc k ) eq <-osuc
OrdTrans :  Transitive  _o≤_
-        OrdTrans (case1 refl) (case1 refl) = case1 refl
-        OrdTrans (case1 refl) (case2 lt2) = case2 lt2
-        OrdTrans (case2 lt1) (case1 refl) = case2 lt1
-        OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y)
+        OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c
+        OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc
+        OrdTrans a≤b b≤c | case1 refl | case2 a≤c = ordtrans a≤c <-osuc
+        OrdTrans a≤b b≤c | case2 a≤c | case1 refl = ordtrans a≤c <-osuc
+        OrdTrans a≤b b≤c | case2 a<b | case2 b<c = ordtrans (ordtrans a<b  b<c) <-osuc

OrdPreorder :   Preorder n n n
OrdPreorder  = record { Carrier = Ordinal
@@ -188,7 +202,7 @@
; _∼_   = _o≤_
; isPreorder   = record {
isEquivalence = record { refl = refl  ; sym = sym ; trans = trans }
-                ; reflexive     = case1
+                ; reflexive     = o≤-refl
; trans         = OrdTrans
}
}
@@ -199,3 +213,11 @@
→ ¬ p
FExists  {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )

+        record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
+          field
+            os→ : (x : Ordinal) → x o< maxordinal → Ordinal
+            os← : Ordinal → Ordinal
+            os←limit : (x : Ordinal) → os← x o< maxordinal
+            os-iso← : {x : Ordinal} →  os→  (os← x) (os←limit x) ≡ x
+            os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) →  os← (os→ x lt) ≡ x
+```
```--- a/cardinal.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/cardinal.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -29,49 +29,48 @@
-- we have to work on Ordinal to keep OD Level n
-- since we use p∨¬p which works only on Level n

-
-∋-p : (A x : OD ) → Dec ( A ∋ x )
+∋-p : (A x : HOD ) → Dec ( A ∋ x )
∋-p A x with ODC.p∨¬p O ( A ∋ x )
∋-p A x | case1 t = yes t
∋-p A x | case2 t = no t

-_⊗_  : (A B : OD) → OD
-A ⊗ B  = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } where
+_⊗_  : (A B : HOD) → HOD
+A ⊗ B  = record { od = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } } where
checkAB : { p : Ordinal } → def ZFProduct p → Set n
-    checkAB (pair x y) = def A x ∧ def B y
+    checkAB (pair x y) = odef A x ∧ odef B y

-func→od0  : (f : Ordinal → Ordinal ) → OD
-func→od0  f = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkfunc p ) } where
+func→od0  : (f : Ordinal → Ordinal ) → HOD
+func→od0  f = record { od = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkfunc p ) }}  where
checkfunc : { p : Ordinal } → def ZFProduct p → Set n
checkfunc (pair x y) = f x ≡ y

--  Power (Power ( A ∪ B )) ∋ ( A ⊗ B )

-Func :  ( A B : OD ) → OD
-Func A B = record { def = λ x → def (Power (A ⊗ B)) x }
+Func :  ( A B : HOD ) → HOD
+Func A B = record { od = record { def = λ x → odef (Power (A ⊗ B)) x }  }

-- power→ :  ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)

-func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD
+func→od : (f : Ordinal → Ordinal ) → ( dom : HOD ) → HOD
func→od f dom = Replace dom ( λ x →  < x , ord→od (f (od→ord x)) > )

-record Func←cd { dom cod : OD } {f : Ordinal }  : Set n where
+record Func←cd { dom cod : HOD } {f : Ordinal }  : Set n where
field
func-1 : Ordinal → Ordinal
func→od∈Func-1 :  Func dom cod ∋  func→od func-1 dom

-od→func : { dom cod : OD } → {f : Ordinal }  → def (Func dom cod ) f  → Func←cd {dom} {cod} {f}
-od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x {!!} ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where
+od→func : { dom cod : HOD } → {f : Ordinal }  → odef (Func dom cod ) f  → Func←cd {dom} {cod} {f}
+od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o {!!} ( λ y lt → lemma x {!!} ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where
lemma : Ordinal → Ordinal → Ordinal
-   lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y)
+   lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → odef (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y)
lemma x y | p | no n  = o∅
lemma x y | p | yes f∋y = lemma2 (proj1 (ODC.double-neg-eilm O ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y)
lemma2 : {p : Ordinal} → ord-pair p  → Ordinal
lemma2 (pair x1 y1) with ODC.decp O ( x1 ≡ x)
lemma2 (pair x1 y1) | yes p = y1
lemma2 (pair x1 y1) | no ¬p = o∅
-   fod : OD
-   fod = Replace dom ( λ x →  < x , ord→od (sup-o ( λ y → lemma (od→ord x) {!!} )) > )
+   fod : HOD
+   fod = Replace dom ( λ x →  < x , ord→od (sup-o {!!} ( λ y lt → lemma (od→ord x) {!!} )) > )

open Func←cd
@@ -91,18 +90,18 @@
--     X ---------------------------> Y
--          ymap   <-  def Y y
--
-record Onto  (X Y : OD )  : Set n where
+record Onto  (X Y : HOD )  : Set n where
field
xmap : Ordinal
ymap : Ordinal
-       xfunc : def (Func X Y) xmap
-       yfunc : def (Func Y X) ymap
-       onto-iso   : {y :  Ordinal  } → (lty : def Y y ) →
+       xfunc : odef (Func X Y) xmap
+       yfunc : odef (Func Y X) ymap
+       onto-iso   : {y :  Ordinal  } → (lty : odef Y y ) →
func-1 ( od→func {X} {Y} {xmap} xfunc ) ( func-1 (od→func  yfunc) y )  ≡ y

open Onto

-onto-restrict : {X Y Z : OD} → Onto X Y → Z ⊆ Y  → Onto X Z
+onto-restrict : {X Y Z : HOD} → Onto X Y → Z ⊆ Y  → Onto X Z
onto-restrict {X} {Y} {Z} onto  Z⊆Y = record {
xmap = xmap1
; ymap = zmap
@@ -114,23 +113,23 @@
xmap1 = od→ord (Select (ord→od (xmap onto)) {!!} )
zmap : Ordinal
zmap = {!!}
-       xfunc1 : def (Func X Z) xmap1
+       xfunc1 : odef (Func X Z) xmap1
xfunc1 = {!!}
-       zfunc : def (Func Z X) zmap
+       zfunc : odef (Func Z X) zmap
zfunc = {!!}
-       onto-iso1   : {z :  Ordinal  } → (ltz : def Z z ) → func-1 (od→func  xfunc1 )  (func-1 (od→func  zfunc ) z )  ≡ z
+       onto-iso1   : {z :  Ordinal  } → (ltz : odef Z z ) → func-1 (od→func  xfunc1 )  (func-1 (od→func  zfunc ) z )  ≡ z
onto-iso1   = {!!}

-record Cardinal  (X  : OD ) : Set n where
+record Cardinal  (X  : HOD ) : Set n where
field
cardinal : Ordinal
conto : Onto X (Ord cardinal)
cmax : ( y : Ordinal  ) → cardinal o< y → ¬ Onto X (Ord y)

-cardinal :  (X  : OD ) → Cardinal X
+cardinal :  (X  : HOD ) → Cardinal X
cardinal  X = record {
-       cardinal = sup-o ( λ x → proj1 ( cardinal-p {!!}) )
+       cardinal = sup-o {!!} ( λ x lt → proj1 ( cardinal-p {!!}) )
; conto = onto
; cmax = cmax
} where
@@ -138,24 +137,24 @@
cardinal-p x with ODC.p∨¬p O ( Onto X (Ord x)  )
cardinal-p x | case1 True  = record { proj1 = x  ; proj2 = yes True }
cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False }
-    S = sup-o (λ x → proj1 (cardinal-p {!!}))
-    lemma1 :  (x : Ordinal) → ((y : Ordinal) → y o< x → Lift (suc n) (y o< (osuc S) → Onto X (Ord y))) →
-                    Lift (suc n) (x o< (osuc S) → Onto X (Ord x) )
+    S = sup-o {!!} (λ x lt → proj1 (cardinal-p {!!}))
+    lemma1 :  (x : Ordinal) → ((y : Ordinal) → y o< x →  (y o< (osuc S) → Onto X (Ord y))) →
+                     (x o< (osuc S) → Onto X (Ord x) )
lemma1 x prev with trio< x (osuc S)
lemma1 x prev | tri< a ¬b ¬c with osuc-≡< a
-    lemma1 x prev | tri< a ¬b ¬c | case1 x=S = lift ( λ lt → {!!} )
-    lemma1 x prev | tri< a ¬b ¬c | case2 x<S = lift ( λ lt → lemma2 ) where
+    lemma1 x prev | tri< a ¬b ¬c | case1 x=S = ( λ lt → {!!} )
+    lemma1 x prev | tri< a ¬b ¬c | case2 x<S = ( λ lt → lemma2 ) where
lemma2 : Onto X (Ord x)
lemma2 with prev {!!} {!!}
-         ... | lift t = t {!!}
-    lemma1 x prev | tri≈ ¬a b ¬c = lift ( λ lt → ⊥-elim ( o<¬≡ b lt ))
-    lemma1 x prev | tri> ¬a ¬b c = lift ( λ lt → ⊥-elim ( o<> c lt ))
+         ... | t = {!!}
+    lemma1 x prev | tri≈ ¬a b ¬c = ( λ lt → ⊥-elim ( o<¬≡ b lt ))
+    lemma1 x prev | tri> ¬a ¬b c = ( λ lt → ⊥-elim ( o<> c lt ))
onto : Onto X (Ord S)
-    onto with TransFinite {λ x → Lift (suc n) ( x o< osuc S → Onto X (Ord x) ) } lemma1 S
-    ... | lift t = t <-osuc
+    onto with TransFinite {λ x →  ( x o< osuc S → Onto X (Ord x) ) } lemma1 S
+    ... | t = t <-osuc
cmax : (y : Ordinal) → S o< y → ¬ Onto X (Ord y)
-    cmax y lt ontoy = o<> lt (o<-subst  {_} {_} {y} {S}
-       (sup-o<  {λ x → proj1 ( cardinal-p {!!})}{{!!}}  ) lemma refl ) where
+    cmax y lt ontoy = o<> lt (o<-subst  {_} {_} {y} {S} {!!} lemma refl ) where
+       -- (sup-o<  ? {λ x lt → proj1 ( cardinal-p {!!})}{{!!}}  ) lemma refl ) where
lemma : proj1 (cardinal-p y) ≡ y
lemma with  ODC.p∨¬p O ( Onto X (Ord y) )
lemma | case1 x = refl```
```--- a/filter.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/filter.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -13,80 +13,143 @@
open import Relation.Binary.Core
open import  Relation.Binary.PropositionalEquality
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
+import BAlgbra
+
+open BAlgbra O

open inOrdinal O
open OD O
open OD.OD
open ODAxiom odAxiom

+import ODC
+
open _∧_
open _∨_
open Bool

-_∩_ : ( A B : OD  ) → OD
-A ∩ B = record { def = λ x → def A x ∧ def B x }
-
-_∪_ : ( A B : OD  ) → OD
-A ∪ B = record { def = λ x → def A x ∨ def B x }
-
-_＼_ : ( A B : OD  ) → OD
-A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) }
-
-
-record Filter  ( L : OD  ) : Set (suc n) where
+-- Kunen p.76 and p.53, we use ⊆
+record Filter  ( L : HOD  ) : Set (suc n) where
field
-       filter : OD
-       proper : ¬ ( filter ∋ od∅ )
-       inL :  filter ⊆ L
-       filter1 : { p q : OD } →  q ⊆ L  → filter ∋ p →  p ⊆ q  → filter ∋ q
-       filter2 : { p q : OD } → filter ∋ p →  filter ∋ q  → filter ∋ (p ∩ q)
+       filter : HOD
+       f⊆PL :  filter ⊆ Power L
+       filter1 : { p q : HOD } →  q ⊆ L  → filter ∋ p →  p ⊆ q  → filter ∋ q
+       filter2 : { p q : HOD } → filter ∋ p →  filter ∋ q  → filter ∋ (p ∩ q)

open Filter

-L⊆L : (L : OD) → L ⊆ L
-L⊆L L = record { incl = λ {x} lt → lt }
+record prime-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where
+   field
+       proper  : ¬ (filter P ∋ od∅)
+       prime   : {p q : HOD } →  filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
+
+record ultra-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where
+   field
+       proper  : ¬ (filter P ∋ od∅)
+       ultra   : {p : HOD } → p ⊆ L →  ( filter P ∋ p ) ∨ (  filter P ∋ ( L ＼ p) )

-L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L
-L-filter {L} P {p} lt = filter1 P {p} {L} (L⊆L L) lt {!!}
+open _⊆_
+
+trans-⊆ :  { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C
+trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) }

-prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n
-prime-filter {L} P {p} {q} =  filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
+power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
+power→⊆ A t  PA∋t = record { incl = λ {x} t∋x → ODC.double-neg-eilm O (t1 t∋x) } where
+   t1 : {x : HOD }  → t ∋ x → ¬ ¬ (A ∋ x)
+   t1 = zf.IsZF.power→ isZF A t PA∋t

-ultra-filter :  {L : OD} → Filter L → ∀ {p : OD } → Set n
-ultra-filter {L} P {p} = L ∋ p →  ( filter P ∋ p ) ∨ (  filter P ∋ ( L ＼ p) )
+∈-filter : {L p : HOD} → (P : Filter L ) → filter P ∋ p → p ⊆ L
+∈-filter {L} {p} P lt = power→⊆ L p ( incl (f⊆PL P) lt )

+∪-lemma1 : {L p q : HOD } → (p ∪ q)  ⊆ L → p ⊆ L
+∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) }
+
+∪-lemma2 : {L p q : HOD } → (p ∪ q)  ⊆ L → q ⊆ L
+∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) }

-filter-lemma1 :  {L : OD} → (P : Filter L)  → ∀ {p q : OD } → ( ∀ (p : OD ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q}
-filter-lemma1 {L} P {p} {q} u lt = {!!}
+q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q
+q∩q⊆q = record { incl = λ lt → proj1 lt }

-filter-lemma2 :  {L : OD} → (P : Filter L)  → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) →  ∀ (p : OD ) → ultra-filter {L} P {p}
-filter-lemma2 {L} P prime p with prime {!!}
-... | t = {!!}
+open HOD
+_=h=_ : (x y : HOD) → Set n
+x =h= y  = od x == od y
+
+-----
+--
+--  ultra filter is prime
+--

-generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
-generated-filter {L} P p = record {
-     proper = {!!} ;
-     filter = {!!}  ; inL = {!!} ;
-     filter1 = {!!} ; filter2 = {!!}
-   }
+filter-lemma1 :  {L : HOD} → (P : Filter L)  → ∀ {p q : HOD } → ultra-filter P  → prime-filter P
+filter-lemma1 {L} P u = record {
+         proper = ultra-filter.proper u
+       ; prime = lemma3
+    } where
+  lemma3 : {p q : HOD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
+  lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) )
+  ... | case1 p∈P  = case1 p∈P
+  ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where
+    lemma5 : ((p ∪ q ) ∩ (L ＼ p)) =h=  (q ∩ (L ＼ p))
+    lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt  }
+       ;  eq← = λ {x} lt → record { proj1 = case2 (proj1 lt) ; proj2 = proj2 lt }
+      } where
+         lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L ＼ p)) x → odef q x
+         lemma4 x lt with proj1 lt
+         lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
+         lemma4 x lt | case2 qx = qx
+    lemma6 : filter P ∋ ((p ∪ q ) ∩ (L ＼ p))
+    lemma6 = filter2 P lt ¬p∈P
+    lemma7 : filter P ∋ (q ∩ (L ＼ p))
+    lemma7 =  subst (λ k → filter P ∋ k ) (==→o≡ lemma5 ) lemma6
+    lemma8 : (q ∩ (L ＼ p)) ⊆ q
+    lemma8 = q∩q⊆q

-record Dense  (P : OD ) : Set (suc n) where
-   field
-       dense : OD
-       incl :  dense ⊆ P
-       dense-f : OD → OD
-       dense-p :  { p : OD} → P ∋ p  → p ⊆ (dense-f p)
+-----
+--
+--  if Filter contains L, prime filter is ultra
+--

--- H(ω,2) = Power ( Power ω ) = Def ( Def ω))
+filter-lemma2 :  {L : HOD} → (P : Filter L)  → filter P ∋ L → prime-filter P → ultra-filter P
+filter-lemma2 {L} P f∋L prime = record {
+         proper = prime-filter.proper prime
+       ; ultra = λ {p}  p⊆L → prime-filter.prime prime (lemma p  p⊆L)
+   } where
+        open _==_
+        p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L ＼ p))
+        eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x)
+        eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x
+        eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p })
+        eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef L k ) diso (incl p⊆L ( subst (λ k → odef p k) (sym diso) p∋x  ))
+        eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p  ) = proj1 ¬p
+        lemma : (p : HOD) → p ⊆ L   →  filter P ∋ (p ∪ (L ＼ p))
+        lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L

-infinite = ZF.infinite OD→ZF
-
-module in-countable-ordinal {n : Level} where
+record Dense  (P : HOD ) : Set (suc n) where
+   field
+       dense : HOD
+       incl :  dense ⊆ P
+       dense-f : HOD → HOD
+       dense-d :  { p : HOD} → P ∋ p  → dense ∋ dense-f p
+       dense-p :  { p : HOD} → P ∋ p  →  p ⊆ (dense-f p)

-   import ordinal
+--    the set of finite partial functions from ω to 2
+--
+--   ph2 : Nat → Set → 2
+--   ph2 : Nat → Maybe 2
+--
+-- Hω2 : Filter (Power (Power infinite))

-   -- open  ordinal.C-Ordinal-with-choice
-   -- both Power and infinite is too ZF, it is better to use simpler one
-   Hω2 : Filter (Power (Power infinite))
-   Hω2 = {!!}
+record Ideal  ( L : HOD  ) : Set (suc n) where
+   field
+       ideal : HOD
+       i⊆PL :  ideal ⊆ Power L
+       ideal1 : { p q : HOD } →  q ⊆ L  → ideal ∋ p →  q ⊆ p  → ideal ∋ q
+       ideal2 : { p q : HOD } → ideal ∋ p →  ideal ∋ q  → ideal ∋ (p ∪ q)

+open Ideal
+
+proper-ideal : {L : HOD} → (P : Ideal L ) → {p : HOD} → Set n
+proper-ideal {L} P {p} = ideal P ∋ od∅
+
+prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n
+prime-ideal {L} P {p} {q} =  ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )
+```
```--- a/ordinal.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/ordinal.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -211,6 +211,7 @@
; o∅ = o∅
; osuc = osuc
; _o<_ = _o<_
+   ; next = next
; isOrdinal = record {
Otrans = ordtrans
; OTri = trio<
@@ -218,14 +219,36 @@
; <-osuc = <-osuc
; osuc-≡< = osuc-≡<
; TransFinite = TransFinite1
+     ; TransFinite1 = TransFinite2
+     ; not-limit = not-limit
+     ; next-limit = next-limit
}
} where
+     next : Ordinal {suc n} → Ordinal {suc n}
+     next (ordinal lv ord) = ordinal (Suc lv) (Φ (Suc lv))
+     next-limit : {y : Ordinal} → (y o< next y) ∧ ((x : Ordinal) → x o< next y → osuc x o< next y)
+     next-limit {y} = record { proj1 = case1 a<sa ; proj2 = lemma } where
+         lemma :  (x : Ordinal) → x o< next y → osuc x o< next y
+         lemma x (case1 lt) = case1 lt
+     not-limit : (x : Ordinal) → Dec (¬ ((y : Ordinal) → ¬ (x ≡ osuc y)))
+     not-limit (ordinal lv (Φ lv)) = no (λ not → not (λ y () ))
+     not-limit (ordinal lv (OSuc lv ox)) = yes (λ not → not (ordinal lv ox) refl )
ord1 : Set (suc n)
ord1 = Ordinal {suc n}
-     TransFinite1 : { ψ : ord1  → Set (suc (suc n)) }
+     TransFinite1 : { ψ : ord1  → Set (suc n) }
→ ( (x : ord1)  → ( (y : ord1  ) → y o< x → ψ y ) → ψ x )
→  ∀ (x : ord1)  → ψ x
-     TransFinite1 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where
+     TransFinite1 {ψ} lt x = TransFinite {n} {suc n} {ψ} caseΦ caseOSuc x where
+        caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
+            ψ (record { lv = lx ; ord = Φ lx })
+        caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev
+        caseOSuc :  (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
+            ψ (record { lv = lx ; ord = OSuc lx x₁ })
+        caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev
+     TransFinite2 : { ψ : ord1  → Set (suc (suc n)) }
+          → ( (x : ord1)  → ( (y : ord1  ) → y o< x → ψ y ) → ψ x )
+          →  ∀ (x : ord1)  → ψ x
+     TransFinite2 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where
caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
ψ (record { lv = lx ; ord = Φ lx })
caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev
@@ -233,3 +256,4 @@
ψ (record { lv = lx ; ord = OSuc lx x₁ })
caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev

+```
```--- a/zf.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/zf.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -49,7 +49,7 @@
-- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
extensionality :  { A B w : ZFSet  } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z)  ) → ( A ∈ w ⇔ B ∈ w )
-- regularity without minimum
-     ε-induction : { ψ : ZFSet → Set (suc m)}
+     ε-induction : { ψ : ZFSet → Set m}
→ ( {x : ZFSet } → ({ y : ZFSet } →  x ∋ y → ψ y ) → ψ x )
→ (x : ZFSet ) → ψ x
-- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )```