Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 422:44a484f17f26
syntax *, &, ⟪ , ⟫
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 01 Aug 2020 11:06:29 +0900 |
| parents | cb067605fea0 |
| children | 9984cdd88da3 |
| files | BAlgbra.agda LEMC.agda OD.agda ODC.agda OPair.agda VL.agda cardinal.agda filter.agda generic-filter.agda logic.agda ordinal.agda |
| diffstat | 11 files changed, 432 insertions(+), 433 deletions(-) [+] |
line wrap: on
line diff
--- a/BAlgbra.agda Fri Jul 31 17:54:52 2020 +0900 +++ b/BAlgbra.agda Sat Aug 01 11:06:29 2020 +0900 @@ -13,7 +13,7 @@ open import Relation.Binary open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality -open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) +open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ; _+_ to _n+_ ) open inOrdinal O open OD O @@ -43,73 +43,72 @@ ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where lemma1 : {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x lemma1 {x} lt = lemma3 lt where - lemma4 : {y : Ordinal} → odef (A , B) y ∧ odef (ord→od y) x → ¬ (¬ ( odef A x ∨ odef B x) ) + lemma4 : {y : Ordinal} → odef (A , B) y ∧ odef (* y) x → ¬ (¬ ( odef A x ∨ odef B x) ) lemma4 {y} z with proj1 z - lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → odef k x ) oiso (proj2 z)) ) - lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → odef k x ) oiso (proj2 z)) ) - lemma3 : (((u : Ordinals.ord O) → ¬ odef (A , B) u ∧ odef (ord→od u) x) → ⊥) → odef (A ∪ B) x + lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → odef k x ) *iso (proj2 z)) ) + lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → odef k x ) *iso (proj2 z)) ) + lemma3 : (((u : Ordinals.ord O) → ¬ odef (A , B) u ∧ odef (* u) x) → ⊥) → odef (A ∪ B) x 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 = 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 = d→∋ B B∋x } )) + lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) A + ⟪ case1 refl , d→∋ A A∋x ⟫ ) + lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) B + ⟪ case2 refl , 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 lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x - lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → odef B k ) diso (proj2 (proj2 lt)) } + lemma1 {x} lt = ⟪ proj1 lt , subst (λ k → odef B k ) &iso (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 = d→∋ A (proj1 lt) ; proj2 = d→∋ B (proj2 lt) } } + lemma2 {x} lt = ⟪ proj1 lt , ⟪ d→∋ A (proj1 lt) , 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 lemma1 : {x : Ordinal} → odef (p ∩ (q ∪ r)) x → odef ((p ∩ q) ∪ (p ∩ r)) x lemma1 {x} lt with proj2 lt - lemma1 {x} lt | case1 q∋x = case1 ( record { proj1 = proj1 lt ; proj2 = q∋x } ) - lemma1 {x} lt | case2 r∋x = case2 ( record { proj1 = proj1 lt ; proj2 = r∋x } ) + lemma1 {x} lt | case1 q∋x = case1 ⟪ proj1 lt , q∋x ⟫ + lemma1 {x} lt | case2 r∋x = case2 ⟪ proj1 lt , r∋x ⟫ lemma2 : {x : Ordinal} → odef ((p ∩ q) ∪ (p ∩ r)) x → odef (p ∩ (q ∪ r)) x - lemma2 {x} (case1 p∩q) = record { proj1 = proj1 p∩q ; proj2 = case1 (proj2 p∩q ) } - lemma2 {x} (case2 p∩r) = record { proj1 = proj1 p∩r ; proj2 = case2 (proj2 p∩r ) } + lemma2 {x} (case1 p∩q) = ⟪ proj1 p∩q , case1 (proj2 p∩q ) ⟫ + lemma2 {x} (case2 p∩r) = ⟪ proj1 p∩r , case2 (proj2 p∩r ) ⟫ dist-ord2 : {p q r : HOD } → p ∪ ( q ∩ r ) ≡ ( p ∪ q ) ∩ ( p ∪ r ) dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where lemma1 : {x : Ordinal} → odef (p ∪ (q ∩ r)) x → odef ((p ∪ q) ∩ (p ∪ r)) x - lemma1 {x} (case1 cp) = record { proj1 = case1 cp ; proj2 = case1 cp } - lemma1 {x} (case2 cqr) = record { proj1 = case2 (proj1 cqr) ; proj2 = case2 (proj2 cqr) } + lemma1 {x} (case1 cp) = ⟪ case1 cp , case1 cp ⟫ + lemma1 {x} (case2 cqr) = ⟪ case2 (proj1 cqr) , case2 (proj2 cqr) ⟫ lemma2 : {x : Ordinal} → odef ((p ∪ q) ∩ (p ∪ r)) x → odef (p ∪ (q ∩ r)) x lemma2 {x} lt with proj1 lt | proj2 lt lemma2 {x} lt | case1 cp | _ = case1 cp lemma2 {x} lt | _ | case1 cp = case1 cp - lemma2 {x} lt | case2 cq | case2 cr = case2 ( record { proj1 = cq ; proj2 = cr } ) + lemma2 {x} lt | case2 cq | case2 cr = case2 ⟪ cq , cr ⟫ record IsBooleanAlgebra ( L : Set n) ( b1 : L ) ( b0 : L ) ( -_ : L → L ) ( _+_ : L → L → L ) - ( _*_ : L → L → L ) : Set (suc n) where + ( _x_ : L → L → L ) : Set (suc n) where field +-assoc : {a b c : L } → a + ( b + c ) ≡ (a + b) + c - *-assoc : {a b c : L } → a * ( b * c ) ≡ (a * b) * c + x-assoc : {a b c : L } → a x ( b x c ) ≡ (a x b) x c +-sym : {a b : L } → a + b ≡ b + a - -sym : {a b : L } → a * b ≡ b * a - -aab : {a b : L } → a + ( a * b ) ≡ a - *-aab : {a b : L } → a * ( a + b ) ≡ a - -dist : {a b c : L } → a + ( b * c ) ≡ ( a * b ) + ( a * c ) - *-dist : {a b c : L } → a * ( b + c ) ≡ ( a + b ) * ( a + c ) + -sym : {a b : L } → a x b ≡ b x a + -aab : {a b : L } → a + ( a x b ) ≡ a + x-aab : {a b : L } → a x ( a + b ) ≡ a + -dist : {a b c : L } → a + ( b x c ) ≡ ( a x b ) + ( a x c ) + x-dist : {a b c : L } → a x ( b + c ) ≡ ( a + b ) x ( a + c ) a+0 : {a : L } → a + b0 ≡ a - a*1 : {a : L } → a * b1 ≡ a + ax1 : {a : L } → a x b1 ≡ a a+-a1 : {a : L } → a + ( - a ) ≡ b1 - a*-a0 : {a : L } → a * ( - a ) ≡ b0 + ax-a0 : {a : L } → a x ( - a ) ≡ b0 record BooleanAlgebra ( L : Set n) : Set (suc n) where field b1 : L b0 : L -_ : L → L - _++_ : L → L → L - _**_ : L → L → L - isBooleanAlgebra : IsBooleanAlgebra L b1 b0 -_ _++_ _**_ + _+_ : L → L → L + _x_ : L → L → L + isBooleanAlgebra : IsBooleanAlgebra L b1 b0 -_ _+_ _x_
--- a/LEMC.agda Fri Jul 31 17:54:52 2020 +0900 +++ b/LEMC.agda Sat Aug 01 11:06:29 2020 +0900 @@ -52,18 +52,18 @@ record choiced ( X : Ordinal ) : Set n where field a-choice : Ordinal - is-in : odef (ord→od X) a-choice + is-in : odef (* X) a-choice open choiced --- ∋→d : ( a : HOD ) { x : HOD } → ord→od (od→ord a) ∋ x → X ∋ ord→od (a-choice (choice-func X not)) --- ∋→d a lt = subst₂ (λ j k → odef j k) oiso (sym diso) lt +-- ∋→d : ( a : HOD ) { x : HOD } → * (& a) ∋ x → X ∋ * (a-choice (choice-func X not)) +-- ∋→d a lt = subst₂ (λ j k → odef j k) *iso (sym &iso) lt -oo∋ : { a : HOD} { x : Ordinal } → odef (ord→od (od→ord a)) x → a ∋ ord→od x -oo∋ lt = subst₂ (λ j k → odef j k) oiso (sym diso) lt +oo∋ : { a : HOD} { x : Ordinal } → odef (* (& a)) x → a ∋ * x +oo∋ lt = subst₂ (λ j k → odef j k) *iso (sym &iso) lt -∋oo : { a : HOD} { x : Ordinal } → a ∋ ord→od x → odef (ord→od (od→ord a)) x -∋oo lt = subst₂ (λ j k → odef j k ) (sym oiso) diso lt +∋oo : { a : HOD} { x : Ordinal } → a ∋ * x → odef (* (& a)) x +∋oo lt = subst₂ (λ j k → odef j k ) (sym *iso) &iso lt OD→ZFC : ZFC OD→ZFC = record { @@ -78,22 +78,18 @@ -- infixr 230 _∩_ _∪_ isZFC : IsZFC (HOD ) _∋_ _=h=_ od∅ Select isZFC = record { - choice-func = λ A {X} not A∋X → ord→od (a-choice (choice-func X not) ); + choice-func = λ A {X} not A∋X → * (a-choice (choice-func X not) ); choice = λ A {X} A∋X not → oo∋ (is-in (choice-func X not)) } where -- -- the axiom choice from LEM and OD ordering -- - choice-func : (X : HOD ) → ¬ ( X =h= od∅ ) → choiced (od→ord X) + choice-func : (X : HOD ) → ¬ ( X =h= od∅ ) → choiced (& X) choice-func X not = have_to_find where ψ : ( ox : Ordinal ) → Set n - ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ odef X x )) ∨ choiced (od→ord X) + ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ odef X x )) ∨ choiced (& X) lemma-ord : ( ox : Ordinal ) → ψ ox lemma-ord ox = TransFinite {ψ} induction ox where - -- ∋-p : (A x : HOD ) → Dec ( A ∋ x ) - -- ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM - -- ∋-p A x | case1 (lift t) = yes t - -- ∋-p A x | case2 t = no (λ x → t (lift x )) ∀-imply-or : {A : Ordinal → Set n } {B : Set n } → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B ∀-imply-or {A} {B} ∀AB with p∨¬p ((x : Ordinal ) → A x) -- LEM @@ -104,18 +100,18 @@ lemma not | case1 b = b lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b )) induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x - induction x prev with ∋-p X ( ord→od x) + induction x prev with ∋-p X ( * x) ... | yes p = case2 ( record { a-choice = x ; is-in = ∋oo p } ) ... | no ¬p = lemma where - lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced (od→ord X) - lemma1 y with ∋-p X (ord→od y) + lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced (& X) + lemma1 y with ∋-p X (* 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 (d→∋ X y<X) ) - lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced (od→ord X) + lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced (& X) lemma = ∀-imply-or lemma1 - have_to_find : choiced (od→ord X) - have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where - ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → odef X x → ⊥) + have_to_find : choiced (& X) + have_to_find = dont-or (lemma-ord (& X )) ¬¬X∋x where + ¬¬X∋x : ¬ ((x : Ordinal) → x o< (& X) → odef X x → ⊥) ¬¬X∋x nn = not record { eq→ = λ {x} lt → ⊥-elim (nn x (odef→o< lt) lt) ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) @@ -140,7 +136,7 @@ ... | case1 P = record { min = x ; x∋min = u∋x - ; min-empty = λ y → P (od→ord y) + ; min-empty = λ y → P (& y) } ... | case2 NP = min2 where p : HOD @@ -149,24 +145,24 @@ lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt)) np : ¬ (p =h= od∅) np p∅ = NP (λ y p∋y → ∅< {p} {_} (d→∋ p p∋y) p∅ ) - y1choice : choiced (od→ord p) + y1choice : choiced (& p) y1choice = choice-func p np y1 : HOD - y1 = ord→od (a-choice y1choice) + y1 = * (a-choice y1choice) y1prop : (x ∋ y1) ∧ (u ∋ y1) y1prop = oo∋ (is-in y1choice) min2 : Minimal u min2 = prev (proj1 y1prop) u (proj2 y1prop) Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u Min2 x u u∋x = (ε-induction1 {λ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x ) - cx : {x : HOD} → ¬ (x =h= od∅ ) → choiced (od→ord x ) + cx : {x : HOD} → ¬ (x =h= od∅ ) → choiced (& x ) cx {x} nx = choice-func x nx minimal : (x : HOD ) → ¬ (x =h= od∅ ) → HOD - minimal x ne = min (Min2 (ord→od (a-choice (cx {x} ne) )) x ( oo∋ (is-in (cx ne))) ) - x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) ) - x∋minimal x ne = x∋min (Min2 (ord→od (a-choice (cx {x} ne) )) x ( oo∋ (is-in (cx ne))) ) - minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) ) - minimal-1 x ne y = min-empty (Min2 (ord→od (a-choice (cx ne) )) x ( oo∋ (is-in (cx ne)))) y + minimal x ne = min (Min2 (* (a-choice (cx {x} ne) )) x ( oo∋ (is-in (cx ne))) ) + x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) ) + x∋minimal x ne = x∋min (Min2 (* (a-choice (cx {x} ne) )) x ( oo∋ (is-in (cx ne))) ) + minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (& y) ) + minimal-1 x ne y = min-empty (Min2 (* (a-choice (cx ne) )) x ( oo∋ (is-in (cx ne)))) y
--- a/OD.agda Fri Jul 31 17:54:52 2020 +0900 +++ b/OD.agda Sat Aug 01 11:06:29 2020 +0900 @@ -5,7 +5,7 @@ open import zf open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import Data.Nat.Properties open import Data.Empty open import Relation.Nullary @@ -91,17 +91,17 @@ record ODAxiom : Set (suc n) where field -- HOD is isomorphic to Ordinal (by means of Goedel number) - od→ord : HOD → Ordinal - ord→od : Ordinal → HOD - c<→o< : {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y - ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) - oiso : {x : HOD } → ord→od ( od→ord x ) ≡ x - diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x + & : HOD → Ordinal + * : Ordinal → HOD + c<→o< : {x y : HOD } → def (od y) ( & x ) → & x o< & y + ⊆→o≤ : {y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) + *iso : {x : HOD } → * ( & x ) ≡ x + &iso : {x : Ordinal } → & ( * x ) ≡ x ==→o≡ : {x y : HOD } → (od x == od y) → x ≡ y sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ -- possible order restriction - ho< : {x : HOD} → od→ord x o< next (odmax x) + ho< : {x : HOD} → & x o< next (odmax x) postulate odAxiom : ODAxiom @@ -118,8 +118,8 @@ odmaxmin = (y : HOD) (z : Ordinal) → ((x : Ordinal)→ def (od y) x → x o< z) → odmax y o< osuc z -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD -¬OD-order : ( od→ord : OD → Ordinal ) → ( ord→od : Ordinal → OD ) → ( { x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y) → ⊥ -¬OD-order od→ord ord→od c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj ) +¬OD-order : ( & : OD → Ordinal ) → ( * : Ordinal → OD ) → ( { x y : OD } → def y ( & x ) → & x o< & y) → ⊥ +¬OD-order & * c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj ) -- Open supreme upper bound leads a contradition, so we use domain restriction on sup ¬open-sup : ( sup-o : (Ordinal → Ordinal ) → Ordinal) → ((ψ : Ordinal → Ordinal ) → (x : Ordinal) → ψ x o< sup-o ψ ) → ⊥ @@ -140,13 +140,13 @@ odef A x = def ( od A ) x _∋_ : ( a x : HOD ) → Set n -_∋_ a x = odef a ( od→ord x ) +_∋_ a x = odef a ( & 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 +d→∋ : ( a : HOD ) { x : Ordinal} → odef a x → a ∋ (* x) +d→∋ a lt = subst (λ k → odef a k ) (sym &iso) lt cseq : HOD → HOD cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where @@ -159,60 +159,60 @@ otrans : {a x y : Ordinal } → odef (Ord a) x → odef (Ord x) y → odef (Ord a) y otrans x<a y<x = ordtrans y<x x<a -odef→o< : {X : HOD } → {x : Ordinal } → odef X x → x o< od→ord X -odef→o< {X} {x} lt = o<-subst {_} {_} {x} {od→ord X} ( c<→o< ( odef-subst {X} {x} lt (sym oiso) (sym diso) )) diso diso +odef→o< : {X : HOD } → {x : Ordinal } → odef X x → x o< & X +odef→o< {X} {x} lt = o<-subst {_} {_} {x} {& X} ( c<→o< ( odef-subst {X} {x} lt (sym *iso) (sym &iso) )) &iso &iso -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 )) +odefo→o< : {X y : Ordinal } → odef (* X) y → y o< X +odefo→o< {X} {y} lt = subst₂ (λ j k → j o< k ) &iso &iso ( c<→o< (subst (λ k → odef (* X) k ) (sym &iso ) 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 y : Ordinal } → x o< y → odef (* y) x ) → {x : HOD } → x ≡ 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 ) + lemma1 : {y : Ordinal} → odef x y → odef (Ord (& x)) y + lemma1 {y} lt = subst ( λ k → k o< & x ) &iso (c<→o< {* y} {x} (d→∋ x lt)) + lemma2 : {y : Ordinal} → odef (Ord (& x)) y → odef x y + lemma2 {y} lt = subst (λ k → odef k y ) *iso (o<→c< {y} {& x} lt ) -- avoiding lv != Zero error -orefl : { x : HOD } → { y : Ordinal } → od→ord x ≡ y → od→ord x ≡ y +orefl : { x : HOD } → { y : Ordinal } → & x ≡ y → & x ≡ y orefl refl = refl -==-iso : { x y : HOD } → od (ord→od (od→ord x)) == od (ord→od (od→ord y)) → od x == od y +==-iso : { x y : HOD } → od (* (& x)) == od (* (& y)) → od x == od y ==-iso {x} {y} eq = record { - eq→ = λ d → lemma ( eq→ eq (odef-subst d (sym oiso) refl )) ; - eq← = λ d → lemma ( eq← eq (odef-subst d (sym oiso) refl )) } + eq→ = λ d → lemma ( eq→ eq (odef-subst d (sym *iso) refl )) ; + eq← = λ d → lemma ( eq← eq (odef-subst d (sym *iso) refl )) } where - lemma : {x : HOD } {z : Ordinal } → odef (ord→od (od→ord x)) z → odef x z - lemma {x} {z} d = odef-subst d oiso refl + lemma : {x : HOD } {z : Ordinal } → odef (* (& x)) z → odef x z + lemma {x} {z} d = odef-subst d *iso refl -=-iso : {x y : HOD } → (od x == od y) ≡ (od (ord→od (od→ord x)) == od y) -=-iso {_} {y} = cong ( λ k → od k == od y ) (sym oiso) +=-iso : {x y : HOD } → (od x == od y) ≡ (od (* (& x)) == od y) +=-iso {_} {y} = cong ( λ k → od k == od y ) (sym *iso) -ord→== : { x y : HOD } → od→ord x ≡ od→ord y → od x == od y -ord→== {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq)) where - lemma : ( ox oy : Ordinal ) → ox ≡ oy → od (ord→od ox) == od (ord→od oy) +ord→== : { x y : HOD } → & x ≡ & y → od x == od y +ord→== {x} {y} eq = ==-iso (lemma (& x) (& y) (orefl eq)) where + lemma : ( ox oy : Ordinal ) → ox ≡ oy → od (* ox) == od (* oy) lemma ox ox refl = ==-refl -o≡→== : { x y : Ordinal } → x ≡ y → od (ord→od x) == od (ord→od y) +o≡→== : { x y : Ordinal } → x ≡ y → od (* x) == od (* y) o≡→== {x} {.x} refl = ==-refl -o∅≡od∅ : ord→od (o∅ ) ≡ od∅ +o∅≡od∅ : * (o∅ ) ≡ od∅ o∅≡od∅ = ==→o≡ lemma where - lemma0 : {x : Ordinal} → odef (ord→od o∅) x → odef od∅ x - lemma0 {x} lt = o<-subst (c<→o< {ord→od x} {ord→od o∅} (odef-subst {ord→od o∅} {x} lt refl (sym diso)) ) diso diso - lemma1 : {x : Ordinal} → odef od∅ x → odef (ord→od o∅) x + lemma0 : {x : Ordinal} → odef (* o∅) x → odef od∅ x + lemma0 {x} lt = o<-subst (c<→o< {* x} {* o∅} (odef-subst {* o∅} {x} lt refl (sym &iso)) ) &iso &iso + lemma1 : {x : Ordinal} → odef od∅ x → odef (* o∅) x lemma1 {x} lt = ⊥-elim (¬x<0 lt) - lemma : od (ord→od o∅) == od od∅ + lemma : od (* o∅) == od od∅ lemma = record { eq→ = lemma0 ; eq← = lemma1 } -ord-od∅ : od→ord (od∅ ) ≡ o∅ -ord-od∅ = sym ( subst (λ k → k ≡ od→ord (od∅ ) ) diso (cong ( λ k → od→ord k ) o∅≡od∅ ) ) +ord-od∅ : & (od∅ ) ≡ o∅ +ord-od∅ = sym ( subst (λ k → k ≡ & (od∅ ) ) &iso (cong ( λ k → & k ) o∅≡od∅ ) ) ∅0 : record { def = λ x → Lift n ⊥ } == od od∅ eq→ ∅0 {w} (lift ()) eq← ∅0 {w} lt = lift (¬x<0 lt) -∅< : { x y : HOD } → odef x (od→ord y ) → ¬ ( od x == od od∅ ) +∅< : { x y : HOD } → odef x (& y ) → ¬ ( od x == od od∅ ) ∅< {x} {y} d eq with eq→ (==-trans eq (==-sym ∅0) ) d ∅< {x} {y} d eq | lift () @@ -230,44 +230,44 @@ -- the pair _,_ : HOD → HOD → HOD -x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = omax (od→ord x) (od→ord y) ; <odmax = lemma } where - lemma : {t : Ordinal} → (t ≡ od→ord x) ∨ (t ≡ od→ord y) → t o< omax (od→ord x) (od→ord y) +x , y = record { od = record { def = λ t → (t ≡ & x ) ∨ ( t ≡ & y ) } ; odmax = omax (& x) (& y) ; <odmax = lemma } where + lemma : {t : Ordinal} → (t ≡ & x) ∨ (t ≡ & y) → t o< omax (& x) (& y) lemma {t} (case1 refl) = omax-x _ _ lemma {t} (case2 refl) = omax-y _ _ -pair-xx<xy : {x y : HOD} → od→ord (x , x) o< osuc (od→ord (x , y) ) +pair-xx<xy : {x y : HOD} → & (x , x) o< osuc (& (x , y) ) pair-xx<xy {x} {y} = ⊆→o≤ lemma where lemma : {z : Ordinal} → def (od (x , x)) z → def (od (x , y)) z lemma {z} (case1 refl) = case1 refl lemma {z} (case2 refl) = case1 refl -pair-<xy : {x y : HOD} → {n : Ordinal} → od→ord x o< next n → od→ord y o< next n → od→ord (x , y) o< next n -pair-<xy {x} {y} {o} x<nn y<nn with trio< (od→ord x) (od→ord y) | inspect (omax (od→ord x)) (od→ord y) +pair-<xy : {x y : HOD} → {n : Ordinal} → & x o< next n → & y o< next n → & (x , y) o< next n +pair-<xy {x} {y} {o} x<nn y<nn with trio< (& x) (& y) | inspect (omax (& x)) (& y) ... | tri< a ¬b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx y<nn)) ho< ... | tri> ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho< ... | tri≈ ¬a b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho< -- another form of infinite -- pair-ord< : {x : Ordinal } → Set n -pair-ord< : {x : HOD } → ( {y : HOD } → od→ord y o< next (odmax y) ) → od→ord ( x , x ) o< next (od→ord x) -pair-ord< {x} ho< = subst (λ k → od→ord (x , x) o< k ) lemmab0 lemmab1 where - lemmab0 : next (odmax (x , x)) ≡ next (od→ord x) +pair-ord< : {x : HOD } → ( {y : HOD } → & y o< next (odmax y) ) → & ( x , x ) o< next (& x) +pair-ord< {x} ho< = subst (λ k → & (x , x) o< k ) lemmab0 lemmab1 where + lemmab0 : next (odmax (x , x)) ≡ next (& x) lemmab0 = trans (cong (λ k → next k) (omxx _)) (sym nexto≡) - lemmab1 : od→ord (x , x) o< next ( odmax (x , x)) + lemmab1 : & (x , x) o< next ( odmax (x , x)) lemmab1 = ho< -pair<y : {x y : HOD } → y ∋ x → od→ord (x , x) o< osuc (od→ord y) +pair<y : {x y : HOD } → y ∋ x → & (x , x) o< osuc (& y) pair<y {x} {y} y∋x = ⊆→o≤ lemma where lemma : {z : Ordinal} → def (od (x , x)) z → def (od y) z lemma (case1 refl) = y∋x lemma (case2 refl) = y∋x -- another possible restriction. We reqest no minimality on odmax, so it may arbitrary larger. -odmax<od→ord : { x y : HOD } → x ∋ y → Set n -odmax<od→ord {x} {y} x∋y = odmax x o< od→ord x +odmax<& : { x y : HOD } → x ∋ y → Set n +odmax<& {x} {y} x∋y = odmax x o< & x in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → OD -in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } +in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ( x ≡ & (ψ (* y ))))) } _∩_ : ( A B : HOD ) → HOD A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } @@ -286,35 +286,35 @@ refl-⊆ : {A : HOD} → A ⊆ A 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 (d→∋ x x>z))) +od⊆→o≤ : {x y : HOD } → x ⊆ y → & x o< osuc (& y) +od⊆→o≤ {x} {y} lt = ⊆→o≤ {x} {y} (λ {z} x>z → subst (λ k → def (od y) k ) &iso (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) ) - → ({y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) ) - → {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y -⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x with trio< (od→ord x) (od→ord y) +-- if we have & (x , x) ≡ osuc (& x), ⊆→o≤ → c<→o< +⊆→o≤→c<→o< : ({x : HOD} → & (x , x) ≡ osuc (& x) ) + → ({y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) ) + → {x y : HOD } → def (od y) ( & x ) → & x o< & y +⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x with trio< (& x) (& y) ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri< a ¬b ¬c = a ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (peq {x}) (pair<y (subst (λ k → k ∋ x) (sym ( ==→o≡ {x} {y} (ord→== b))) y∋x ))) ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri> ¬a ¬b c = ⊥-elim ( o<> (⊆→o≤ {x , x} {y} y⊆x,x ) lemma1 ) where - lemma : {z : Ordinal} → (z ≡ od→ord x) ∨ (z ≡ od→ord x) → od→ord x ≡ z + lemma : {z : Ordinal} → (z ≡ & x) ∨ (z ≡ & x) → & x ≡ z lemma (case1 refl) = refl lemma (case2 refl) = refl y⊆x,x : {z : Ordinals.ord O} → def (od (x , x)) z → def (od y) z y⊆x,x {z} lt = subst (λ k → def (od y) k ) (lemma lt) y∋x - lemma1 : osuc (od→ord y) o< od→ord (x , x) - lemma1 = subst (λ k → osuc (od→ord y) o< k ) (sym (peq {x})) (osucc c ) + lemma1 : osuc (& y) o< & (x , x) + lemma1 = subst (λ k → osuc (& y) o< k ) (sym (peq {x})) (osucc c ) subset-lemma : {A x : HOD } → ( {y : HOD } → x ∋ y → (A ∩ x ) ∋ y ) ⇔ ( x ⊆ A ) subset-lemma {A} {x} = record { proj1 = λ lt → record { incl = λ x∋z → proj1 (lt x∋z) } - ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt } + ; proj2 = λ x⊆A lt → ⟪ incl x⊆A lt , lt ⟫ } -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)) +power< : {A x : HOD } → x ⊆ A → Ord (osuc (& A)) ∋ x +power< {A} {x} x⊆A = ⊆→o≤ (λ {y} x∋y → subst (λ k → def (od A) k) &iso (lemma y x∋y ) ) where + lemma : (y : Ordinal) → def (od x) y → def (od A) (& (* y)) lemma y x∋y = incl x⊆A (d→∋ x x∋y) open import Data.Unit @@ -322,30 +322,30 @@ ε-induction : { ψ : HOD → Set n} → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x ) → (x : HOD ) → ψ x -ε-induction {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where - induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox) - induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) - ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) - ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy +ε-induction {ψ} ind x = subst (λ k → ψ k ) *iso (ε-induction-ord (osuc (& x)) <-osuc ) where + induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (* oy)) → ψ (* ox) + induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) *iso (prev (& y) (o<-subst (c<→o< lt) refl &iso ))) + ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (* oy) + ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (* oy)} induction oy -- level trick (what'a shame) for LEM / minimal ε-induction1 : { ψ : HOD → Set (suc n)} → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x ) → (x : HOD ) → ψ x -ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where - induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox) - induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) - ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) - ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy +ε-induction1 {ψ} ind x = subst (λ k → ψ k ) *iso (ε-induction-ord (osuc (& x)) <-osuc ) where + induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (* oy)) → ψ (* ox) + induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) *iso (prev (& y) (o<-subst (c<→o< lt) refl &iso ))) + ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (* oy) + ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (* oy)} induction oy Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD -Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) } +Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( * x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) } Replace : HOD → (HOD → HOD) → HOD -Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) ∧ def (in-codomain X ψ) x } +Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → & (ψ (* y)))) ∧ def (in-codomain X ψ) x } ; odmax = rmax ; <odmax = rmax<} where rmax : Ordinal - rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y))) + rmax = sup-o X (λ y X∋y → & (ψ (* y))) rmax< : {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax rmax< lt = proj1 lt @@ -353,28 +353,28 @@ -- If we have LEM, Replace' is equivalent to Replace -- in-codomain' : (X : HOD ) → ((x : HOD) → X ∋ x → HOD) → OD -in-codomain' X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ((lt : odef X y) → x ≡ od→ord (ψ (ord→od y ) (d→∋ X lt) )))) } +in-codomain' X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ((lt : odef X y) → x ≡ & (ψ (* y ) (d→∋ X lt) )))) } Replace' : (X : HOD) → ((x : HOD) → X ∋ x → HOD) → HOD -Replace' X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y) (d→∋ X X∋y) ))) ∧ def (in-codomain' X ψ) x } +Replace' X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → & (ψ (* y) (d→∋ X X∋y) ))) ∧ def (in-codomain' X ψ) x } ; odmax = rmax ; <odmax = rmax< } where rmax : Ordinal - rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y) (d→∋ X X∋y))) + rmax = sup-o X (λ y X∋y → & (ψ (* y) (d→∋ X X∋y))) rmax< : {y : Ordinal} → (y o< rmax) ∧ def (in-codomain' X ψ) y → y o< rmax rmax< lt = proj1 lt Union : HOD → HOD -Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } - ; odmax = osuc (od→ord U) ; <odmax = umax< } where - umax< : {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (ord→od u)) y) → y o< osuc (od→ord U) +Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (* u) x))) } + ; odmax = osuc (& U) ; <odmax = umax< } where + umax< : {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (* u)) y) → y o< osuc (& 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< (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< (d→∋ U x<U)) - lemma1 : {x : Ordinal} → def (od U) x ∧ def (od (ord→od x)) y → ¬ (od→ord U o< y) + lemma0 : {x : Ordinal} → def (od (* x)) y → y o< x + lemma0 {x} x<y = subst₂ (λ j k → j o< k ) &iso &iso (c<→o< (d→∋ (* x) x<y )) + lemma2 : {x : Ordinal} → def (od U) x → x o< & U + lemma2 {x} x<U = subst (λ k → k o< & U ) &iso (c<→o< (d→∋ U x<U)) + lemma1 : {x : Ordinal} → def (od U) x ∧ def (od (* x)) y → ¬ (& 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) - lemma not with trio< y (od→ord U) + lemma : ¬ ((& U) o< y ) → y o< osuc (& U) + lemma not with trio< y (& U) lemma not | tri< a ¬b ¬c = ordtrans a <-osuc lemma not | tri≈ ¬a refl ¬c = <-osuc lemma not | tri> ¬a ¬b c = ⊥-elim (not c) @@ -382,31 +382,31 @@ A ∈ B = B ∋ A OPwr : (A : HOD ) → HOD -OPwr A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( A ∩ (ord→od x)) ) ) +OPwr A = Ord ( sup-o (Ord (osuc (& A))) ( λ x A∋x → & ( A ∩ (* x)) ) ) Power : HOD → HOD -Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x ) +Power A = Replace (OPwr (Ord (& A))) ( λ x → A ∩ x ) -- ｛_｝ : ZFSet → ZFSet -- ｛ x ｝ = ( x , x ) -- better to use (x , x) directly union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z -union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx - ; proj2 = subst ( λ k → odef k (od→ord z)) (sym oiso) (proj2 xx) } )) +union→ X z u xx not = ⊥-elim ( not (& u) ( ⟪ proj1 xx + , subst ( λ k → odef k (& z)) (sym *iso) (proj2 xx) ⟫ )) 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 = d→∋ X (proj1 xx) ; proj2 = proj2 xx } + lemma : {y : Ordinal} → odef X y ∧ odef (* y) (& z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z)) + lemma {y} xx not = not (* y) ⟪ d→∋ X (proj1 xx) , proj2 xx ⟫ data infinite-d : ( x : Ordinal ) → Set n where iφ : infinite-d o∅ isuc : {x : Ordinal } → infinite-d x → - infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) + infinite-d (& ( Union (* x , (* x , * x ) ) )) -- ω can be diverged in our case, since we have no restriction on the corresponding ordinal of a pair. -- We simply assumes infinite-d y has a maximum. -- --- This means that many of OD may not be HODs because of the od→ord mapping divergence. --- We should have some axioms to prevent this such as od→ord x o< next (odmax x). +-- This means that many of OD may not be HODs because of the & mapping divergence. +-- We should have some axioms to prevent this such as & x o< next (odmax x). -- -- postulate -- ωmax : Ordinal @@ -421,25 +421,25 @@ infinite : HOD infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where u : (y : Ordinal ) → HOD - u y = Union (ord→od y , (ord→od y , ord→od y)) + u y = Union (* y , (* y , * y)) -- next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z - lemma8 : {y : Ordinal} → od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y)) + lemma8 : {y : Ordinal} → & (* y , * y) o< next (odmax (* y , * y)) lemma8 = ho< --- (x,y) < next (omax x y) < next (osuc y) = next y - lemmaa : {x y : HOD} → od→ord x o< od→ord y → od→ord (x , y) o< next (od→ord y) - lemmaa {x} {y} x<y = subst (λ k → od→ord (x , y) o< k ) (sym nexto≡) (subst (λ k → od→ord (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< ) - lemma81 : {y : Ordinal} → od→ord (ord→od y , ord→od y) o< next (od→ord (ord→od y)) - lemma81 {y} = nexto=n (subst (λ k → od→ord (ord→od y , ord→od y) o< k ) (cong (λ k → next k) (omxx _)) lemma8) - lemma9 : {y : Ordinal} → od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y , ord→od y)) + lemmaa : {x y : HOD} → & x o< & y → & (x , y) o< next (& y) + lemmaa {x} {y} x<y = subst (λ k → & (x , y) o< k ) (sym nexto≡) (subst (λ k → & (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< ) + lemma81 : {y : Ordinal} → & (* y , * y) o< next (& (* y)) + lemma81 {y} = nexto=n (subst (λ k → & (* y , * y) o< k ) (cong (λ k → next k) (omxx _)) lemma8) + lemma9 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y , * y)) lemma9 = lemmaa (c<→o< (case1 refl)) - lemma71 : {y : Ordinal} → od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y)) + lemma71 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y)) lemma71 = next< lemma81 lemma9 - lemma1 : {y : Ordinal} → od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y)))) + lemma1 : {y : Ordinal} → & (u y) o< next (osuc (& (* y , (* y , * y)))) lemma1 = ho< --- main recursion lemma : {y : Ordinal} → infinite-d y → y o< next o∅ lemma {o∅} iφ = x<nx - lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → od→ord (ord→od y , (ord→od y , ord→od y)) o< next k) diso lemma71 ) (nexto=n lemma1)) + lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → & (* y , (* y , * y)) o< next k) &iso lemma71 ) (nexto=n lemma1)) ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅ ω<next-o∅ {y} lt = <odmax infinite lt @@ -455,11 +455,11 @@ ω→nat : (n : HOD) → infinite ∋ n → Nat ω→nat n = ω→nato -ω∋nat→ω : {n : Nat} → def (od infinite) (od→ord (nat→ω n)) +ω∋nat→ω : {n : Nat} → def (od infinite) (& (nat→ω n)) ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) (sym ord-od∅) iφ ω∋nat→ω {Suc n} = subst (λ k → def (od infinite) k) lemma (isuc ( ω∋nat→ω {n})) where - lemma : od→ord (Union (ord→od (od→ord (nat→ω n)) , (ord→od (od→ord (nat→ω n)) , ord→od (od→ord (nat→ω n))))) ≡ od→ord (nat→ω (Suc n)) - lemma = subst (λ k → od→ord (Union (k , ( k , k ))) ≡ od→ord (nat→ω (Suc n))) (sym oiso) refl + lemma : & (Union (* (& (nat→ω n)) , (* (& (nat→ω n)) , * (& (nat→ω n))))) ≡ & (nat→ω (Suc n)) + lemma = subst (λ k → & (Union (k , ( k , k ))) ≡ & (nat→ω (Suc n))) (sym *iso) refl _=h=_ : (x y : HOD) → Set n x =h= y = od x == od y @@ -468,12 +468,12 @@ -- infixr 230 _∩_ _∪_ pair→ : ( x y t : HOD ) → (x , y) ∋ t → ( t =h= x ) ∨ ( t =h= y ) -pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j =h= k ) oiso oiso (o≡→== t≡x )) -pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j =h= k ) oiso oiso (o≡→== t≡y )) +pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j =h= k ) *iso *iso (o≡→== t≡x )) +pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j =h= k ) *iso *iso (o≡→== t≡y )) pair← : ( x y t : HOD ) → ( t =h= x ) ∨ ( t =h= y ) → (x , y) ∋ t -pair← x y t (case1 t=h=x) = case1 (cong (λ k → od→ord k ) (==→o≡ t=h=x)) -pair← x y t (case2 t=h=y) = case2 (cong (λ k → od→ord k ) (==→o≡ t=h=y)) +pair← x y t (case1 t=h=x) = case1 (cong (λ k → & k ) (==→o≡ t=h=x)) +pair← x y t (case2 t=h=y) = case2 (cong (λ k → & k ) (==→o≡ t=h=y)) pair1 : { x y : HOD } → (x , y ) ∋ x pair1 = case1 refl @@ -495,109 +495,109 @@ ⊆→o< {x} {y} lt with trio< x y ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc -⊆→o< {x} {y} lt | tri> ¬a ¬b c with (incl lt) (o<-subst c (sym diso) refl ) -... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl )) +⊆→o< {x} {y} lt | tri> ¬a ¬b c with (incl lt) (o<-subst c (sym &iso) refl ) +... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt &iso refl )) open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) -- postulate f-extensionality : { n m : Level} → HE.Extensionality n m -ω-prev-eq1 : {x y : Ordinal} → od→ord (Union (ord→od y , (ord→od y , ord→od y))) ≡ od→ord (Union (ord→od x , (ord→od x , ord→od x))) → ¬ (x o< y) -ω-prev-eq1 {x} {y} eq x<y = eq→ (ord→== eq) {od→ord (ord→od y)} (λ not2 → not2 (od→ord (ord→od y , ord→od y)) - record { proj1 = case2 refl ; proj2 = subst (λ k → odef k (od→ord (ord→od y))) (sym oiso) (case1 refl)} ) (λ u → lemma u ) where - lemma : (u : Ordinal) → ¬ def (od (ord→od x , (ord→od x , ord→od x))) u ∧ def (od (ord→od u)) (od→ord (ord→od y)) +ω-prev-eq1 : {x y : Ordinal} → & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → ¬ (x o< y) +ω-prev-eq1 {x} {y} eq x<y = eq→ (ord→== eq) {& (* y)} (λ not2 → not2 (& (* y , * y)) + ⟪ case2 refl , subst (λ k → odef k (& (* y))) (sym *iso) (case1 refl)⟫ ) (λ u → lemma u ) where + lemma : (u : Ordinal) → ¬ def (od (* x , (* x , * x))) u ∧ def (od (* u)) (& (* y)) lemma u t with proj1 t - lemma u t | case1 u=x = o<> (c<→o< {ord→od y} {ord→od u} (proj2 t)) (subst₂ (λ j k → j o< k ) - (trans (sym diso) (trans (sym u=x) (sym diso)) ) (sym diso) x<y ) -- x ≡ od→ord (ord→od u) - lemma u t | case2 u=xx = o<¬≡ (lemma1 (subst (λ k → odef k (od→ord (ord→od y)) ) (trans (cong (λ k → ord→od k ) u=xx) oiso ) (proj2 t))) x<y where - lemma1 : {x y : Ordinal } → (ord→od x , ord→od x ) ∋ ord→od y → x ≡ y -- y = x ∈ ( x , x ) = u - lemma1 (case1 eq) = subst₂ (λ j k → j ≡ k ) diso diso (sym eq) - lemma1 (case2 eq) = subst₂ (λ j k → j ≡ k ) diso diso (sym eq) + lemma u t | case1 u=x = o<> (c<→o< {* y} {* u} (proj2 t)) (subst₂ (λ j k → j o< k ) + (trans (sym &iso) (trans (sym u=x) (sym &iso)) ) (sym &iso) x<y ) -- x ≡ & (* u) + lemma u t | case2 u=xx = o<¬≡ (lemma1 (subst (λ k → odef k (& (* y)) ) (trans (cong (λ k → * k ) u=xx) *iso ) (proj2 t))) x<y where + lemma1 : {x y : Ordinal } → (* x , * x ) ∋ * y → x ≡ y -- y = x ∈ ( x , x ) = u + lemma1 (case1 eq) = subst₂ (λ j k → j ≡ k ) &iso &iso (sym eq) + lemma1 (case2 eq) = subst₂ (λ j k → j ≡ k ) &iso &iso (sym eq) -ω-prev-eq : {x y : Ordinal} → od→ord (Union (ord→od y , (ord→od y , ord→od y))) ≡ od→ord (Union (ord→od x , (ord→od x , ord→od x))) → x ≡ y +ω-prev-eq : {x y : Ordinal} → & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → x ≡ y ω-prev-eq {x} {y} eq with trio< x y ω-prev-eq {x} {y} eq | tri< a ¬b ¬c = ⊥-elim (ω-prev-eq1 eq a) ω-prev-eq {x} {y} eq | tri≈ ¬a b ¬c = b ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c) ω-∈s : (x : HOD) → Union ( x , (x , x)) ∋ x -ω-∈s x not = not (od→ord (x , x)) record { proj1 = case2 refl ; proj2 = subst (λ k → odef k (od→ord x) ) (sym oiso) (case1 refl) } +ω-∈s x not = not (& (x , x)) ⟪ case2 refl , subst (λ k → odef k (& x) ) (sym *iso) (case1 refl) ⟫ ωs≠0 : (x : HOD) → ¬ ( Union ( x , (x , x)) ≡ od∅ ) -ωs≠0 y eq = ⊥-elim ( ¬x<0 (subst (λ k → od→ord y o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (od→ord y )) eq (ω-∈s y) ))) ) +ωs≠0 y eq = ⊥-elim ( ¬x<0 (subst (λ k → & y o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (& y )) eq (ω-∈s y) ))) ) nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i nat→ω-iso {i} = ε-induction1 {λ i → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i } ind i where ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) → (lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x - ind {x} prev lt = ind1 lt oiso where - ind1 : {ox : Ordinal } → (ltd : infinite-d ox ) → ord→od ox ≡ x → nat→ω (ω→nato ltd) ≡ x + ind {x} prev lt = ind1 lt *iso where + ind1 : {ox : Ordinal } → (ltd : infinite-d ox ) → * ox ≡ x → nat→ω (ω→nato ltd) ≡ x ind1 {o∅} iφ refl = sym o∅≡od∅ ind1 (isuc {x₁} ltd) ox=x = begin nat→ω (ω→nato (isuc ltd) ) ≡⟨⟩ Union (nat→ω (ω→nato ltd) , (nat→ω (ω→nato ltd) , nat→ω (ω→nato ltd))) ≡⟨ cong (λ k → Union (k , (k , k ))) lemma ⟩ - Union (ord→od x₁ , (ord→od x₁ , ord→od x₁)) - ≡⟨ trans ( sym oiso) ox=x ⟩ + Union (* x₁ , (* x₁ , * x₁)) + ≡⟨ trans ( sym *iso) ox=x ⟩ x ∎ where open ≡-Reasoning - lemma0 : x ∋ ord→od x₁ - lemma0 = subst (λ k → odef k (od→ord (ord→od x₁))) (trans (sym oiso) ox=x) (λ not → not - (od→ord (ord→od x₁ , ord→od x₁)) record {proj1 = pair2 ; proj2 = subst (λ k → odef k (od→ord (ord→od x₁))) (sym oiso) pair1 } ) - lemma1 : infinite ∋ ord→od x₁ - lemma1 = subst (λ k → odef infinite k) (sym diso) ltd + lemma0 : x ∋ * x₁ + lemma0 = subst (λ k → odef k (& (* x₁))) (trans (sym *iso) ox=x) (λ not → not + (& (* x₁ , * x₁)) ⟪ pair2 , subst (λ k → odef k (& (* x₁))) (sym *iso) pair1 ⟫ ) + lemma1 : infinite ∋ * x₁ + lemma1 = subst (λ k → odef infinite k) (sym &iso) ltd lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1 lemma3 iφ iφ refl = HE.refl - lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) diso eq (c<→o< (ω-∈s (ord→od y)) ))) - lemma3 (isuc {y} ltd) iφ eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) diso (sym eq) (c<→o< (ω-∈s (ord→od y)) ))) + lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso eq (c<→o< (ω-∈s (* y)) ))) + lemma3 (isuc {y} ltd) iφ eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso (sym eq) (c<→o< (ω-∈s (* y)) ))) lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (sym eq)) ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅ (ω-prev-eq eq)) t lemma2 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1 lemma2 {x} {y} ltd ltd1 eq = lemma6 eq (lemma3 {x} {y} ltd ltd1 eq) where lemma6 : {x y : Ordinal} → {ltd : infinite-d x } {ltd1 : infinite-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1 lemma6 refl HE.refl = refl - lemma : nat→ω (ω→nato ltd) ≡ ord→od x₁ - lemma = trans (cong (λ k → nat→ω k) (lemma2 {x₁} {_} ltd (subst (λ k → infinite-d k ) (sym diso) ltd) diso ) ) ( prev {ord→od x₁} lemma0 lemma1 ) + lemma : nat→ω (ω→nato ltd) ≡ * x₁ + lemma = trans (cong (λ k → nat→ω k) (lemma2 {x₁} {_} ltd (subst (λ k → infinite-d k ) (sym &iso) ltd) &iso ) ) ( prev {* x₁} lemma0 lemma1 ) ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i -ω→nat-iso {i} = lemma i (ω∋nat→ω {i}) oiso where - lemma : {x : Ordinal } → ( i : Nat ) → (ltd : infinite-d x ) → ord→od x ≡ nat→ω i → ω→nato ltd ≡ i +ω→nat-iso {i} = lemma i (ω∋nat→ω {i}) *iso where + lemma : {x : Ordinal } → ( i : Nat ) → (ltd : infinite-d x ) → * x ≡ nat→ω i → ω→nato ltd ≡ i lemma {x} Zero iφ eq = refl lemma {x} (Suc i) iφ eq = ⊥-elim ( ωs≠0 (nat→ω i) (trans (sym eq) o∅≡od∅ )) -- Union (nat→ω i , (nat→ω i , nat→ω i)) ≡ od∅ - lemma Zero (isuc {x} ltd) eq = ⊥-elim ( ωs≠0 (ord→od x) (subst (λ k → k ≡ od∅ ) oiso eq )) - lemma (Suc i) (isuc {x} ltd) eq = cong (λ k → Suc k ) (lemma i ltd (lemma1 eq) ) where -- ord→od x ≡ nat→ω i - lemma1 : ord→od (od→ord (Union (ord→od x , (ord→od x , ord→od x)))) ≡ Union (nat→ω i , (nat→ω i , nat→ω i)) → ord→od x ≡ nat→ω i - lemma1 eq = subst (λ k → ord→od x ≡ k ) oiso (cong (λ k → ord→od k) - ( ω-prev-eq (subst (λ k → _ ≡ k ) diso (cong (λ k → od→ord k ) (sym - (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym oiso ) eq )))))) + lemma Zero (isuc {x} ltd) eq = ⊥-elim ( ωs≠0 (* x) (subst (λ k → k ≡ od∅ ) *iso eq )) + lemma (Suc i) (isuc {x} ltd) eq = cong (λ k → Suc k ) (lemma i ltd (lemma1 eq) ) where -- * x ≡ nat→ω i + lemma1 : * (& (Union (* x , (* x , * x)))) ≡ Union (nat→ω i , (nat→ω i , nat→ω i)) → * x ≡ nat→ω i + lemma1 eq = subst (λ k → * x ≡ k ) *iso (cong (λ k → * k) + ( ω-prev-eq (subst (λ k → _ ≡ k ) &iso (cong (λ k → & k ) (sym + (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym *iso ) eq )))))) ψiso : {ψ : HOD → Set n} {x y : HOD } → ψ x → x ≡ y → ψ y ψiso {ψ} t refl = t selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) -selection {ψ} {X} {y} = record { - proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) } - ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso } - } +selection {ψ} {X} {y} = ⟪ + ( λ cond → ⟪ proj1 cond , ψiso {ψ} (proj2 cond) (sym *iso) ⟫ ) + , ( λ select → ⟪ proj1 select , ψiso {ψ} (proj2 select) *iso ⟫ ) + ⟫ selection-in-domain : {ψ : HOD → Set n} {X y : HOD} → Select X ψ ∋ y → X ∋ y selection-in-domain {ψ} {X} {y} lt = proj1 ((proj2 (selection {ψ} {X} )) lt) -sup-c< : (ψ : HOD → HOD) → {X x : HOD} → X ∋ x → od→ord (ψ x) o< (sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) -sup-c< ψ {X} {x} lt = subst (λ k → od→ord (ψ k) o< _ ) oiso (sup-o< X lt ) +sup-c< : (ψ : HOD → HOD) → {X x : HOD} → X ∋ x → & (ψ x) o< (sup-o X (λ y X∋y → & (ψ (* y)))) +sup-c< ψ {X} {x} lt = subst (λ k → & (ψ k) o< _ ) *iso (sup-o< X lt ) replacement← : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace X ψ ∋ ψ x -replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {X} {x} lt ; proj2 = lemma } where - lemma : def (in-codomain X ψ) (od→ord (ψ x)) - lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} )) +replacement← {ψ} X x lt = ⟪ sup-c< ψ {X} {x} lt , lemma ⟫ where + lemma : def (in-codomain X ψ) (& (ψ x)) + lemma not = ⊥-elim ( not ( & x ) (⟪ lt , cong (λ k → & (ψ k)) (sym *iso)⟫ )) replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y)) replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where - lemma2 : ¬ ((y : Ordinal) → ¬ odef X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y)))) - → ¬ ((y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y))) - lemma2 not not2 = not ( λ y d → not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where - lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od y))) → (ord→od (od→ord x) =h= ψ (ord→od y)) - lemma3 {y} eq = subst (λ k → ord→od (od→ord x) =h= k ) oiso (o≡→== eq ) - lemma : ( (y : HOD) → ¬ (x =h= ψ y)) → ( (y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y)) ) - lemma not y not2 = not (ord→od y) (subst (λ k → k =h= ψ (ord→od y)) oiso ( proj2 not2 )) + lemma2 : ¬ ((y : Ordinal) → ¬ odef X y ∧ ((& x) ≡ & (ψ (* y)))) + → ¬ ((y : Ordinal) → ¬ odef X y ∧ (* (& x) =h= ψ (* y))) + lemma2 not not2 = not ( λ y d → not2 y (⟪ proj1 d , lemma3 (proj2 d)⟫)) where + lemma3 : {y : Ordinal } → (& x ≡ & (ψ (* y))) → (* (& x) =h= ψ (* y)) + lemma3 {y} eq = subst (λ k → * (& x) =h= k ) *iso (o≡→== eq ) + lemma : ( (y : HOD) → ¬ (x =h= ψ y)) → ( (y : Ordinal) → ¬ odef X y ∧ (* (& x) =h= ψ (* y)) ) + lemma not y not2 = not (* y) (subst (λ k → k =h= ψ (* y)) *iso ( proj2 not2 )) --- --- Power Set @@ -609,126 +609,123 @@ -- ∩-≡ : { 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 (d→∋ a x<a)) refl diso } ; + eq→ = λ {x} x<a → ⟪ odef-subst {_} {_} {b} {x} (inc (d→∋ a x<a)) refl &iso , x<a ⟫ ; eq← = λ {x} x<a∩b → proj2 x<a∩b } -- -- Transitive Set case -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is (Ord a) ∩ t =h= t -- OPwr (Ord a) is a sup of (Ord a) ∩ t, so OPwr (Ord a) ∋ t --- OPwr A = Ord ( sup-o ( λ x → od→ord ( A ∩ (ord→od x )) ) ) +-- OPwr A = Ord ( sup-o ( λ x → & ( A ∩ (* x )) ) ) -- ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t -ord-power← a t t→A = odef-subst {_} {_} {OPwr (Ord a)} {od→ord t} +ord-power← a t t→A = odef-subst {_} {_} {OPwr (Ord a)} {& t} lemma refl (lemma1 lemma-eq )where lemma-eq : ((Ord a) ∩ t) =h= t eq→ lemma-eq {z} w = proj2 w - eq← lemma-eq {z} w = record { proj2 = w ; - proj1 = odef-subst {_} {_} {(Ord a)} {z} - ( t→A (d→∋ t w)) refl diso } + eq← lemma-eq {z} w = ⟪ odef-subst {_} {_} {(Ord a)} {z} ( t→A (d→∋ t w)) refl &iso , w ⟫ 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 (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))) + → (eq : ((Ord a) ∩ t) =h= t) → & ((Ord a) ∩ (* (& t))) ≡ & t + lemma1 {a} {t} eq = subst (λ k → & ((Ord a) ∩ k) ≡ & t ) (sym *iso) (cong (λ k → & k ) (==→o≡ eq )) + lemma2 : (& t) o< (osuc (& (Ord a))) + lemma2 = ⊆→o≤ {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) &iso (t→A (d→∋ t x<t))) + lemma : & ((Ord a) ∩ (* (& t)) ) o< sup-o (Ord (osuc (& (Ord a)))) (λ x lt → & ((Ord a) ∩ (* x))) lemma = sup-o< _ lemma2 -- --- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first +-- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (& A)) first -- then replace of all elements of the Power set by A ∩ y -- --- Power A = Replace (OPwr (Ord (od→ord A))) ( λ y → A ∩ y ) +-- Power A = Replace (OPwr (Ord (& A))) ( λ y → A ∩ y ) -- we have oly double negation form because of the replacement axiom -- power→ : ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → ¬ ¬ (A ∋ x) power→ A t P∋t {x} t∋x = FExists _ lemma5 lemma4 where - a = od→ord A + a = & A lemma2 : ¬ ( (y : HOD) → ¬ (t =h= (A ∩ y))) - lemma2 = replacement→ {λ x → A ∩ x} (OPwr (Ord (od→ord A))) t P∋t + lemma2 = replacement→ {λ x → A ∩ x} (OPwr (Ord (& A))) t P∋t lemma3 : (y : HOD) → t =h= ( A ∩ y ) → ¬ ¬ (A ∋ x) lemma3 y eq not = not (proj1 (eq→ eq t∋x)) - lemma4 : ¬ ((y : Ordinal) → ¬ (t =h= (A ∩ ord→od y))) - lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t =h= ( A ∩ k )) (sym oiso) not1 )) - lemma5 : {y : Ordinal} → t =h= (A ∩ ord→od y) → ¬ ¬ (odef A (od→ord x)) - lemma5 {y} eq not = (lemma3 (ord→od y) eq) not + lemma4 : ¬ ((y : Ordinal) → ¬ (t =h= (A ∩ * y))) + lemma4 not = lemma2 ( λ y not1 → not (& y) (subst (λ k → t =h= ( A ∩ k )) (sym *iso) not1 )) + lemma5 : {y : Ordinal} → t =h= (A ∩ * y) → ¬ ¬ (odef A (& x)) + lemma5 {y} eq not = (lemma3 (* y) eq) not power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t -power← A t t→A = record { proj1 = lemma1 ; proj2 = lemma2 } where - a = od→ord A +power← A t t→A = ⟪ lemma1 , lemma2 ⟫ where + a = & A lemma0 : {x : HOD} → t ∋ x → Ord a ∋ x lemma0 {x} t∋x = c<→o< (t→A t∋x) lemma3 : OPwr (Ord a) ∋ t lemma3 = ord-power← a t lemma0 - lemma4 : (A ∩ ord→od (od→ord t)) ≡ t + lemma4 : (A ∩ * (& t)) ≡ t lemma4 = let open ≡-Reasoning in begin - A ∩ ord→od (od→ord t) - ≡⟨ cong (λ k → A ∩ k) oiso ⟩ + A ∩ * (& t) + ≡⟨ cong (λ k → A ∩ k) *iso ⟩ A ∩ t ≡⟨ sym (==→o≡ ( ∩-≡ {t} {A} t→A )) ⟩ t ∎ sup1 : Ordinal - sup1 = sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord ((Ord (od→ord A)) ∩ (ord→od x))) - lemma9 : def (od (Ord (Ordinals.osuc O (od→ord (Ord (od→ord A)))))) (od→ord (Ord (od→ord A))) + sup1 = sup-o (Ord (osuc (& (Ord (& A))))) (λ x A∋x → & ((Ord (& A)) ∩ (* x))) + lemma9 : def (od (Ord (Ordinals.osuc O (& (Ord (& A)))))) (& (Ord (& A))) lemma9 = <-osuc - 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 (d→∋ t lt))) - lemmac : ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A) )))) =h= Ord (od→ord A) + lemmab : & ((Ord (& A)) ∩ (* (& (Ord (& A) )))) o< sup1 + lemmab = sup-o< (Ord (osuc (& (Ord (& A))))) lemma9 + lemmad : Ord (osuc (& A)) ∋ t + lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) &iso (t→A (d→∋ t lt))) + lemmac : ((Ord (& A)) ∩ (* (& (Ord (& A) )))) =h= 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 + lemmaf : {x : Ordinal} → def (od ((Ord (& A)) ∩ (* (& (Ord (& A)))))) x → def (od (Ord (& A))) x lemmaf {x} lt = proj1 lt - lemmag : {x : Ordinal} → def (od (Ord (od→ord A))) x → def (od ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A)))))) x - lemmag {x} lt = record { proj1 = lt ; proj2 = subst (λ k → def (od k) x) (sym oiso) lt } - lemmae : od→ord ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A))))) ≡ od→ord (Ord (od→ord A)) - lemmae = cong (λ k → od→ord k ) ( ==→o≡ lemmac) - lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t) + lemmag : {x : Ordinal} → def (od (Ord (& A))) x → def (od ((Ord (& A)) ∩ (* (& (Ord (& A)))))) x + lemmag {x} lt = ⟪ lt , subst (λ k → def (od k) x) (sym *iso) lt ⟫ + lemmae : & ((Ord (& A)) ∩ (* (& (Ord (& A))))) ≡ & (Ord (& A)) + lemmae = cong (λ k → & k ) ( ==→o≡ lemmac) + lemma7 : def (od (OPwr (Ord (& A)))) (& t) lemma7 with osuc-≡< lemmad lemma7 | case2 lt = ordtrans (c<→o< lt) (subst (λ k → k o< sup1) lemmae lemmab ) - lemma7 | case1 eq with osuc-≡< (⊆→o≤ {ord→od (od→ord t)} {ord→od (od→ord (Ord (od→ord t)))} (λ {x} lt → lemmah lt )) where - lemmah : {x : Ordinal } → def (od (ord→od (od→ord t))) x → def (od (ord→od (od→ord (Ord (od→ord t))))) x - lemmah {x} lt = subst (λ k → def (od k) x ) (sym oiso) (subst (λ k → k o< (od→ord t)) - diso - (c<→o< (subst₂ (λ j k → def (od j) k) oiso (sym diso) lt ))) + lemma7 | case1 eq with osuc-≡< (⊆→o≤ {* (& t)} {* (& (Ord (& t)))} (λ {x} lt → lemmah lt )) where + lemmah : {x : Ordinal } → def (od (* (& t))) x → def (od (* (& (Ord (& t))))) x + lemmah {x} lt = subst (λ k → def (od k) x ) (sym *iso) (subst (λ k → k o< (& t)) + &iso + (c<→o< (subst₂ (λ j k → def (od j) k) *iso (sym &iso) lt ))) lemma7 | case1 eq | case1 eq1 = subst (λ k → k o< sup1) (trans lemmae lemmai) lemmab where - lemmai : od→ord (Ord (od→ord A)) ≡ od→ord t + lemmai : & (Ord (& A)) ≡ & t lemmai = let open ≡-Reasoning in begin - od→ord (Ord (od→ord A)) - ≡⟨ sym (cong (λ k → od→ord (Ord k)) eq) ⟩ - od→ord (Ord (od→ord t)) - ≡⟨ sym diso ⟩ - od→ord (ord→od (od→ord (Ord (od→ord t)))) + & (Ord (& A)) + ≡⟨ sym (cong (λ k → & (Ord k)) eq) ⟩ + & (Ord (& t)) + ≡⟨ sym &iso ⟩ + & (* (& (Ord (& t)))) ≡⟨ sym eq1 ⟩ - od→ord (ord→od (od→ord t)) - ≡⟨ diso ⟩ - od→ord t + & (* (& t)) + ≡⟨ &iso ⟩ + & t ∎ lemma7 | case1 eq | case2 lt = ordtrans lemmaj (subst (λ k → k o< sup1) lemmae lemmab ) where - lemmak : od→ord (ord→od (od→ord (Ord (od→ord t)))) ≡ od→ord (Ord (od→ord A)) + lemmak : & (* (& (Ord (& t)))) ≡ & (Ord (& A)) lemmak = let open ≡-Reasoning in begin - od→ord (ord→od (od→ord (Ord (od→ord t)))) - ≡⟨ diso ⟩ - od→ord (Ord (od→ord t)) - ≡⟨ cong (λ k → od→ord (Ord k)) eq ⟩ - od→ord (Ord (od→ord A)) + & (* (& (Ord (& t)))) + ≡⟨ &iso ⟩ + & (Ord (& t)) + ≡⟨ cong (λ k → & (Ord k)) eq ⟩ + & (Ord (& A)) ∎ - lemmaj : od→ord t o< od→ord (Ord (od→ord A)) - lemmaj = subst₂ (λ j k → j o< k ) diso lemmak lt - lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x))) - lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))) - lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 ) - lemma2 : def (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t) - lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where - lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) - lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym oiso) ( ∩-≡ {t} {A} t→A ))) + lemmaj : & t o< & (Ord (& A)) + lemmaj = subst₂ (λ j k → j o< k ) &iso lemmak lt + lemma1 : & t o< sup-o (OPwr (Ord (& A))) (λ x lt → & (A ∩ (* x))) + lemma1 = subst (λ k → & k o< sup-o (OPwr (Ord (& A))) (λ x lt → & (A ∩ (* x)))) + lemma4 (sup-o< (OPwr (Ord (& A))) lemma7 ) + lemma2 : def (in-codomain (OPwr (Ord (& A))) (_∩_ A)) (& t) + lemma2 not = ⊥-elim ( not (& t) (⟪ lemma3 , lemma6 ⟫) ) where + lemma6 : & t ≡ & (A ∩ * (& t)) + lemma6 = cong ( λ k → & k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym *iso) ( ∩-≡ {t} {A} t→A ))) ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a)) ord⊆power a = record { incl = λ {x} lt → power← (Ord a) x (lemma lt) } where - lemma : {x y : HOD} → od→ord x o< osuc a → x ∋ y → Ord a ∋ y + lemma : {x y : HOD} → & x o< osuc a → x ∋ y → Ord a ∋ y lemma lt y<x with osuc-≡< lt lemma lt y<x | case1 refl = c<→o< y<x lemma lt y<x | case2 x<a = ordtrans (c<→o< y<x) x<a @@ -737,28 +734,28 @@ continuum-hyphotheis a = Power (Ord a) ⊆ Ord (osuc a) extensionality0 : {A B : HOD } → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A =h= B -eq→ (extensionality0 {A} {B} eq ) {x} d = odef-iso {A} {B} (sym diso) (proj1 (eq (ord→od x))) d -eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso {B} {A} (sym diso) (proj2 (eq (ord→od x))) d +eq→ (extensionality0 {A} {B} eq ) {x} d = odef-iso {A} {B} (sym &iso) (proj1 (eq (* x))) d +eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso {B} {A} (sym &iso) (proj2 (eq (* x))) d extensionality : {A B w : HOD } → ((z : HOD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B) proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d infinity∅ : infinite ∋ od∅ -infinity∅ = odef-subst {_} {_} {infinite} {od→ord (od∅ )} iφ refl lemma where - lemma : o∅ ≡ od→ord od∅ +infinity∅ = odef-subst {_} {_} {infinite} {& (od∅ )} iφ refl lemma where + lemma : o∅ ≡ & od∅ lemma = let open ≡-Reasoning in begin o∅ - ≡⟨ sym diso ⟩ - od→ord ( ord→od o∅ ) - ≡⟨ cong ( λ k → od→ord k ) o∅≡od∅ ⟩ - od→ord od∅ + ≡⟨ sym &iso ⟩ + & ( * o∅ ) + ≡⟨ cong ( λ k → & k ) o∅≡od∅ ⟩ + & od∅ ∎ infinity : (x : HOD) → infinite ∋ x → infinite ∋ Union (x , (x , x )) -infinity x lt = odef-subst {_} {_} {infinite} {od→ord (Union (x , (x , x )))} ( isuc {od→ord x} lt ) refl lemma where - lemma : od→ord (Union (ord→od (od→ord x) , (ord→od (od→ord x) , ord→od (od→ord x)))) - ≡ od→ord (Union (x , (x , x))) - lemma = cong (λ k → od→ord (Union ( k , ( k , k ) ))) oiso +infinity x lt = odef-subst {_} {_} {infinite} {& (Union (x , (x , x )))} ( isuc {& x} lt ) refl lemma where + lemma : & (Union (* (& x) , (* (& x) , * (& x)))) + ≡ & (Union (x , (x , x))) + lemma = cong (λ k → & (Union ( k , ( k , k ) ))) *iso isZF : IsZF (HOD ) _∋_ _=h=_ od∅ _,_ Union Power Select Replace infinite isZF = record {
--- a/ODC.agda Fri Jul 31 17:54:52 2020 +0900 +++ b/ODC.agda Sat Aug 01 11:06:29 2020 +0900 @@ -30,9 +30,9 @@ -- mimimul and x∋minimal is an Axiom of choice minimal : (x : HOD ) → ¬ (x =h= od∅ )→ HOD -- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x ) - x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) ) + x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) ) -- minimality (may proved by ε-induction with LEM) - minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) ) + minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (& y) ) -- @@ -48,19 +48,19 @@ ppp {p} {a} d = proj2 d p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice -p∨¬p p with is-o∅ ( od→ord (pred-od p )) +p∨¬p p with is-o∅ ( & (pred-od p )) p∨¬p p | yes eq = case2 (¬p eq) where ps = pred-od p - eqo∅ : ps =h= od∅ → od→ord ps ≡ o∅ - eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) + eqo∅ : ps =h= od∅ → & ps ≡ o∅ + eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq)) lemma : ps =h= od∅ → p → ⊥ - lemma eq p0 = ¬x<0 {od→ord ps} (eq→ eq record { proj1 = eqo∅ eq ; proj2 = p0 } ) - ¬p : (od→ord ps ≡ o∅) → p → ⊥ - ¬p eq = lemma ( subst₂ (λ j k → j =h= k ) oiso o∅≡od∅ ( o≡→== eq )) + lemma eq p0 = ¬x<0 {& ps} (eq→ eq record { proj1 = eqo∅ eq ; proj2 = p0 } ) + ¬p : (& ps ≡ o∅) → p → ⊥ + ¬p eq = lemma ( subst₂ (λ j k → j =h= k ) *iso o∅≡od∅ ( o≡→== eq )) p∨¬p p | no ¬p = case1 (ppp {p} {minimal ps (λ eq → ¬p (eqo∅ eq))} lemma) where ps = pred-od p - eqo∅ : ps =h= od∅ → od→ord ps ≡ o∅ - eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) + eqo∅ : ps =h= od∅ → & ps ≡ o∅ + eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq)) lemma : ps ∋ minimal ps (λ eq → ¬p (eqo∅ eq)) lemma = x∋minimal ps (λ eq → ¬p (eqo∅ eq)) @@ -87,7 +87,7 @@ t1 = power→ A t PA∋t OrdP : ( x : Ordinal ) ( y : HOD ) → Dec ( Ord x ∋ y ) -OrdP x y with trio< x (od→ord y) +OrdP x y with trio< x (& y) OrdP x y | tri< a ¬b ¬c = no ¬c OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl ) OrdP x y | tri> ¬a ¬b c = yes c
--- a/OPair.agda Fri Jul 31 17:54:52 2020 +0900 +++ b/OPair.agda Sat Aug 01 11:06:29 2020 +0900 @@ -40,56 +40,56 @@ right (case1 t) = case2 t right (case2 t) = case1 t -ord≡→≡ : { x y : HOD } → od→ord x ≡ od→ord y → x ≡ y -ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq ) +ord≡→≡ : { x y : HOD } → & x ≡ & y → x ≡ y +ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong ( λ k → * k ) eq ) -od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y -od≡→≡ eq = subst₂ (λ j k → j ≡ k ) diso diso ( cong ( λ k → od→ord k ) eq ) +od≡→≡ : { x y : Ordinal } → * x ≡ * y → x ≡ y +od≡→≡ eq = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong ( λ k → & k ) eq ) eq-prod : { x x' y y' : HOD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' > eq-prod refl refl = refl xx=zy→x=y : {x y z : HOD } → ( x , x ) =h= ( z , y ) → x ≡ y -xx=zy→x=y {x} {y} eq with trio< (od→ord x) (od→ord y) -xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c with eq← eq {od→ord y} (case2 refl) +xx=zy→x=y {x} {y} eq with trio< (& x) (& y) +xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c with eq← eq {& y} (case2 refl) xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a ) xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a ) xx=zy→x=y {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b -xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c with eq← eq {od→ord y} (case2 refl) +xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c with eq← eq {& y} (case2 refl) xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c ) xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c ) prod-eq : { x x' y y' : HOD } → < x , y > =h= < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' ) -prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where +prod-eq {x} {x'} {y} {y'} eq = ⟪ lemmax , lemmay ⟫ where lemma2 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → z ≡ y lemma2 {x} {y} {z} eq = trans (sym (xx=zy→x=y lemma3 )) ( xx=zy→x=y eq ) where lemma3 : ( x , x ) =h= ( y , z ) lemma3 = ==-trans eq exg-pair lemma1 : {x y : HOD } → ( x , x ) =h= ( y , y ) → x ≡ y - lemma1 {x} {y} eq with eq← eq {od→ord y} (case2 refl) + lemma1 {x} {y} eq with eq← eq {& y} (case2 refl) lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s) lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s) lemma4 : {x y z : HOD } → ( x , y ) =h= ( x , z ) → y ≡ z - lemma4 {x} {y} {z} eq with eq← eq {od→ord z} (case2 refl) + lemma4 {x} {y} {z} eq with eq← eq {& z} (case2 refl) lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z ... | refl with lemma2 (==-sym eq ) ... | refl = refl lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z lemmax : x ≡ x' - lemmax with eq→ eq {od→ord (x , x)} (case1 refl) + lemmax with eq→ eq {& (x , x)} (case1 refl) lemmax | case1 s = lemma1 (ord→== s ) -- (x,x)≡(x',x') lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y' ... | refl = lemma1 (ord→== s ) lemmay : y ≡ y' lemmay with lemmax ... | refl with lemma4 eq -- with (x,y)≡(x,y') - ... | eq1 = lemma4 (ord→== (cong (λ k → od→ord k ) eq1 )) + ... | eq1 = lemma4 (ord→== (cong (λ k → & k ) eq1 )) -- -- unlike ordered pair, ZFProduct is not a HOD data ord-pair : (p : Ordinal) → Set n where - pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) ) + pair : (x y : Ordinal ) → ord-pair ( & ( < * x , * y > ) ) ZFProduct : OD ZFProduct = record { def = λ x → ord-pair x } @@ -101,55 +101,55 @@ pi1 : { p : Ordinal } → ord-pair p → Ordinal pi1 ( pair x y) = x -π1 : { p : HOD } → def ZFProduct (od→ord p) → HOD -π1 lt = ord→od (pi1 lt ) +π1 : { p : HOD } → def ZFProduct (& p) → HOD +π1 lt = * (pi1 lt ) pi2 : { p : Ordinal } → ord-pair p → Ordinal pi2 ( pair x y ) = y -π2 : { p : HOD } → def ZFProduct (od→ord p) → HOD -π2 lt = ord→od (pi2 lt ) +π2 : { p : HOD } → def ZFProduct (& p) → HOD +π2 lt = * (pi2 lt ) -op-cons : { ox oy : Ordinal } → def ZFProduct (od→ord ( < ord→od ox , ord→od oy > )) +op-cons : { ox oy : Ordinal } → def ZFProduct (& ( < * ox , * oy > )) op-cons {ox} {oy} = pair ox oy def-subst : {Z : OD } {X : Ordinal }{z : OD } {x : Ordinal }→ def Z X → Z ≡ z → X ≡ x → def z x def-subst df refl refl = df -p-cons : ( x y : HOD ) → def ZFProduct (od→ord ( < x , y >)) -p-cons x y = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl ( +p-cons : ( x y : HOD ) → def ZFProduct (& ( < x , y >)) +p-cons x y = def-subst {_} {_} {ZFProduct} {& (< x , y >)} (pair (& x) ( & y )) refl ( let open ≡-Reasoning in begin - od→ord < ord→od (od→ord x) , ord→od (od→ord y) > - ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩ - od→ord < x , y > + & < * (& x) , * (& y) > + ≡⟨ cong₂ (λ j k → & < j , k >) *iso *iso ⟩ + & < x , y > ∎ ) -op-iso : { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op +op-iso : { op : Ordinal } → (q : ord-pair op ) → & < * (pi1 q) , * (pi2 q) > ≡ op op-iso (pair ox oy) = refl -p-iso : { x : HOD } → (p : def ZFProduct (od→ord x) ) → < π1 p , π2 p > ≡ x +p-iso : { x : HOD } → (p : def ZFProduct (& x) ) → < π1 p , π2 p > ≡ x p-iso {x} p = ord≡→≡ (op-iso p) -p-pi1 : { x y : HOD } → (p : def ZFProduct (od→ord < x , y >) ) → π1 p ≡ x +p-pi1 : { x y : HOD } → (p : def ZFProduct (& < x , y >) ) → π1 p ≡ x p-pi1 {x} {y} p = proj1 ( prod-eq ( ord→== (op-iso p) )) -p-pi2 : { x y : HOD } → (p : def ZFProduct (od→ord < x , y >) ) → π2 p ≡ y +p-pi2 : { x y : HOD } → (p : def ZFProduct (& < x , y >) ) → π2 p ≡ y p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p))) -ω-pair : {x y : HOD} → {m : Ordinal} → od→ord x o< next m → od→ord y o< next m → od→ord (x , y) o< next m +ω-pair : {x y : HOD} → {m : Ordinal} → & x o< next m → & y o< next m → & (x , y) o< next m ω-pair lx ly = next< (omax<nx lx ly ) ho< -ω-opair : {x y : HOD} → {m : Ordinal} → od→ord x o< next m → od→ord y o< next m → od→ord < x , y > o< next m +ω-opair : {x y : HOD} → {m : Ordinal} → & x o< next m → & y o< next m → & < x , y > o< next m ω-opair {x} {y} {m} lx ly = lemma0 where - lemma0 : od→ord < x , y > o< next m + lemma0 : & < x , y > o< next m lemma0 = osucprev (begin - osuc (od→ord < x , y >) + osuc (& < x , y >) <⟨ osuc<nx ho< ⟩ - next (omax (od→ord (x , x)) (od→ord (x , y))) + next (omax (& (x , x)) (& (x , y))) ≡⟨ cong (λ k → next k) (sym ( omax≤ _ _ pair-xx<xy )) ⟩ - next (osuc (od→ord (x , y))) + next (osuc (& (x , y))) ≡⟨ sym (nexto≡) ⟩ - next (od→ord (x , y)) + next (& (x , y)) ≤⟨ x<ny→≤next (ω-pair lx ly) ⟩ next m ∎ ) where @@ -159,23 +159,23 @@ A ⊗ B = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) )) product→ : {A B a b : HOD} → A ∋ a → B ∋ b → ( A ⊗ B ) ∋ < a , b > -product→ {A} {B} {a} {b} A∋a B∋b = λ t → t (od→ord (Replace A (λ a → < a , b >))) - record { proj1 = lemma1 ; proj2 = subst (λ k → odef k (od→ord < a , b >)) (sym oiso) lemma2 } where - lemma1 : odef (Replace B (λ b₁ → Replace A (λ a₁ → < a₁ , b₁ >))) (od→ord (Replace A (λ a₁ → < a₁ , b >))) +product→ {A} {B} {a} {b} A∋a B∋b = λ t → t (& (Replace A (λ a → < a , b >))) + ⟪ lemma1 , subst (λ k → odef k (& < a , b >)) (sym *iso) lemma2 ⟫ where + lemma1 : odef (Replace B (λ b₁ → Replace A (λ a₁ → < a₁ , b₁ >))) (& (Replace A (λ a₁ → < a₁ , b >))) lemma1 = replacement← B b B∋b - lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (od→ord < a , b >) + lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (& < a , b >) lemma2 = replacement← A a A∋a -x<nextA : {A x : HOD} → A ∋ x → od→ord x o< next (odmax A) +x<nextA : {A x : HOD} → A ∋ x → & x o< next (odmax A) x<nextA {A} {x} A∋x = ordtrans (c<→o< {x} {A} A∋x) ho< -A<Bnext : {A B x : HOD} → od→ord A o< od→ord B → A ∋ x → od→ord x o< next (odmax B) +A<Bnext : {A B x : HOD} → & A o< & B → A ∋ x → & x o< next (odmax B) A<Bnext {A} {B} {x} lt A∋x = osucprev (begin - osuc (od→ord x) + osuc (& x) <⟨ osucc (c<→o< A∋x) ⟩ - osuc (od→ord A) + osuc (& A) <⟨ osucc lt ⟩ - osuc (od→ord B) + osuc (& B) <⟨ osuc<nx ho< ⟩ next (odmax B) ∎ ) where open o≤-Reasoning O @@ -186,21 +186,21 @@ where lemma : (y : Ordinal) → ( ord-pair y ∧ ((p : ord-pair y) → odef A (pi1 p) ∧ odef B (pi2 p))) → y o< omax (next (odmax A)) (next (odmax B)) lemma y lt with proj1 lt - lemma p lt | pair x y with trio< (od→ord A) (od→ord B) - lemma p lt | pair x y | tri< a ¬b ¬c = ordtrans (ω-opair (A<Bnext a (subst (λ k → odef A k ) (sym diso) + lemma p lt | pair x y with trio< (& A) (& B) + lemma p lt | pair x y | tri< a ¬b ¬c = ordtrans (ω-opair (A<Bnext a (subst (λ k → odef A k ) (sym &iso) (proj1 (proj2 lt (pair x y))))) (lemma1 (proj2 (proj2 lt (pair x y))))) (omax-y _ _ ) where - lemma1 : odef B y → od→ord (ord→od y) o< next (HOD.odmax B) + lemma1 : odef B y → & (* y) o< next (HOD.odmax B) lemma1 lt = x<nextA {B} (d→∋ B lt) lemma p lt | pair x y | tri≈ ¬a b ¬c = ordtrans (ω-opair (x<nextA {A} (d→∋ A ((proj1 (proj2 lt (pair x y)))))) lemma2 ) (omax-x _ _ ) where - lemma2 : od→ord (ord→od y) o< next (HOD.odmax A) - lemma2 = ordtrans ( subst (λ k → od→ord (ord→od y) o< k ) (sym b) (c<→o< (d→∋ B ((proj2 (proj2 lt (pair x y))))))) ho< + lemma2 : & (* y) o< next (HOD.odmax A) + lemma2 = ordtrans ( subst (λ k → & (* y) o< k ) (sym b) (c<→o< (d→∋ B ((proj2 (proj2 lt (pair x y))))))) ho< lemma p lt | pair x y | tri> ¬a ¬b c = ordtrans (ω-opair (x<nextA {A} (d→∋ A ((proj1 (proj2 lt (pair x y)))))) - (A<Bnext c (subst (λ k → odef B k ) (sym diso) (proj2 (proj2 lt (pair x y)))))) (omax-x _ _ ) + (A<Bnext c (subst (λ k → odef B k ) (sym &iso) (proj2 (proj2 lt (pair x y)))))) (omax-x _ _ ) ZFP⊆⊗ : {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x -ZFP⊆⊗ {A} {B} {px} record { proj1 = (pair x y) ; proj2 = p2 } = product→ (d→∋ A (proj1 (p2 (pair x y) ))) (d→∋ B (proj2 (p2 (pair x y) ))) +ZFP⊆⊗ {A} {B} {px} ⟪ (pair x y) , p2 ⟫ = product→ (d→∋ A (proj1 (p2 (pair x y) ))) (d→∋ B (proj2 (p2 (pair x y) ))) -- axiom of choice required --- ⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → def ZFProduct (od→ord x) --- ⊗⊆ZFP {A} {B} {x} lt = subst (λ k → ord-pair (od→ord k )) {!!} op-cons +-- ⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → def ZFProduct (& x) +-- ⊗⊆ZFP {A} {B} {x} lt = subst (λ k → ord-pair (& k )) {!!} op-cons
--- a/VL.agda Fri Jul 31 17:54:52 2020 +0900 +++ b/VL.agda Sat Aug 01 11:06:29 2020 +0900 @@ -30,15 +30,21 @@ -- V α := ⋃ { V β | β < α } V : ( β : Ordinal ) → HOD -V β = TransFinite1 Vβ₁ β where - Vβ₁ : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD ) → HOD - Vβ₁ x Vβ₀ with trio< x o∅ - Vβ₁ x Vβ₀ | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a) - Vβ₁ x Vβ₀ | tri≈ ¬a refl ¬c = Ord o∅ - Vβ₁ x Vβ₀ | tri> ¬a ¬b c with Oprev-p x - Vβ₁ x Vβ₀ | tri> ¬a ¬b c | yes p = Power ( Vβ₀ (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x p) <-osuc )) - Vβ₁ x Vβ₀ | tri> ¬a ¬b c | no ¬p = - record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) → odef (Vβ₀ y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt } +V β = TransFinite1 V1 β where + V1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD ) → HOD + V1 x V0 with trio< x o∅ + V1 x V0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a) + V1 x V0 | tri≈ ¬a refl ¬c = Ord o∅ + V1 x V0 | tri> ¬a ¬b c with Oprev-p x + V1 x V0 | tri> ¬a ¬b c | yes p = Power ( V0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x p) <-osuc )) + V1 x V0 | tri> ¬a ¬b c | no ¬p = + record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) → odef (V0 y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt } + +-- +-- L ⊆ HOD ⊆ V +-- +-- HOD=V : (x : HOD) → V (odmax x) ∋ x +-- HOD=V x = {!!} -- -- Definition for Power Set @@ -58,15 +64,15 @@ -- V α := ⋃ { L β | β < α } L : ( β : Ordinal ) → Definitions → HOD -L β D = TransFinite1 Lβ₁ β where - Lβ₁ : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD ) → HOD - Lβ₁ x Lβ₀ with trio< x o∅ - Lβ₁ x Lβ₀ | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a) - Lβ₁ x Lβ₀ | tri≈ ¬a refl ¬c = Ord o∅ - Lβ₁ x Lβ₀ | tri> ¬a ¬b c with Oprev-p x - Lβ₁ x Lβ₀ | tri> ¬a ¬b c | yes p = Df D ( Lβ₀ (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x p) <-osuc )) - Lβ₁ x Lβ₀ | tri> ¬a ¬b c | no ¬p = - record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) → odef (Lβ₀ y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt } +L β D = TransFinite1 L1 β where + L1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD ) → HOD + L1 x L0 with trio< x o∅ + L1 x L0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a) + L1 x L0 | tri≈ ¬a refl ¬c = Ord o∅ + L1 x L0 | tri> ¬a ¬b c with Oprev-p x + L1 x L0 | tri> ¬a ¬b c | yes p = Df D ( L0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x p) <-osuc )) + L1 x L0 | tri> ¬a ¬b c | no ¬p = + record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) → odef (L0 y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt } V=L0 : Set (suc n) V=L0 = (x : Ordinal) → V x ≡ L x record { Definition = λ y → y }
--- a/cardinal.agda Fri Jul 31 17:54:52 2020 +0900 +++ b/cardinal.agda Sat Aug 01 11:06:29 2020 +0900 @@ -33,7 +33,7 @@ Func : OD Func = record { def = λ x → def ZFProduct x - ∧ ( (a b c : Ordinal) → odef (ord→od x) (od→ord < ord→od a , ord→od b >) ∧ odef (ord→od x) (od→ord < ord→od a , ord→od c >) → b ≡ c ) } + ∧ ( (a b c : Ordinal) → odef (* x) (& < * a , * b >) ∧ odef (* x) (& < * a , * c >) → b ≡ c ) } FuncP : ( A B : HOD ) → HOD FuncP A B = record { od = record { def = λ x → odef (ZFP A B) x @@ -41,32 +41,32 @@ ; odmax = odmax (ZFP A B) ; <odmax = λ lt → <odmax (ZFP A B) (proj1 lt) } Func∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x ) - → def Func (od→ord (Replace A (λ x → < x , f x > ))) + → def Func (& (Replace A (λ x → < x , f x > ))) Func∋f = {!!} FuncP∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x ) - → odef (FuncP A B) (od→ord (Replace A (λ x → < x , f x > ))) + → odef (FuncP A B) (& (Replace A (λ x → < x , f x > ))) FuncP∋f = {!!} --- Func→f : {A B f x : HOD} → def Func (od→ord f) → (x : HOD ) → A ∋ x → ( HOD ∧ ((y : HOD ) → B ∋ y )) +-- Func→f : {A B f x : HOD} → def Func (& f) → (x : HOD ) → A ∋ x → ( HOD ∧ ((y : HOD ) → B ∋ y )) -- Func→f = {!!} --- Func₁ : {A B f : HOD} → def Func (od→ord f) → {!!} +-- Func₁ : {A B f : HOD} → def Func (& f) → {!!} -- Func₁ = {!!} --- Cod : {A B f : HOD} → def Func (od→ord f) → {!!} +-- Cod : {A B f : HOD} → def Func (& f) → {!!} -- Cod = {!!} --- 1-1 : {A B f : HOD} → def Func (od→ord f) → {!!} +-- 1-1 : {A B f : HOD} → def Func (& f) → {!!} -- 1-1 = {!!} --- onto : {A B f : HOD} → def Func (od→ord f) → {!!} +-- onto : {A B f : HOD} → def Func (& f) → {!!} -- onto = {!!} record Bijection (A B : Ordinal ) : Set n where field fun→ : Ordinal → Ordinal fun← : Ordinal → Ordinal - fun→inA : (x : Ordinal) → odef (ord→od A) ( fun→ x ) - fun←inB : (x : Ordinal) → odef (ord→od B) ( fun← x ) - fiso→ : (x : Ordinal ) → odef (ord→od B) x → fun→ ( fun← x ) ≡ x - fiso← : (x : Ordinal ) → odef (ord→od A) x → fun← ( fun→ x ) ≡ x + fun→inA : (x : Ordinal) → odef (* A) ( fun→ x ) + fun←inB : (x : Ordinal) → odef (* B) ( fun← x ) + fiso→ : (x : Ordinal ) → odef (* B) x → fun→ ( fun← x ) ≡ x + fiso← : (x : Ordinal ) → odef (* A) x → fun← ( fun→ x ) ≡ x Card : OD Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x }
--- a/filter.agda Fri Jul 31 17:54:52 2020 +0900 +++ b/filter.agda Sat Aug 01 11:06:29 2020 +0900 @@ -77,8 +77,8 @@ ... | case1 p∈P = case1 p∈P ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where lemma5 : ((p ∪ q ) ∩ (L ＼ p)) =h= (q ∩ (L ＼ p)) - lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt } - ; eq← = λ {x} lt → record { proj1 = case2 (proj1 lt) ; proj2 = proj2 lt } + lemma5 = record { eq→ = λ {x} lt → ⟪ lemma4 x lt , proj2 lt ⟫ + ; eq← = λ {x} lt → ⟪ case2 (proj1 lt) , proj2 lt ⟫ } where lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L ＼ p)) x → odef q x lemma4 x lt with proj1 lt @@ -105,8 +105,8 @@ p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L ＼ p)) eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x) eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x - eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p }) - eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef L k ) diso (incl p⊆L ( subst (λ k → odef p k) (sym diso) p∋x )) + eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 ⟪ lt , ¬p ⟫ + eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef L k ) &iso (incl p⊆L ( subst (λ k → odef p k) (sym &iso) p∋x )) eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p lemma : (p : HOD) → p ⊆ L → filter P ∋ (p ∪ (L ＼ p)) lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L
--- a/generic-filter.agda Fri Jul 31 17:54:52 2020 +0900 +++ b/generic-filter.agda Sat Aug 01 11:06:29 2020 +0900 @@ -69,9 +69,9 @@ data Hω2 : (i : Nat) ( x : Ordinal ) → Set n where hφ : Hω2 0 o∅ h0 : {i : Nat} {x : Ordinal } → Hω2 i x → - Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 0 >) , ord→od x ))) + Hω2 (Suc i) (& (Union ((< nat→ω i , nat→ω 0 >) , * x ))) h1 : {i : Nat} {x : Ordinal } → Hω2 i x → - Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 1 >) , ord→od x ))) + Hω2 (Suc i) (& (Union ((< nat→ω i , nat→ω 1 >) , * x ))) he : {i : Nat} {x : Ordinal } → Hω2 i x → Hω2 (Suc i) x @@ -85,13 +85,13 @@ HODω2 : HOD HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where P : (i j : Nat) (x : Ordinal ) → HOD - P i j x = ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) , ord→od x - nat1 : (i : Nat) (x : Ordinal) → od→ord (nat→ω i) o< next x + P i j x = ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) , * x + nat1 : (i : Nat) (x : Ordinal) → & (nat→ω i) o< next x nat1 i x = next< nexto∅ ( <odmax infinite (ω∋nat→ω {i})) - lemma1 : (i j : Nat) (x : Ordinal ) → osuc (od→ord (P i j x)) o< next x + lemma1 : (i j : Nat) (x : Ordinal ) → osuc (& (P i j x)) o< next x lemma1 i j x = osuc<nx (pair-<xy (pair-<xy (pair-<xy (nat1 i x) (nat1 i x) ) (pair-<xy (nat1 i x) (nat1 j x) ) ) - (subst (λ k → k o< next x) (sym diso) x<nx )) - lemma : (i j : Nat) (x : Ordinal ) → od→ord (Union (P i j x)) o< next x + (subst (λ k → k o< next x) (sym &iso) x<nx )) + lemma : (i j : Nat) (x : Ordinal ) → & (Union (P i j x)) o< next x lemma i j x = next< (lemma1 i j x ) ho< odmax0 : {y : Ordinal} → Hω2r y → y o< next o∅ odmax0 {y} r with hω2 r @@ -125,7 +125,7 @@ ω→2f x lt n | no ¬p = i0 fω→2-sel : ( f : Nat → Two ) (x : HOD) → Set n -fω→2-sel f x = (infinite ∋ x) ∧ ( (lt : odef infinite (od→ord x) ) → f (ω→nat x lt) ≡ i1 ) +fω→2-sel f x = (infinite ∋ x) ∧ ( (lt : odef infinite (& x) ) → f (ω→nat x lt) ≡ i1 ) fω→2 : (Nat → Two) → HOD fω→2 f = Select infinite (fω→2-sel f) @@ -177,7 +177,7 @@ -- PGHOD : (i : Nat) → (C : CountableOrdinal) → (P : HOD) → (p : Ordinal) → HOD PGHOD i C P p = record { od = record { def = λ x → - odef P x ∧ odef (ord→od (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (ord→od p) y → odef (ord→od x) y ) } + odef P x ∧ odef (* (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (* p) y → odef (* x) y ) } ; odmax = odmax P ; <odmax = λ {y} lt → <odmax P (proj1 lt) } --- @@ -186,7 +186,7 @@ next-p : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (p : Ordinal) → Ordinal next-p C P i p with ODC.decp O ( PGHOD i C P p =h= od∅ ) next-p C P i p | yes y = p -next-p C P i p | no not = od→ord (ODC.minimal O (PGHOD i C P p ) not) +next-p C P i p | no not = & (ODC.minimal O (PGHOD i C P p ) not) --- -- ascendant search on p(n) @@ -201,7 +201,7 @@ record PDN (C : CountableOrdinal) (P : HOD ) (x : Ordinal) : Set n where field gr : Nat - pn<gr : (y : Ordinal) → odef (ord→od x) y → odef (ord→od (find-p C P gr o∅)) y + pn<gr : (y : Ordinal) → odef (* x) y → odef (* (find-p C P gr o∅)) y px∈ω : odef (Power P) x open PDN @@ -219,7 +219,7 @@ -- Generic Filter on Power P for HOD's Countable Ordinal (G ⊆ Power P ≡ G i.e. Nat → P → Set ) -- -- p 0 ≡ ∅ --- p (suc n) = if ∃ q ∈ ord→od ( ctl→ n ) ∧ p n ⊆ q → q (axiom of choice) +-- p (suc n) = if ∃ q ∈ * ( ctl→ n ) ∧ p n ⊆ q → q (axiom of choice) --- else p n P-GenericFilter : (C : CountableOrdinal) → (P : HOD ) → GenericFilter P @@ -229,17 +229,17 @@ } where P∅ : {P : HOD} → odef (Power P) o∅ P∅ {P} = subst (λ k → odef (Power P) k ) ord-od∅ (lemma o∅ o∅≡od∅) where - lemma : (x : Ordinal ) → ord→od x ≡ od∅ → odef (Power P) (od→ord od∅) + lemma : (x : Ordinal ) → * x ≡ od∅ → odef (Power P) (& od∅) lemma x eq = power← P od∅ (λ {x} lt → ⊥-elim (¬x<0 lt )) - x<y→∋ : {x y : Ordinal} → odef (ord→od x) y → ord→od x ∋ ord→od y - x<y→∋ {x} {y} lt = subst (λ k → odef (ord→od x) k ) (sym diso) lt - find-p-⊆P : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x y : Ordinal) → odef (Power P) x → odef (ord→od (find-p C P i x)) y → odef P y - find-p-⊆P C P Zero x y Px Py = subst (λ k → odef P k ) diso - ( incl (ODC.power→⊆ O P (ord→od x) (d→∋ (Power P) Px)) (x<y→∋ Py)) + x<y→∋ : {x y : Ordinal} → odef (* x) y → * x ∋ * y + x<y→∋ {x} {y} lt = subst (λ k → odef (* x) k ) (sym &iso) lt + find-p-⊆P : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x y : Ordinal) → odef (Power P) x → odef (* (find-p C P i x)) y → odef P y + find-p-⊆P C P Zero x y Px Py = subst (λ k → odef P k ) &iso + ( incl (ODC.power→⊆ O P (* x) (d→∋ (Power P) Px)) (x<y→∋ Py)) find-p-⊆P C P (Suc i) x y Px Py = find-p-⊆P C P i (next-p C P i x) y {!!} {!!} f⊆PL : PDHOD C P ⊆ Power P f⊆PL = record { incl = λ {x} lt → power← P x (λ {y} y<x → - find-p-⊆P C P (gr lt) o∅ (od→ord y) P∅ (pn<gr lt (od→ord y) (subst (λ k → odef k (od→ord y)) (sym oiso) y<x))) } + find-p-⊆P C P (gr lt) o∅ (& y) P∅ (pn<gr lt (& y) (subst (λ k → odef k (& y)) (sym *iso) y<x))) } open GenericFilter
--- a/logic.agda Fri Jul 31 17:54:52 2020 +0900 +++ b/logic.agda Sat Aug 01 11:06:29 2020 +0900 @@ -17,6 +17,7 @@ false : Bool record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where + constructor ⟪_,_⟫ field proj1 : A proj2 : B
--- a/ordinal.agda Fri Jul 31 17:54:52 2020 +0900 +++ b/ordinal.agda Sat Aug 01 11:06:29 2020 +0900 @@ -171,14 +171,14 @@ → ∀ (x : Ordinal) → ψ x TransFinite {n} {m} {ψ} caseΦ caseOSuc x = proj1 (TransFinite1 (lv x) (ord x) ) where TransFinite1 : (lx : Nat) (ox : OrdinalD lx ) → ψ (ordinal lx ox) ∧ ( ( (x : Ordinal {suc n} ) → x o< ordinal lx ox → ψ x ) ) - TransFinite1 Zero (Φ 0) = record { proj1 = caseΦ Zero lemma ; proj2 = lemma1 } where + TransFinite1 Zero (Φ 0) = ⟪ caseΦ Zero lemma , lemma1 ⟫ where lemma : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x lemma x (case1 ()) lemma x (case2 ()) lemma1 : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x lemma1 x (case1 ()) lemma1 x (case2 ()) - TransFinite1 (Suc lx) (Φ (Suc lx)) = record { proj1 = caseΦ (Suc lx) (λ x → lemma (lv x) (ord x)) ; proj2 = (λ x → lemma (lv x) (ord x)) } where + TransFinite1 (Suc lx) (Φ (Suc lx)) = ⟪ caseΦ (Suc lx) (λ x → lemma (lv x) (ord x)) , (λ x → lemma (lv x) (ord x)) ⟫ where lemma0 : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy o< ordinal lx (Φ lx) → ψ (ordinal ly oy) lemma0 ly oy lt = proj2 ( TransFinite1 lx (Φ lx) ) (ordinal ly oy) lt lemma : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy o< ordinal (Suc lx) (Φ (Suc lx)) → ψ (ordinal ly oy) @@ -197,7 +197,7 @@ lemma2 y lt2 | case2 (case1 lt3) = proj2 (TransFinite1 lx (Φ lx)) y (case1 (<-trans lt3 lt1 )) lemma2 y lt2 | case2 (case2 lt3) with d<→lv lt3 ... | refl = proj2 (TransFinite1 lx (Φ lx)) y (case1 lt1) - TransFinite1 lx (OSuc lx ox) = record { proj1 = caseOSuc lx ox lemma ; proj2 = lemma } where + TransFinite1 lx (OSuc lx ox) = ⟪ caseOSuc lx ox lemma , lemma ⟫ where lemma : (y : Ordinal) → y o< ordinal lx (OSuc lx ox) → ψ y lemma y lt with osuc-≡< lt lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox )