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

comparison src/cardinal.agda @ 1174:375615f9d60f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Func and Funcs
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 18 Feb 2023 11:51:22 +0900
parents d122d0c1b094
children 7d2bae0ff36b
comparison
equal deleted inserted replaced
1173:4b2f49a5a1d5 1174:375615f9d60f
43 open HOD 43 open HOD
44 44
45 -- _⊗_ : (A B : HOD) → HOD 45 -- _⊗_ : (A B : HOD) → HOD
46 -- A ⊗ B = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) )) 46 -- A ⊗ B = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
47 47
48 Func : OD 48 record Func (A B : HOD) : Set n where
49 Func = record { def = λ x → def ZFPair x 49 field
50 ∧ ( (a b c : Ordinal) → odef (* x) (& < * a , * b >) ∧ odef (* x) (& < * a , * c >) → b ≡ c ) } 50 func : Ordinal → Ordinal
51 is-func : {x : Ordinal } → odef A x → odef B (func x)
51 52
52 FuncP : ( A B : HOD ) → HOD 53 data FuncHOD (A B : HOD) : (x : Ordinal) → Set n where
53 FuncP A B = record { od = record { def = λ x → odef (ZFP A B) x 54 felm : (F : Func A B) → FuncHOD A B (& ( Replace A ( λ x → < x , (* (Func.func F (& x))) > )))
54 ∧ ( (x : Ordinal ) (p q : odef (ZFP A B ) x ) → pi1 ? ≡ pi1 ? → pi2 ? ≡ pi2 ? ) } 55
55 ; odmax = odmax (ZFP A B) ; <odmax = λ lt → <odmax (ZFP A B) (proj1 lt) } 56 FuncHOD→F : {A B : HOD} {x : Ordinal} → FuncHOD A B x → Func A B
57 FuncHOD→F {A} {B} (felm F) = F
58
59 FuncHOD=R : {A B : HOD} {x : Ordinal} → (fc : FuncHOD A B x) → (* x) ≡ Replace A ( λ x → < x , (* (Func.func (FuncHOD→F fc) (& x))) > )
60 FuncHOD=R {A} {B} (felm F) = *iso
61
62 Funcs : (A B : HOD) → HOD
63 Funcs A B = record { od = record { def = λ x → FuncHOD A B x } ; odmax = osuc (& (A ⊗ B))
64 ; <odmax = λ {y} px → subst ( λ k → k o≤ (& (A ⊗ B)) ) &iso (⊆→o≤ (lemma1 px)) } where
65 lemma1 : {y : Ordinal } → FuncHOD A B y → {x : Ordinal} → odef (* y) x → odef (A ⊗ B) x
66 lemma1 {y} (felm F) {x} yx with subst (λ k → odef k x) *iso yx
67 ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (A ⊗ B) k ) (sym x=ψz) (
68 product→ (subst (λ k → odef A k) (sym &iso) az) (subst (λ k → odef B k)
69 (trans (cong (Func.func F) (sym &iso)) (sym &iso)) (Func.is-func F az) ))
56 70
57 record Injection (A B : Ordinal ) : Set n where 71 record Injection (A B : Ordinal ) : Set n where
58 field 72 field
59 i→ : (x : Ordinal ) → odef (* A) x → Ordinal 73 i→ : (x : Ordinal ) → odef (* A) x → Ordinal
60 iB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( i→ x lt ) 74 iB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( i→ x lt )