Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff OD.agda @ 396:8c092c042093
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 27 Jul 2020 15:11:54 +0900 |
parents | 77c6123f49ee |
children | 382a4a411aff |
line wrap: on
line diff
--- a/OD.agda Mon Jul 27 09:29:41 2020 +0900 +++ b/OD.agda Mon Jul 27 15:11:54 2020 +0900 @@ -139,20 +139,15 @@ odef : HOD → Ordinal → Set n odef A x = def ( od A ) x --- If we have reverse of c<→o<, everything becomes Ordinal -o<→c<→HOD=Ord : ( o<→c< : {x y : Ordinal } → x o< y → odef (ord→od y) x ) → {x : HOD } → x ≡ Ord (od→ord x) -o<→c<→HOD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where - lemma1 : {y : Ordinal} → odef x y → odef (Ord (od→ord x)) y - lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (subst (λ k → odef x k ) (sym diso) lt)) - lemma2 : {y : Ordinal} → odef (Ord (od→ord x)) y → odef x y - lemma2 {y} lt = subst (λ k → odef k y ) oiso (o<→c< {y} {od→ord x} lt ) - _∋_ : ( a x : HOD ) → Set n _∋_ a x = odef a ( od→ord x ) _c<_ : ( x a : HOD ) → Set n x c< a = a ∋ x +d→∋ : ( a : HOD ) { x : Ordinal} → odef a x → a ∋ (ord→od x) +d→∋ a lt = subst (λ k → odef a k ) (sym diso) lt + cseq : HOD → HOD cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x) @@ -170,6 +165,14 @@ odefo→o< : {X y : Ordinal } → odef (ord→od X) y → y o< X odefo→o< {X} {y} lt = subst₂ (λ j k → j o< k ) diso diso ( c<→o< (subst (λ k → odef (ord→od X) k ) (sym diso ) lt )) +-- If we have reverse of c<→o<, everything becomes Ordinal +o<→c<→HOD=Ord : ( o<→c< : {x y : Ordinal } → x o< y → odef (ord→od y) x ) → {x : HOD } → x ≡ Ord (od→ord x) +o<→c<→HOD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where + lemma1 : {y : Ordinal} → odef x y → odef (Ord (od→ord x)) y + lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (d→∋ x lt)) + lemma2 : {y : Ordinal} → odef (Ord (od→ord x)) y → odef x y + lemma2 {y} lt = subst (λ k → odef k y ) oiso (o<→c< {y} {od→ord x} lt ) + -- avoiding lv != Zero error orefl : { x : HOD } → { y : Ordinal } → od→ord x ≡ y → od→ord x ≡ y orefl refl = refl @@ -263,7 +266,6 @@ odmax<od→ord : { x y : HOD } → x ∋ y → Set n odmax<od→ord {x} {y} x∋y = odmax x o< od→ord x --- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n) in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → OD @@ -287,7 +289,7 @@ refl-⊆ {A} = record { incl = λ x → x } od⊆→o≤ : {x y : HOD } → x ⊆ y → od→ord x o< osuc (od→ord y) -od⊆→o≤ {x} {y} lt = ⊆→o≤ {x} {y} (λ {z} x>z → 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<y = subst₂ (λ j k → j o< k ) diso diso (c<→o< (subst (λ k → def (od (ord→od x)) k) (sym diso) x<y)) + lemma0 {x} x<y = subst₂ (λ j k → j o< k ) diso diso (c<→o< (d→∋ (ord→od x) x<y )) lemma2 : {x : Ordinal} → def (od U) x → x o< od→ord U - lemma2 {x} x<U = subst (λ k → k o< od→ord U ) diso (c<→o< (subst (λ k → def (od U) k) (sym diso) x<U)) + lemma2 {x} x<U = subst (λ k → k o< od→ord U ) diso (c<→o< (d→∋ U x<U)) lemma1 : {x : Ordinal} → def (od U) x ∧ def (od (ord→od x)) y → ¬ (od→ord U o< y) lemma1 {x} lt u<y = o<> u<y (ordtrans (lemma0 (proj2 lt)) (lemma2 (proj1 lt)) ) lemma : ¬ ((od→ord U) o< y ) → y o< osuc (od→ord U) @@ -455,6 +454,18 @@ _=h=_ : (x y : HOD) → Set n x =h= y = od x == od y +open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) + +ord∋eq : {n : Level } {A i : HOD } → { f : (x : HOD ) → A ∋ x → Set n} + → ( ( x : Ordinal ) → ( lx : odef A x ) → f (ord→od x) (d→∋ A lx) ) + → ( lt : A ∋ i ) → f i lt +ord∋eq {n} {A} {i} {f} of lt = subst (λ k → odef A k ) ? (of (od→ord i) ?) + +nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i +nat→ω-iso {i} lt = ord∋eq {_} {infinite} {i} (λ x lx → lemma lx ) lt where + lemma : {x : Ordinal} → (lx : infinite-d x ) → nat→ω ( ω→nat (ord→od x) (d→∋ infinite lx) ) ≡ ord→od x + lemma = {!!} + infixr 200 _∈_ -- infixr 230 _∩_ _∪_ @@ -485,7 +496,7 @@ union← : (X z : HOD) (X∋z : Union X ∋ z) → ¬ ( (u : HOD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) union← X z UX∋z = FExists _ lemma UX∋z where lemma : {y : Ordinal} → odef X y ∧ odef (ord→od y) (od→ord z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z)) - lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → odef X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } + lemma {y} xx not = not (ord→od y) record { proj1 = d→∋ X (proj1 xx) ; proj2 = proj2 xx } ψiso : {ψ : HOD → Set n} {x y : HOD } → ψ x → x ≡ y → ψ y ψiso {ψ} t refl = t @@ -525,7 +536,7 @@ ∩-≡ : { a b : HOD } → ({x : HOD } → (a ∋ x → b ∋ x)) → a =h= ( b ∩ a ) ∩-≡ {a} {b} inc = record { eq→ = λ {x} x<a → record { proj2 = x<a ; - proj1 = odef-subst {_} {_} {b} {x} (inc (odef-subst {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ; + proj1 = odef-subst {_} {_} {b} {x} (inc (d→∋ a x<a)) refl diso } ; eq← = λ {x} x<a∩b → proj2 x<a∩b } -- -- Transitive Set case @@ -540,12 +551,12 @@ eq→ lemma-eq {z} w = proj2 w eq← lemma-eq {z} w = record { proj2 = w ; proj1 = odef-subst {_} {_} {(Ord a)} {z} - ( t→A (odef-subst {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso } + ( t→A (d→∋ t w)) refl diso } lemma1 : {a : Ordinal } { t : HOD } → (eq : ((Ord a) ∩ t) =h= t) → od→ord ((Ord a) ∩ (ord→od (od→ord t))) ≡ od→ord t lemma1 {a} {t} eq = subst (λ k → od→ord ((Ord a) ∩ k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq )) lemma2 : (od→ord t) o< (osuc (od→ord (Ord a))) - lemma2 = ⊆→o≤ {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) diso (t→A (subst (λ k → def (od t) k) (sym diso) x<t))) + lemma2 = ⊆→o≤ {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) diso (t→A (d→∋ t x<t))) lemma : od→ord ((Ord a) ∩ (ord→od (od→ord t)) ) o< sup-o (Ord (osuc (od→ord (Ord a)))) (λ x lt → od→ord ((Ord a) ∩ (ord→od x))) lemma = sup-o< _ lemma2 @@ -591,7 +602,7 @@ lemmab : od→ord ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A) )))) o< sup1 lemmab = sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 lemmad : Ord (osuc (od→ord A)) ∋ t - lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) diso (t→A (subst (λ k → def (od t) k ) (sym diso) lt))) + lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) diso (t→A (d→∋ t lt))) lemmac : ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A) )))) =h= Ord (od→ord A) lemmac = record { eq→ = lemmaf ; eq← = lemmag } where lemmaf : {x : Ordinal} → def (od ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A)))))) x → def (od (Ord (od→ord A))) x