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

comparison HOD.agda @ 114:89204edb71fa

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
f x d
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 25 Jun 2019 21:05:07 +0900
parents 5f97ebaeb89b
children 277c2f3b8acb
comparison
equal deleted inserted replaced
113:5f97ebaeb89b 114:89204edb71fa
15 -- Ordinal Definable Set 15 -- Ordinal Definable Set
16 16
17 record HOD {n : Level} : Set (suc n) where 17 record HOD {n : Level} : Set (suc n) where
18 field 18 field
19 def : (x : Ordinal {n} ) → Set n 19 def : (x : Ordinal {n} ) → Set n
20 otrans : {x y : Ordinal {n} } → def x → y o< x → def y 20 otrans : {x : Ordinal {n} } → def x → { y : Ordinal {n} } → y o< x → def y
21 21
22 open HOD 22 open HOD
23 open import Data.Unit 23 open import Data.Unit
24 24
25 open Ordinal 25 open Ordinal
44 eq-trans x=y y=z = record { eq→ = λ t → eq→ y=z ( eq→ x=y t) ; eq← = λ t → eq← x=y ( eq← y=z t) } 44 eq-trans x=y y=z = record { eq→ = λ t → eq→ y=z ( eq→ x=y t) ; eq← = λ t → eq← x=y ( eq← y=z t) }
45 45
46 -- Ordinal in HOD ( and ZFSet ) 46 -- Ordinal in HOD ( and ZFSet )
47 Ord : { n : Level } → ( a : Ordinal {n} ) → HOD {n} 47 Ord : { n : Level } → ( a : Ordinal {n} ) → HOD {n}
48 Ord {n} a = record { def = λ y → y o< a ; otrans = lemma } where 48 Ord {n} a = record { def = λ y → y o< a ; otrans = lemma } where
49 lemma : {x y : Ordinal} → x o< a → y o< x → y o< a 49 lemma : {x : Ordinal} → x o< a → {y : Ordinal} → y o< x → y o< a
50 lemma {x} {y} x<a y<x = ordtrans {n} {y} {x} {a} y<x x<a 50 lemma {x} x<a {y} y<x = ordtrans {n} {y} {x} {a} y<x x<a
51 51
52 -- od∅ : {n : Level} → HOD {n} 52 -- od∅ : {n : Level} → HOD {n}
53 -- od∅ {n} = record { def = λ _ → Lift n ⊥ } 53 -- od∅ {n} = record { def = λ _ → Lift n ⊥ }
54 od∅ : {n : Level} → HOD {n} 54 od∅ : {n : Level} → HOD {n}
55 od∅ {n} = Ord o∅ 55 od∅ {n} = Ord o∅
81 _c≤_ : {n : Level} → HOD {n} → HOD {n} → Set (suc n) 81 _c≤_ : {n : Level} → HOD {n} → HOD {n} → Set (suc n)
82 a c≤ b = (a ≡ b) ∨ ( b ∋ a ) 82 a c≤ b = (a ≡ b) ∨ ( b ∋ a )
83 83
84 cseq : {n : Level} → HOD {n} → HOD {n} 84 cseq : {n : Level} → HOD {n} → HOD {n}
85 cseq x = record { def = λ y → osuc y o< (od→ord x) ; otrans = lemma } where 85 cseq x = record { def = λ y → osuc y o< (od→ord x) ; otrans = lemma } where
86 lemma : {ox oy : Ordinal} → osuc ox o< od→ord x → oy o< ox → osuc oy o< od→ord x 86 lemma : {ox : Ordinal} → osuc ox o< od→ord x → { oy : Ordinal}→ oy o< ox → osuc oy o< od→ord x
87 lemma {ox} {oy} oox<Ox oy<ox = ordtrans (osucc oy<ox ) oox<Ox 87 lemma {ox} oox<Ox {oy} oy<ox = ordtrans (osucc oy<ox ) oox<Ox
88 88
89 def-subst : {n : Level } {Z : HOD {n}} {X : Ordinal {n} }{z : HOD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z → X ≡ x → def z x 89 def-subst : {n : Level } {Z : HOD {n}} {X : Ordinal {n} }{z : HOD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z → X ≡ x → def z x
90 def-subst df refl refl = df 90 def-subst df refl refl = df
91 91
92 o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → Ord y ∋ Ord x 92 o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → Ord y ∋ Ord x
245 ; isZF = isZF 245 ; isZF = isZF
246 } where 246 } where
247 Replace : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n} 247 Replace : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n}
248 Replace X ψ = sup-od ψ 248 Replace X ψ = sup-od ψ
249 Select : (X : HOD {suc n} ) → ((x : HOD {suc n} ) → X ∋ x → Set (suc n) ) → HOD {suc n} 249 Select : (X : HOD {suc n} ) → ((x : HOD {suc n} ) → X ∋ x → Set (suc n) ) → HOD {suc n}
250 Select X ψ = record { def = λ x → (d : def X x ) → f x d ; otrans = ftrans } where 250 Select X ψ = record { def = λ x → (d : def X x) → f x d ; otrans = λ {x} g {y} d1 → {!!} } where
251 f : (x : Ordinal {suc n}) → (d : def X x ) → Set (suc n) 251 f : (x : Ordinal {suc n}) → (d : def X x ) → Set (suc n)
252 f x d = ψ (ord→od x) (subst (λ k → def X k ) (sym diso) d) 252 f x d = ψ (ord→od x) (subst (λ k → def X k ) (sym diso) d)
253 ftrans : {x y : Ordinal} → ((d : def X x) → f x d) → y o< x → (d : def X y) → f y d 253 ftrans' : {x : Ordinal} ( g : (x : Ordinal {suc n} ) (d : def X x ) → f x d ) → {y : Ordinal} → y o< x → (d : def X y) → f y d
254 ftrans {x} {y} g = TransFinite {suc n} {λ y1 → (y1<x : y1 o< x) → (d1 : def X y1) → f y1 d1} lemma1 lemma2 y where 254 ftrans' {x} g {y} y<x d = g y d
255 lemma1 : (lx : Nat) → record { lv = lx ; ord = Φ lx } o< x → (d1 : def X (record { lv = lx ; ord = Φ lx })) → f (record { lv = lx ; ord = Φ lx }) d1
256 lemma1 = {!!}
257 lemma2 : (lx : Nat) (x₁ : OrdinalD lx) → (record { lv = lx ; ord = x₁ } o< x →
258 (d1 : def X (record { lv = lx ; ord = x₁ })) → f (record { lv = lx ; ord = x₁ }) d1) → record { lv = lx ; ord = OSuc lx x₁ } o< x →
259 (d1 : def X (record { lv = lx ; ord = OSuc lx x₁ })) → f (record { lv = lx ; ord = OSuc lx x₁ }) d1
260 lemma2 = {!!}
261 _,_ : HOD {suc n} → HOD {suc n} → HOD {suc n} 255 _,_ : HOD {suc n} → HOD {suc n} → HOD {suc n}
262 x , y = Ord (omax (od→ord x) (od→ord y)) 256 x , y = Ord (omax (od→ord x) (od→ord y))
263 Union : HOD {suc n} → HOD {suc n} 257 Union : HOD {suc n} → HOD {suc n}
264 Union U = cseq U 258 Union U = cseq U
265 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x ) 259 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x )