diff LEMC.agda @ 396:8c092c042093

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 27 Jul 2020 15:11:54 +0900
parents 19687f3304c9
children 44a484f17f26
line wrap: on
line diff
--- a/LEMC.agda	Mon Jul 27 09:29:41 2020 +0900
+++ b/LEMC.agda	Mon Jul 27 15:11:54 2020 +0900
@@ -45,7 +45,7 @@
 power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
 power→⊆ A t  PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (λ not → t1 t∋x (λ x → not x) ) } where
    t1 : {x : HOD }  → t ∋ x → ¬ ¬ (A ∋ x)
-   t1 = zf.IsZF.power→ isZF A t PA∋t
+   t1 = power→ A t PA∋t
 
 --- With assuption of HOD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
 ---
@@ -110,7 +110,7 @@
                          lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced (od→ord X)
                          lemma1 y with ∋-p X (ord→od y)
                          lemma1 y | yes y<X = case2 ( record { a-choice = y ; is-in = ∋oo y<X } )
-                         lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → odef X k ) (sym diso) y<X ) )
+                         lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (d→∋ X y<X) )
                          lemma :  ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced (od→ord X)
                          lemma = ∀-imply-or lemma1
                  have_to_find : choiced (od→ord X)
@@ -148,7 +148,7 @@
                  lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u)
                  lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt))
               np : ¬ (p =h= od∅)
-              np p∅ =  NP (λ y p∋y → ∅< {p} {_} (subst (λ k → odef p k) (sym diso) p∋y) p∅ ) 
+              np p∅ =  NP (λ y p∋y → ∅< {p} {_} (d→∋ p p∋y) p∅ ) 
               y1choice : choiced (od→ord p)
               y1choice = choice-func p np
               y1 : HOD