Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 196:a3211dcb4d83

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 29 Jul 2019 11:58:10 +0900
parents 0cefb1e4d2cc
children b114cf5b9130
files OD.agda
diffstat 1 files changed, 8 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Mon Jul 29 11:49:58 2019 +0900
+++ b/OD.agda	Mon Jul 29 11:58:10 2019 +0900
@@ -558,16 +558,20 @@
                                lx ≡ ly → ly ≡ lv (od→ord z)  → ψ z 
                           lemma6 {ly} {ox} {oy} refl refl = lemma5 (OSuc lx (ord (od→ord z)) ) (case2 s<refl)
 
-         choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) )  → ¬ ( X == od∅ ) → OD {suc n}
+         record choiced {n : Level} ( X : OD {suc n}) : Set (suc (suc n)) where
+            field
+                a-choice : OD {suc n}
+                is-in : X ∋ a-choice
+         choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) )  → ¬ ( X == od∅ ) → choiced X
          choice-func' X ∋-p not = lemma-ord (lv (osuc (od→ord X))) (ord (osuc (od→ord X)))  <-osuc
            where
             lemma-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly }
-                → (ly < lx) ∨ (oy d< ox  ) → OD {suc n}
+                → (ly < lx) ∨ (oy d< ox  ) → choiced X
             lemma-ord Zero (Φ 0) (case1 ())
             lemma-ord Zero (Φ 0) (case2 ())
             lemma-ord lx (OSuc lx ox) lt with ∋-p X (ord→od record { lv = lx ; ord = OSuc lx ox })
-            lemma-ord lx (OSuc lx ox) lt | yes p = ord→od record { lv = lx ; ord = OSuc lx ox }
+            lemma-ord lx (OSuc lx ox) lt | yes p = record { a-choice = ord→od record { lv = lx ; ord = OSuc lx ox } ; is-in = p } 
             lemma-ord lx (OSuc lx ox) {ly} {oy} lt | no ¬p = lemma-ord lx ox {ly} {oy} {!!}
             lemma-ord (Suc lx) (Φ (Suc lx)) lt with ∋-p X (ord→od record { lv = Suc lx ; ord = Φ (Suc lx)})
-            lemma-ord (Suc lx) (Φ (Suc lx)) lt | yes p = ord→od record { lv = Suc lx ; ord = Φ (Suc lx)}
+            lemma-ord (Suc lx) (Φ (Suc lx)) lt | yes p =  record { a-choice =  ord→od record { lv = Suc lx ; ord = Φ (Suc lx)}  ; is-in = p }
             lemma-ord (Suc lx) (Φ .(Suc lx)) {ly} {oy} (case1 lt ) | no ¬p = {!!}