diff OD.agda @ 183:de3d87b7494f

fix zf
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 21 Jul 2019 17:56:12 +0900
parents 9f3c0e0b2bc9
children 65e1b2e415bb
line wrap: on
line diff
--- a/OD.agda	Sun Jul 21 12:11:50 2019 +0900
+++ b/OD.agda	Sun Jul 21 17:56:12 2019 +0900
@@ -71,10 +71,11 @@
   -- sup-x  : {n : Level } → ( Ordinal {n} → Ordinal {n}) →  Ordinal {n}
   -- sup-lb : {n : Level } → { ψ : Ordinal {n} →  Ordinal {n}} → {z : Ordinal {n}}  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
   -- sup-lb : {n : Level } → ( ψ : Ordinal {n} →  Ordinal {n}) → ( ∀ {x : Ordinal {n}} →  ψx  o<  z ) →  z o< osuc ( sup-o ψ ) 
-  -- mimimul and x∋minimul is a weaker form of Axiom of choice
+  -- mimimul and x∋minimul is an Axiom of choice
   minimul : {n : Level } → (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 
   -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
   x∋minimul : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) )
+  -- 
   minimul-1 : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → (y : OD {suc n}) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord  y) )
 
 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n
@@ -292,13 +293,14 @@
        ;   power→ = power→  
        ;   power← = power← 
        ;   extensionality = extensionality
-       ;   minimul = minimul
-       ;   regularity = regularity
+       ;   ε-induction = ε-induction
        ;   infinity∅ = infinity∅
        ;   infinity = infinity
        ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
        ;   replacement← = replacement←
        ;   replacement→ = replacement→
+       ;   choice-func = choice-func
+       ;   choice = choice
      } where
 
          pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧  ((A , B) ∋ B)