--- a/OD.agda	Thu Jul 25 14:42:19 2019 +0900
+++ b/OD.agda	Fri Jul 26 21:08:06 2019 +0900
@@ -198,7 +198,7 @@
 -- Axiom of choice in intutionistic logic implies the exclude middle
 --     https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
 --
-p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )
+p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )         -- assuming axiom of choice
 p∨¬p {n} p with is-o∅ ( od→ord ( record { def = λ x → p } ))
 p∨¬p {n} p | yes eq = case2 (¬p eq) where
    ps = record { def = λ x → p }
@@ -213,13 +213,13 @@
    lemma : ps ∋ minimul ps (λ eq →  ¬p (eqo∅ eq)) 
    lemma = x∋minimul ps (λ eq →  ¬p (eqo∅ eq))
 
-∋-p : { n : Level } → ( p : Set (suc n) ) → Dec p 
+∋-p : { n : Level } → ( p : Set (suc n) ) → Dec p   -- assuming axiom of choice    
 ∋-p {n} p with p∨¬p p
 ∋-p {n} p | case1 x = yes x
 ∋-p {n} p | case2 x = no x
 
 double-neg-eilm : {n  : Level } {A : Set (suc n)} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
-double-neg-eilm {n} {A} notnot with ∋-p  A
+double-neg-eilm {n} {A} notnot with ∋-p  A                         -- assuming axiom of choice
 ... | yes p = p
 ... | no ¬p = ⊥-elim ( notnot ¬p )
 
@@ -243,6 +243,24 @@
 Def :  {n : Level} → (A :  OD {suc n}) → OD {suc n}
 Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   -- Ord x does not help ord-power→
 
+
+_⊆_ : {n : Level} ( A B : OD {suc n}  ) → ∀{ x : OD {suc n} } →  Set (suc n)
+_⊆_ A B {x} = A ∋ x →  B ∋ x
+
+infixr  220 _⊆_
+
+subset-lemma : {n : Level} → {A x y : OD {suc n} } → (  x ∋ y → ZFSubset A x ∋  y ) ⇔  ( _⊆_ x A {y} )
+subset-lemma {n} {A} {x} {y} = record {
+      proj1 = λ z lt → proj1 (z  lt)
+    ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt }
+   } 
+
+Def=A→Set : {n : Level} → (A  :  Ordinal {suc n}) → Def (Ord A) == record { def = λ x → x o< A → Set n  }
+Def=A→Set {n} A  = record {
+              eq→ = λ {y} DAx y<A →  {!!}
+        ;  eq← = {!!} -- λ {y} f → {!!}
+    } where
+
 -- Constructible Set on α
 -- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y <  od→ord x } 
 -- L (Φ 0) = Φ
@@ -285,8 +303,6 @@
     Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x)))  }
     _∈_ : ( A B : ZFSet  ) → Set (suc n)
     A ∈ B = B ∋ A
-    _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set (suc n)
-    _⊆_ A B {x} = A ∋ x →  B ∋ x
     Power : OD {suc n} → OD {suc n}
     Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
     ｛_｝ : ZFSet → ZFSet
@@ -302,7 +318,6 @@
 
     infixr  200 _∈_
     -- infixr  230 _∩_ _∪_
-    infixr  220 _⊆_
     isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace infinite
     isZF = record {
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
@@ -446,6 +461,7 @@
                   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  )))
 
+         --  assuming axiom of choice
          regularity :  (x : OD) (not : ¬ (x == od∅)) →
             (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
          proj1 (regularity x not ) = x∋minimul x not