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

comparison src/ODUtil.agda @ 1286:619e68271cf8

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, 22 May 2023 19:06:25 +0900
parents 302cfb533201
children
comparison
equal deleted inserted replaced
1285:302cfb533201 1286:619e68271cf8
73 pair-xx<xy {x} {y} = ⊆→o≤ lemma where 73 pair-xx<xy {x} {y} = ⊆→o≤ lemma where
74 lemma : {z : Ordinal} → def (od (x , x)) z → def (od (x , y)) z 74 lemma : {z : Ordinal} → def (od (x , x)) z → def (od (x , y)) z
75 lemma {z} (case1 refl) = case1 refl 75 lemma {z} (case1 refl) = case1 refl
76 lemma {z} (case2 refl) = case1 refl 76 lemma {z} (case2 refl) = case1 refl
77 77
78 pair-<xy : {x y : HOD} → {n : Ordinal} → & x o< next n → & y o< next n → & (x , y) o< next n 78 -- pair-<xy : {x y : HOD} → {z : Ordinal} → & x o< next z → & y o< next z → & (x , y) o< next z
79 pair-<xy {x} {y} {o} x<nn y<nn with trio< (& x) (& y) | inspect (omax (& x)) (& y) 79 -- pair-<xy {x} {y} {z} x<nn y<nn with trio< (& x) (& y) | inspect (omax (& x)) (& y)
80 ... | tri< a ¬b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx y<nn)) ho< 80 -- ... | tri< a ¬b ¬c | record { eq = eq1 } = ? where
81 ... | tri> ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho< 81 -- ll1 : omax (& x) (& y) o< next z
82 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho< 82 -- ll1 = subst (λ k → k o< next z ) (sym eq1) (osuc<nx y<nn)
83 -- ll2 : & (x , y) o< next (omax (& x) (& y))
84 -- ll2 = ho<
85 -- ... | tri> ¬a ¬b c | record { eq = eq1 } = ? -- next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho<
86 -- ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ? -- next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho<
83 87
84 -- another form of infinite 88 -- another form of infinite
85 -- pair-ord< : {x : Ordinal } → Set n 89 -- pair-ord< : {x : Ordinal } → Set n
86 pair-ord< : {x : HOD } → ( {y : HOD } → & y o< next (odmax y) ) → & ( x , x ) o< next (& x) 90 pair-ord< : {x : HOD } → ( {y : HOD } → & y o< next (odmax y) ) → & ( x , x ) o< next (& x)
87 pair-ord< {x} ho< = subst (λ k → & (x , x) o< k ) lemmab0 lemmab1 where 91 pair-ord< {x} ho< = subst (λ k → & (x , x) o< k ) lemmab0 lemmab1 where
113 subset-lemma {A} {x} = record { 117 subset-lemma {A} {x} = record {
114 proj1 = λ lt x∋z → subst (λ k → odef A k ) &iso ( proj1 (lt (subst (λ k → odef x k) (sym &iso) x∋z ) )) 118 proj1 = λ lt x∋z → subst (λ k → odef A k ) &iso ( proj1 (lt (subst (λ k → odef x k) (sym &iso) x∋z ) ))
115 ; proj2 = λ x⊆A lt → ⟪ x⊆A lt , lt ⟫ 119 ; proj2 = λ x⊆A lt → ⟪ x⊆A lt , lt ⟫
116 } 120 }
117 121
118 ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅ 122 ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< infinite-odmax
119 ω<next-o∅ {y} lt = <odmax infinite lt 123 ω<next-o∅ {y} lt = <odmax infinite lt
120 124
121 nat→ω : Nat → HOD 125 nat→ω : Nat → HOD
122 nat→ω Zero = od∅ 126 nat→ω Zero = od∅
123 nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) 127 nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y))