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

comparison cardinal.agda @ 421:cb067605fea0

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 Fri, 31 Jul 2020 17:54:52 +0900
parents 53422a8ea836
children 44a484f17f26
comparison
equal deleted inserted replaced
420:53422a8ea836 421:cb067605fea0
46 46
47 FuncP∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x ) 47 FuncP∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x )
48 → odef (FuncP A B) (od→ord (Replace A (λ x → < x , f x > ))) 48 → odef (FuncP A B) (od→ord (Replace A (λ x → < x , f x > )))
49 FuncP∋f = {!!} 49 FuncP∋f = {!!}
50 50
51 Func→f : {A B f x : HOD} → def Func (od→ord f) → (x : HOD ) → A ∋ x → ( HOD ∧ ((y : HOD ) → B ∋ y )) 51 -- Func→f : {A B f x : HOD} → def Func (od→ord f) → (x : HOD ) → A ∋ x → ( HOD ∧ ((y : HOD ) → B ∋ y ))
52 Func→f = {!!} 52 -- Func→f = {!!}
53 53 -- Func₁ : {A B f : HOD} → def Func (od→ord f) → {!!}
54 Func₁ : {A B f : HOD} → def Func (od→ord f) → {!!} 54 -- Func₁ = {!!}
55 Func₁ = {!!} 55 -- Cod : {A B f : HOD} → def Func (od→ord f) → {!!}
56 56 -- Cod = {!!}
57 Cod : {A B f : HOD} → def Func (od→ord f) → {!!} 57 -- 1-1 : {A B f : HOD} → def Func (od→ord f) → {!!}
58 Cod = {!!} 58 -- 1-1 = {!!}
59 59 -- onto : {A B f : HOD} → def Func (od→ord f) → {!!}
60 1-1 : {A B f : HOD} → def Func (od→ord f) → {!!} 60 -- onto = {!!}
61 1-1 = {!!}
62
63 onto : {A B f : HOD} → def Func (od→ord f) → {!!}
64 onto = {!!}
65 61
66 record Bijection (A B : Ordinal ) : Set n where 62 record Bijection (A B : Ordinal ) : Set n where
67 field 63 field
68 fun→ : Ordinal → Ordinal 64 fun→ : Ordinal → Ordinal
69 fun← : Ordinal → Ordinal 65 fun← : Ordinal → Ordinal
70 fun→inA : (x : Ordinal) → odef (ord→od A) ( fun→ x ) 66 fun→inA : (x : Ordinal) → odef (ord→od A) ( fun→ x )
71 fun←inB : (x : Ordinal) → odef (ord→od B) ( fun← x ) 67 fun←inB : (x : Ordinal) → odef (ord→od B) ( fun← x )
72 fiso→ : (x : Ordinal ) → odef (ord→od A) x → fun→ ( fun← x ) ≡ x 68 fiso→ : (x : Ordinal ) → odef (ord→od B) x → fun→ ( fun← x ) ≡ x
73 fiso← : (x : Ordinal ) → odef (ord→od B) x → fun← ( fun→ x ) ≡ x 69 fiso← : (x : Ordinal ) → odef (ord→od A) x → fun← ( fun→ x ) ≡ x
74 70
75 Card : OD 71 Card : OD
76 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x } 72 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x }