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

changeset 1408:2fe6908fb48e

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, 30 Jun 2023 06:11:05 +0900
parents 523bd51605cb
children 1e2c77c1227d
files src/cardinal.agda
diffstat 1 files changed, 8 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Thu Jun 29 18:56:57 2023 +0900
+++ b/src/cardinal.agda	Fri Jun 30 06:11:05 2023 +0900
@@ -194,7 +194,7 @@
       ... | case2 ¬ism = ⊥-elim ( nc0 ( a-g ax ¬ism ) )
 
       be10 : Injection (& a-UC) (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )) )
-      be10 = record { i→ = λ x lt → g⁻¹ (be15 lt) (be16 lt) ; iB = be17 ; inject = ? } where
+      be10 = record { i→ = λ x lt → g⁻¹ (be15 lt) (be16 lt) ; iB = be17 ; inject = be18 } where
           be15 : {x : Ordinal } → odef (* (& a-UC)) x → odef (* a) x
           be15 {x} lt with subst (λ k → odef k x) *iso lt
           ... | ⟪ ax , ncn ⟫ = ax
@@ -202,7 +202,13 @@
           be16 {x} lt nc0 with subst (λ k → odef k x) *iso lt
           ... | ⟪ ax , ncn ⟫ = ⊥-elim ( ncn record { i = 0 ; gfix = nc0 } )
           be17 : (x : Ordinal) (lt : odef (* (& a-UC)) x) → odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) (g⁻¹ (be15 lt) (be16 lt))
-          be17 = ?
+          be17 x lt with subst (λ k → odef k x) *iso lt
+          ... | ⟪ ax , ncn ⟫ = subst₂ ( λ j k → odef j k ) (sym *iso)  ? ⟪ b∋g⁻¹ (be15 lt) (be16 lt), ? ⟫
+              be18 : ¬ odef (* (& (Image (& UC) (Injection-⊆ (λ {x} lt → a∋gfImage (CN.i (subst (λ k → odef k x) *iso lt)) (CN.gfix (subst (λ k → odef k x) *iso lt))) f)))) (g⁻¹ (be15 lt) (be16 lt))
+              be18 = ?
+
+          be18 : (x y : Ordinal) (ltx : odef (* (& a-UC)) x) (lty : odef (* (& a-UC)) y) → g⁻¹ (be15 ltx) (be16 ltx) ≡ g⁻¹ (be15 lty) (be16 lty) → x ≡ y
+          be18 = ?
 
       be11 : Injection  (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) ))) (& a-UC)
       be11 = record { i→ = be13 ; iB = be14 ; inject = ? } where