Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1390:64b243e501b2
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 26 Jun 2023 09:03:12 +0900 |
| parents | 242bba9c82bf |
| children | 250e52f15f43 |
| files | src/cardinal.agda |
| diffstat | 1 files changed, 23 insertions(+), 20 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cardinal.agda Mon Jun 26 07:10:12 2023 +0900 +++ b/src/cardinal.agda Mon Jun 26 09:03:12 2023 +0900 @@ -143,30 +143,33 @@ be02 = subst (λ k → odef k x) *iso lt fU : Injection (& UC) (& (Image {& UC} {b} (Injection-⊆ UC⊆a f) )) - fU = record { i→ = be03 ; iB = be10 ; inject = ? } where - be03 : (x : Ordinal) → odef (* (& UC)) x → Ordinal - be03 x ucx = be04 _ (CN.gfix be02) where - be02 : CN x - be02 = subst (λ k → odef k x) *iso ucx - be04 : (i : ℕ) → {x : Ordinal } → gfImage i x → Ordinal - be05 : (i : ℕ) → {x : Ordinal } → (gfi : gfImage i x) → odef (* a) (be04 i gfi ) - be04 0 {x} (a-g ax ¬ib) = x - be04 (suc i) {x} (next-gf lt _) = fba ( fab (be04 i lt) (be05 i lt) ) ( b∋fab _ (be05 i lt)) - be05 0 {x} (a-g ax ¬ib) = ax - be05 (suc i) {x} (next-gf lt _) = a∋fba ( fab (be04 i lt) (be05 i lt) ) ( b∋fab _ (be05 i lt)) - be10 : (x : Ordinal) (lt : odef (* (& UC)) x) → - odef (* (& (Image (Injection-⊆ UC⊆a (record { i→ = fab ; iB = b∋fab ; inject = fab-inject }))))) (be03 x lt) - be10 x lt = subst (λ k → odef k (be03 x lt)) (sym *iso) be11 where + fU = record { i→ = λ x lt → IsImage.y (be10 x lt) ; iB = λ x lt → be20 (IsImage.y (be10 x lt)) (be21 x lt) ; inject = ? } where + be10 : (x : Ordinal) (lt : odef (* (& UC)) x) → IsImage _ _ (Injection-⊆ UC⊆a f) x + be20 : (x : Ordinal) (lt : odef (* (& UC)) x) → odef (* (& (Image (Injection-⊆ UC⊆a f)))) x + be20 x lt = subst ( λ k → odef k x ) (sym *iso) (be10 x lt ) + be21 : (x : Ordinal) (lt : odef (* (& UC)) x) → odef (* (& UC)) (IsImage.y (be10 x lt)) + be21 = ? + g⁻¹ : { x : Ordinal} → odef (* b) x → Ordinal + g⁻¹ = ? + a∋g⁻¹ : { x : Ordinal} → (bx : odef (* b) x ) → odef (* a) (g⁻¹ bx ) + a∋g⁻¹ = ? + is-g⁻¹ : { x : Ordinal} → (bx : odef (* b) x ) → x ≡ fab (g⁻¹ bx ) (a∋g⁻¹ bx) + is-g⁻¹ = ? + be10 x lt = record { y = be14 _ (CN.gfix be02) ; ay = ? ; x=fy = ? } where be02 : CN x be02 = subst (λ k → odef k x) *iso lt be14 : (i : ℕ) → {x : Ordinal } → gfImage i x → Ordinal - be15 : (i : ℕ) → {x : Ordinal } → gfImage i x → ( IsImage _ _ ((Injection-⊆ UC⊆a f)) ? ) + be05 : (i : ℕ) → {x : Ordinal } → (gfi : gfImage i x) → odef (* a) (be14 i gfi ) be14 0 {x} (a-g ax ¬ib) = x - be14 (suc i) {x} (next-gf lt _) = fba ( fab (be14 i lt) ? ) ( b∋fab _ ?) - be15 0 {x} (a-g ax ¬ib) = ? - be15 (suc i) {x} (next-gf ix ix₁) = ? - be11 : IsImage _ _ ((Injection-⊆ UC⊆a f)) (be03 x lt) - be11 = be15 _ (CN.gfix be02) + be14 (suc i) {x} (next-gf lt _) = fba ( fab (be14 i lt) (be05 i lt) ) ( b∋fab _ (be05 i lt)) + be05 0 {x} (a-g ax ¬ib) = ax + be05 (suc i) {x} (next-gf lt _) = a∋fba ( fab (be14 i lt) (be05 i lt) ) ( b∋fab _ (be05 i lt)) + be16 : (i : ℕ) → {x : Ordinal } → (gfi : gfImage i x) → IsImage _ _ ((Injection-⊆ UC⊆a f)) (be14 i gfi) + be16 0 {x} (a-g ax ¬ib) = record { y = g⁻¹ (b∋fab x ax) + ; ay = subst (λ k → odef k ( g⁻¹ (b∋fab x ax))) (sym *iso) record { i = 0 ; gfix = a-g ? ? } ; x=fy = is-g⁻¹ ? } + be16 (suc i) {x} (next-gf ix ix₁) = record { y = ? ; ay = ? ; x=fy = ? } + be11 : IsImage _ _ ((Injection-⊆ UC⊆a f)) (be14 _ (CN.gfix be02)) + be11 = be16 _ (CN.gfix be02) gU : Injection (& (Image {& UC} {b} (Injection-⊆ UC⊆a f))) (& UC) gU = ?