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

comparison cardinal.agda @ 376:6c72bee25653

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, 20 Jul 2020 16:28:12 +0900
parents 12071f79f3cf
children 853ead1b56b8
comparison
equal deleted inserted replaced
375:8cade5f660bd 376:6c72bee25653
32 ∋-p : (A x : HOD ) → Dec ( A ∋ x ) 32 ∋-p : (A x : HOD ) → Dec ( A ∋ x )
33 ∋-p A x with ODC.p∨¬p O ( A ∋ x ) 33 ∋-p A x with ODC.p∨¬p O ( A ∋ x )
34 ∋-p A x | case1 t = yes t 34 ∋-p A x | case1 t = yes t
35 ∋-p A x | case2 t = no t 35 ∋-p A x | case2 t = no t
36 36
37 _⊗_ : (A B : HOD) → HOD 37 --_⊗_ : (A B : HOD) → HOD
38 A ⊗ B = record { od = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } } where 38 --A ⊗ B = record { od = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } } where
39 checkAB : { p : Ordinal } → def ZFProduct p → Set n 39 -- checkAB : { p : Ordinal } → def ZFProduct p → Set n
40 checkAB (pair x y) = odef A x ∧ odef B y 40 -- checkAB (pair x y) = odef A x ∧ odef B y
41 41
42 func→od0 : (f : Ordinal → Ordinal ) → HOD 42 func→od0 : (f : Ordinal → Ordinal ) → HOD
43 func→od0 f = record { od = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkfunc p ) }} where 43 func→od0 f = record { od = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkfunc p ) }} where
44 checkfunc : { p : Ordinal } → def ZFProduct p → Set n 44 checkfunc : { p : Ordinal } → def ZFProduct p → Set n
45 checkfunc (pair x y) = f x ≡ y 45 checkfunc (pair x y) = f x ≡ y
62 od→func : { dom cod : HOD } → {f : Ordinal } → odef (Func dom cod ) f → Func←cd {dom} {cod} {f} 62 od→func : { dom cod : HOD } → {f : Ordinal } → odef (Func dom cod ) f → Func←cd {dom} {cod} {f}
63 od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o {!!} ( λ y lt → lemma x {!!} ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where 63 od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o {!!} ( λ y lt → lemma x {!!} ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where
64 lemma : Ordinal → Ordinal → Ordinal 64 lemma : Ordinal → Ordinal → Ordinal
65 lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → odef (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y) 65 lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → odef (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y)
66 lemma x y | p | no n = o∅ 66 lemma x y | p | no n = o∅
67 lemma x y | p | yes f∋y = lemma2 (proj1 (ODC.double-neg-eilm O ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) 67 lemma x y | p | yes f∋y = lemma2 ? where -- (ODC.double-neg-eilm O ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y)
68 lemma2 : {p : Ordinal} → ord-pair p → Ordinal 68 lemma2 : {p : Ordinal} → ord-pair p → Ordinal
69 lemma2 (pair x1 y1) with ODC.decp O ( x1 ≡ x) 69 lemma2 (pair x1 y1) with ODC.decp O ( x1 ≡ x)
70 lemma2 (pair x1 y1) | yes p = y1 70 lemma2 (pair x1 y1) | yes p = y1
71 lemma2 (pair x1 y1) | no ¬p = o∅ 71 lemma2 (pair x1 y1) | no ¬p = o∅
72 fod : HOD 72 fod : HOD