--- a/ODC.agda	Sun Jul 05 11:40:55 2020 +0900
+++ b/ODC.agda	Sun Jul 05 12:32:09 2020 +0900
@@ -21,13 +21,18 @@
 open OD._==_
 open ODAxiom odAxiom
 
+open HOD
+
+_=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 ) )
+  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 )
-  minimal-1 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
+  minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord  y) )
 
 
 --
@@ -35,23 +40,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
+-- ppp :  { p : Set n } { a : HOD  } → record { def = λ x → p } ∋ a → p
+-- ppp  {p} {a} d = 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 | 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 )
-   ¬p : (od→ord ps ≡ o∅) → p → ⊥
-   ¬p eq = lemma ( subst₂ (λ j k → j ==  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∅  
-   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))
+-- p∨¬p : ( p : Set n ) → p ∨ ( ¬ p )         -- assuming axiom of choice
+-- p∨¬p  p with is-o∅ ( od→ord ( record { odef = λ x → p } ))
+-- p∨¬p  p | yes eq = case2 (¬p eq) where
+--    ps = record { odef = λ x → p }
+--    lemma : ps =h= od∅ → p → ⊥
+--    lemma eq p0 = ¬x<0  {od→ord ps} (eq→ eq p0 )
+--    ¬p : (od→ord ps ≡ o∅) → p → ⊥
+--    ¬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 { odef = λ x → 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))
+
+postulate 
+   p∨¬p : ( p : Set n ) → p ∨ ( ¬ p )         -- assuming axiom of choice
 
 decp : ( p : Set n ) → Dec p   -- assuming axiom of choice    
 decp  p with p∨¬p p
@@ -63,7 +71,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 +79,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