# HG changeset patch # User Shinji KONO # Date 1595830314 -32400 # Node ID 8c092c04209360e5de9a661061aa2906f9977987 # Parent 77c6123f49eed335d629bbb34b10351834db661d ... diff -r 77c6123f49ee -r 8c092c042093 BAlgbra.agda --- a/BAlgbra.agda Mon Jul 27 09:29:41 2020 +0900 +++ b/BAlgbra.agda Mon Jul 27 15:11:54 2020 +0900 @@ -51,9 +51,9 @@ lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not) -- choice lemma2 : {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A - (record { proj1 = case1 refl ; proj2 = subst (λ k → odef A k) (sym diso) A∋x})) + (record { proj1 = case1 refl ; proj2 = d→∋ A A∋x } )) lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B - (record { proj1 = case2 refl ; proj2 = subst (λ k → odef B k) (sym diso) B∋x})) + (record { proj1 = case2 refl ; proj2 = d→∋ B B∋x } )) ∩-Select : { A B : HOD } → Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) ≡ ( A ∩ B ) ∩-Select {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where @@ -61,7 +61,7 @@ lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → odef B k ) diso (proj2 (proj2 lt)) } lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x lemma2 {x} lt = record { proj1 = proj1 lt ; proj2 = - record { proj1 = subst (λ k → odef A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → odef B k ) (sym diso) (proj2 lt) } } + record { proj1 = d→∋ A (proj1 lt) ; proj2 = d→∋ B (proj2 lt) } } dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r ) dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where diff -r 77c6123f49ee -r 8c092c042093 LEMC.agda --- 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 yz → subst (λ k → def (od y) k ) diso (incl lt (subst (λ k → def (od x) k ) (sym diso) x>z ))) +od⊆→o≤ {x} {y} lt = ⊆→o≤ {x} {y} (λ {z} x>z → subst (λ k → def (od y) k ) diso (incl lt (d→∋ x x>z))) -- if we have od→ord (x , x) ≡ osuc (od→ord x), ⊆→o≤ → c<→o< ⊆→o≤→c<→o< : ({x : HOD} → od→ord (x , x) ≡ osuc (od→ord x) ) @@ -315,7 +317,7 @@ power< : {A x : HOD } → x ⊆ A → Ord (osuc (od→ord A)) ∋ x power< {A} {x} x⊆A = ⊆→o≤ (λ {y} x∋y → subst (λ k → def (od A) k) diso (lemma y x∋y ) ) where lemma : (y : Ordinal) → def (od x) y → def (od A) (od→ord (ord→od y)) - lemma y x∋y = incl x⊆A (subst (λ k → def (od x) k ) (sym diso) x∋y ) + lemma y x∋y = incl x⊆A (d→∋ x x∋y) open import Data.Unit @@ -349,9 +351,6 @@ rmax< : {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax rmax< lt = proj1 lt -d→∋ : ( a : HOD ) { x : Ordinal} → odef a x → a ∋ (ord→od x) -d→∋ a lt = subst (λ k → odef a k ) (sym diso) lt - -- -- If we have LEM, Replace' is equivalent to Replace -- @@ -371,9 +370,9 @@ umax< : {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (ord→od u)) y) → y o< osuc (od→ord U) umax< {y} not = lemma (FExists _ lemma1 not ) where lemma0 : {x : Ordinal} → def (od (ord→od x)) y → y o< x - lemma0 {x} x u