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

comparison OD.agda @ 397:382a4a411aff

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 27 Jul 2020 16:20:14 +0900
parents 8c092c042093
children fbe1a49876ad
comparison
equal deleted inserted replaced
396:8c092c042093 397:382a4a411aff
263 lemma (case2 refl) = y∋x 263 lemma (case2 refl) = y∋x
264 264
265 -- another possible restriction. We reqest no minimality on odmax, so it may arbitrary larger. 265 -- another possible restriction. We reqest no minimality on odmax, so it may arbitrary larger.
266 odmax<od→ord : { x y : HOD } → x ∋ y → Set n 266 odmax<od→ord : { x y : HOD } → x ∋ y → Set n
267 odmax<od→ord {x} {y} x∋y = odmax x o< od→ord x 267 odmax<od→ord {x} {y} x∋y = odmax x o< od→ord x
268
269 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
270 268
271 in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → OD 269 in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → OD
272 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } 270 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) }
273 271
274 _∩_ : ( A B : HOD ) → HOD 272 _∩_ : ( A B : HOD ) → HOD
453 451
454 _=h=_ : (x y : HOD) → Set n 452 _=h=_ : (x y : HOD) → Set n
455 x =h= y = od x == od y 453 x =h= y = od x == od y
456 454
457 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 455 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
458 456 postulate f-extensionality : { n m : Level} → HE.Extensionality n m
459 ord∋eq : {n : Level } {A i : HOD } → { f : (x : HOD ) → A ∋ x → Set n} 457
458
459 ord∋eq : {A i : HOD } → { f : (x : HOD ) → A ∋ x → Set (suc n)}
460 → ( ( x : Ordinal ) → ( lx : odef A x ) → f (ord→od x) (d→∋ A lx) ) 460 → ( ( x : Ordinal ) → ( lx : odef A x ) → f (ord→od x) (d→∋ A lx) )
461 → ( lt : A ∋ i ) → f i lt 461 → ( lt : A ∋ i ) → f i lt
462 ord∋eq {n} {A} {i} {f} of lt = subst (λ k → odef A k ) ? (of (od→ord i) ?) 462 ord∋eq {A} {i} {f} of lt with of (od→ord i) lt
463 ... | t = HE.subst₂ (λ j k → f j (k j)) (HE.≡-to-≅ oiso) (f-extensionality (λ _ → refl ) lemma ) t where
464 lemma : (i : HOD) → ? ≅ ?
465 lemma = {!!}
463 466
464 nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i 467 nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
465 nat→ω-iso {i} lt = ord∋eq {_} {infinite} {i} (λ x lx → lemma lx ) lt where 468 nat→ω-iso {i} lt = ord∋eq {infinite} {i} (λ x lx → lemma lx ) lt where
466 lemma : {x : Ordinal} → (lx : infinite-d x ) → nat→ω ( ω→nat (ord→od x) (d→∋ infinite lx) ) ≡ ord→od x 469 lemma : {x : Ordinal} → (lx : infinite-d x ) → nat→ω ( ω→nat (ord→od x) (d→∋ infinite lx) ) ≡ ord→od x
467 lemma = {!!} 470 lemma = {!!}
468 471
469 infixr 200 _∈_ 472 infixr 200 _∈_
470 -- infixr 230 _∩_ _∪_ 473 -- infixr 230 _∩_ _∪_