--- a/src/ODC.agda	Mon Jan 02 10:15:20 2023 +0900
+++ b/src/ODC.agda	Tue Jan 03 09:28:23 2023 +0900
@@ -4,9 +4,9 @@
 module ODC {n : Level } (O : Ordinals {n} ) where
 
 open import zf
-open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
 open import  Relation.Binary.PropositionalEquality
-open import Data.Nat.Properties 
+open import Data.Nat.Properties
 open import Data.Empty
 open import Relation.Nullary
 open import Relation.Binary
@@ -35,9 +35,9 @@
 
 open _∧_
 
-postulate      
+postulate
   -- mimimul and x∋minimal is an Axiom of choice
-  minimal : (x : HOD  ) → ¬ (x =h= od∅ )→ HOD 
+  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 ( & ( minimal x ne ) )
   -- minimality (proved by ε-induction with LEM)
@@ -51,7 +51,7 @@
 
 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 } 
+   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
@@ -59,32 +59,32 @@
 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p )         -- assuming axiom of choice
 p∨¬p  p with is-o∅ ( & (pred-od p ))
 p∨¬p  p | yes eq = case2 (¬p eq) where
-   ps = pred-od p 
-   eqo∅ : ps =h=  od∅  → & ps ≡  o∅  
-   eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq)) 
+   ps = pred-od p
+   eqo∅ : ps =h=  od∅  → & ps ≡  o∅
+   eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq))
    lemma : ps =h= od∅ → p → ⊥
    lemma eq p0 = ¬x<0  {& ps} (eq→ eq record { proj1 = eqo∅ eq ; proj2 = p0 } )
    ¬p : (& ps ≡ o∅) → p → ⊥
    ¬p eq = lemma ( subst₂ (λ j k → j =h=  k ) *iso o∅≡od∅ ( o≡→== eq ))
 p∨¬p  p | no ¬p = case1 (ppp  {p} {minimal ps (λ eq →  ¬p (eqo∅ eq))} lemma) where
-   ps = pred-od p 
-   eqo∅ : ps =h=  od∅  → & ps ≡  o∅  
-   eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq)) 
-   lemma : ps ∋ minimal ps (λ eq →  ¬p (eqo∅ eq)) 
+   ps = pred-od p
+   eqo∅ : ps =h=  od∅  → & ps ≡  o∅
+   eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq))
+   lemma : ps ∋ minimal ps (λ eq →  ¬p (eqo∅ eq))
    lemma = x∋minimal ps (λ eq →  ¬p (eqo∅ eq))
 
-decp : ( p : Set n ) → Dec p   -- assuming axiom of choice    
+decp : ( p : Set n ) → Dec p   -- assuming axiom of choice
 decp  p with p∨¬p p
 decp  p | case1 x = yes x
 decp  p | case2 x = no x
 
-∋-p : (A x : HOD ) → Dec ( A ∋ x ) 
+∋-p : (A x : HOD ) → Dec ( A ∋ x )
 ∋-p A x with p∨¬p ( A ∋ x ) -- LEM
 ∋-p A x | case1 t  = yes t
 ∋-p A x | case2 t  = no (λ x → t x)
 
-double-neg-eilm : {A : Set n} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
-double-neg-eilm  {A} notnot with decp  A                         -- assuming axiom of choice
+double-neg-elim : {A : Set n} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
+double-neg-elim  {A} notnot with decp  A                         -- assuming axiom of choice
 ... | yes p = p
 ... | no ¬p = ⊥-elim ( notnot ¬p )
 
@@ -95,6 +95,18 @@
 or-exclude {A} {B} (case2 b) | case1 a = case1 a
 or-exclude {A} {B} (case2 b) | case2 ¬a = case2 ⟪ ¬a , b ⟫
 
+-- record By-contradiction (A : Set n) (B : A → Set n)  : Set (suc n) where
+--  field
+--     a : A
+--     b : B a
+-- 
+-- by-contradiction : {A : Set n} {B : A → Set n}  → ¬ ( (a : A ) → ¬ B a ) → By-contradiction A B
+-- by-contradiction {A} {B} not with p∨¬p A 
+-- ... | case2 ¬a  = ⊥-elim (not (λ a → ⊥-elim (¬a a  )))
+-- ... | case1 a with p∨¬p (B a)
+-- ... | case1 b  = record { a = a ; b = b }
+-- ... | case2 ¬b = ⊥-elim ( not ( λ a b → ⊥-elim ( ¬b ? )))
+-- 
 power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
 power→⊆ A t  PA∋t tx = subst (λ k → odef A k ) &iso ( power→ A t PA∋t (subst (λ k → odef t k) (sym &iso) tx ) )
 
@@ -112,10 +124,10 @@
 open import zfc
 
 HOD→ZFC : ZFC
-HOD→ZFC   = record { 
-    ZFSet = HOD 
-    ; _∋_ = _∋_ 
-    ; _≈_ = _=h=_ 
+HOD→ZFC   = record {
+    ZFSet = HOD
+    ; _∋_ = _∋_
+    ; _≈_ = _=h=_
     ; ∅  = od∅
     ; Select = Select
     ; isZFC = isZFC
@@ -128,9 +140,9 @@
        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 ) ] 
+         -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
          choice-func : (X : HOD  ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD
          choice-func X {x} not X∋x = minimal x not
-         choice : (X : HOD  ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= 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