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

comparison src/generic-filter.agda @ 1264:440ebaf9f707

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
generic filter done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 20 Mar 2023 08:15:10 +0900
parents d04fb4b2c72b
children 48d37da98331
comparison
equal deleted inserted replaced
1263:d04fb4b2c72b 1264:440ebaf9f707
350 -- 350 --
351 -- val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > } 351 -- val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
352 -- 352 --
353 353
354 val< : {x y p : Ordinal} → odef (* x) ( & < * y , * p > ) → y o< x 354 val< : {x y p : Ordinal} → odef (* x) ( & < * y , * p > ) → y o< x
355 val< = ? 355 val< {x} {y} {p} xyp = osucprev ( begin
356 osuc y ≤⟨ osucc (odef< (subst (λ k → odef (* y , * y) k) &iso (v00 _ _ ) )) ⟩
357 & (* y , * y) <⟨ c<→o< (v01 _ _) ⟩
358 & < * y , * p > <⟨ odef< xyp ⟩
359 & (* x) ≡⟨ &iso ⟩
360 x ∎ ) where
361 v00 : (x y : HOD) → odef (x , y) (& x)
362 v00 _ _ = case1 refl
363 v01 : (x y : HOD) → < x , y > ∋ (x , x)
364 v01 _ _ = case1 refl
365 open o≤-Reasoning O
356 366
357 record valS (G : HOD) (x z : Ordinal) (val : (y : Ordinal) → y o< x → HOD): Set n where 367 record valS (G : HOD) (x z : Ordinal) (val : (y : Ordinal) → y o< x → HOD): Set n where
358 field 368 field
359 y p : Ordinal 369 y p : Ordinal
360 G∋p : odef G p 370 G∋p : odef G p
361 is-val : odef (* x) ( & < * y , * p > ) 371 is-val : odef (* x) ( & < * y , * p > )
362 x=valy : z ≡ & (val y (val< is-val)) 372 z=valy : z ≡ & (val y (val< is-val))
373 z<x : z o< x
363 374
364 val : (x : HOD) {P L M : HOD } {LP : L ⊆ Power P} 375 val : (x : HOD) {P L M : HOD } {LP : L ⊆ Power P}
365 → (G : GenericFilter {L} {P} LP M ) 376 → (G : GenericFilter {L} {P} LP M )
366 → HOD 377 → HOD
367 val x G = TransFinite {λ x → HOD } ind (& x) where 378 val x G = TransFinite {λ x → HOD } ind (& x) where
368 ind : (x : Ordinal) → ((y : Ordinal) → y o< x → HOD) → HOD 379 ind : (x : Ordinal) → ((y : Ordinal) → y o< x → HOD) → HOD
369 ind x valy = record { od = record { def = λ z → valS (⊆-Ideal.ideal (genf G)) x z valy } ; odmax = {!!} ; <odmax = {!!} } 380 ind x valy = record { od = record { def = λ z → valS (⊆-Ideal.ideal (genf G)) x z valy } ; odmax = x ; <odmax = v02 } where
370 381 v02 : {z : Ordinal} → valS (⊆-Ideal.ideal (genf G)) x z valy → z o< x
371 382 v02 {z} lt = valS.z<x lt
372 383
373 384
374 385
375 386
387
388