--- a/ODC.agda	Sun Jul 05 15:49:00 2020 +0900
+++ b/ODC.agda	Sun Jul 05 16:56:21 2020 +0900
@@ -23,6 +23,8 @@
 
 open HOD
 
+open _∧_
+
 _=h=_ : (x y : HOD) → Set n
 x =h= y  = od x == od y
 
@@ -40,26 +42,29 @@
 --     https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
 --
 
-ppp :  { p : Set n } { a : HOD  } → record { od = record { def = λ x → p } ; odmax = {!!} ; <odmax = {!!} } ∋ 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 { 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
+p∨¬p : ( p : Set n ) → p ∨ ( ¬ p )         -- assuming axiom of choice
+p∨¬p  p with is-o∅ ( od→ord (pred-od p ))
+p∨¬p  p | yes eq = case2 (¬p eq) where
+   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 =h=  k ) oiso 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∅  → 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))
 
 decp : ( p : Set n ) → Dec p   -- assuming axiom of choice    
 decp  p with p∨¬p p