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

comparison src/cardinal.agda @ 1390:64b243e501b2

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, 26 Jun 2023 09:03:12 +0900
parents 242bba9c82bf
children 250e52f15f43
comparison
equal deleted inserted replaced
1389:242bba9c82bf 1390:64b243e501b2
141 UC⊆a {x} lt = a∋gfImage (CN.i be02) (CN.gfix be02) where 141 UC⊆a {x} lt = a∋gfImage (CN.i be02) (CN.gfix be02) where
142 be02 : CN x 142 be02 : CN x
143 be02 = subst (λ k → odef k x) *iso lt 143 be02 = subst (λ k → odef k x) *iso lt
144 144
145 fU : Injection (& UC) (& (Image {& UC} {b} (Injection-⊆ UC⊆a f) )) 145 fU : Injection (& UC) (& (Image {& UC} {b} (Injection-⊆ UC⊆a f) ))
146 fU = record { i→ = be03 ; iB = be10 ; inject = ? } where 146 fU = record { i→ = λ x lt → IsImage.y (be10 x lt) ; iB = λ x lt → be20 (IsImage.y (be10 x lt)) (be21 x lt) ; inject = ? } where
147 be03 : (x : Ordinal) → odef (* (& UC)) x → Ordinal 147 be10 : (x : Ordinal) (lt : odef (* (& UC)) x) → IsImage _ _ (Injection-⊆ UC⊆a f) x
148 be03 x ucx = be04 _ (CN.gfix be02) where 148 be20 : (x : Ordinal) (lt : odef (* (& UC)) x) → odef (* (& (Image (Injection-⊆ UC⊆a f)))) x
149 be02 : CN x 149 be20 x lt = subst ( λ k → odef k x ) (sym *iso) (be10 x lt )
150 be02 = subst (λ k → odef k x) *iso ucx 150 be21 : (x : Ordinal) (lt : odef (* (& UC)) x) → odef (* (& UC)) (IsImage.y (be10 x lt))
151 be04 : (i : ℕ) → {x : Ordinal } → gfImage i x → Ordinal 151 be21 = ?
152 be05 : (i : ℕ) → {x : Ordinal } → (gfi : gfImage i x) → odef (* a) (be04 i gfi ) 152 g⁻¹ : { x : Ordinal} → odef (* b) x → Ordinal
153 be04 0 {x} (a-g ax ¬ib) = x 153 g⁻¹ = ?
154 be04 (suc i) {x} (next-gf lt _) = fba ( fab (be04 i lt) (be05 i lt) ) ( b∋fab _ (be05 i lt)) 154 a∋g⁻¹ : { x : Ordinal} → (bx : odef (* b) x ) → odef (* a) (g⁻¹ bx )
155 be05 0 {x} (a-g ax ¬ib) = ax 155 a∋g⁻¹ = ?
156 be05 (suc i) {x} (next-gf lt _) = a∋fba ( fab (be04 i lt) (be05 i lt) ) ( b∋fab _ (be05 i lt)) 156 is-g⁻¹ : { x : Ordinal} → (bx : odef (* b) x ) → x ≡ fab (g⁻¹ bx ) (a∋g⁻¹ bx)
157 be10 : (x : Ordinal) (lt : odef (* (& UC)) x) → 157 is-g⁻¹ = ?
158 odef (* (& (Image (Injection-⊆ UC⊆a (record { i→ = fab ; iB = b∋fab ; inject = fab-inject }))))) (be03 x lt) 158 be10 x lt = record { y = be14 _ (CN.gfix be02) ; ay = ? ; x=fy = ? } where
159 be10 x lt = subst (λ k → odef k (be03 x lt)) (sym *iso) be11 where
160 be02 : CN x 159 be02 : CN x
161 be02 = subst (λ k → odef k x) *iso lt 160 be02 = subst (λ k → odef k x) *iso lt
162 be14 : (i : ℕ) → {x : Ordinal } → gfImage i x → Ordinal 161 be14 : (i : ℕ) → {x : Ordinal } → gfImage i x → Ordinal
163 be15 : (i : ℕ) → {x : Ordinal } → gfImage i x → ( IsImage _ _ ((Injection-⊆ UC⊆a f)) ? ) 162 be05 : (i : ℕ) → {x : Ordinal } → (gfi : gfImage i x) → odef (* a) (be14 i gfi )
164 be14 0 {x} (a-g ax ¬ib) = x 163 be14 0 {x} (a-g ax ¬ib) = x
165 be14 (suc i) {x} (next-gf lt _) = fba ( fab (be14 i lt) ? ) ( b∋fab _ ?) 164 be14 (suc i) {x} (next-gf lt _) = fba ( fab (be14 i lt) (be05 i lt) ) ( b∋fab _ (be05 i lt))
166 be15 0 {x} (a-g ax ¬ib) = ? 165 be05 0 {x} (a-g ax ¬ib) = ax
167 be15 (suc i) {x} (next-gf ix ix₁) = ? 166 be05 (suc i) {x} (next-gf lt _) = a∋fba ( fab (be14 i lt) (be05 i lt) ) ( b∋fab _ (be05 i lt))
168 be11 : IsImage _ _ ((Injection-⊆ UC⊆a f)) (be03 x lt) 167 be16 : (i : ℕ) → {x : Ordinal } → (gfi : gfImage i x) → IsImage _ _ ((Injection-⊆ UC⊆a f)) (be14 i gfi)
169 be11 = be15 _ (CN.gfix be02) 168 be16 0 {x} (a-g ax ¬ib) = record { y = g⁻¹ (b∋fab x ax)
169 ; ay = subst (λ k → odef k ( g⁻¹ (b∋fab x ax))) (sym *iso) record { i = 0 ; gfix = a-g ? ? } ; x=fy = is-g⁻¹ ? }
170 be16 (suc i) {x} (next-gf ix ix₁) = record { y = ? ; ay = ? ; x=fy = ? }
171 be11 : IsImage _ _ ((Injection-⊆ UC⊆a f)) (be14 _ (CN.gfix be02))
172 be11 = be16 _ (CN.gfix be02)
170 173
171 gU : Injection (& (Image {& UC} {b} (Injection-⊆ UC⊆a f))) (& UC) 174 gU : Injection (& (Image {& UC} {b} (Injection-⊆ UC⊆a f))) (& UC)
172 gU = ? 175 gU = ?
173 176
174 -- Injection (b - a) b 177 -- Injection (b - a) b