# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688073065 -32400
# Node ID 2fe6908fb48e3755e437170ddef7061d96d550a4
# Parent  523bd51605cbfa08b7a3eb7608034eab5915da3c
...

diff -r 523bd51605cb -r 2fe6908fb48e src/cardinal.agda
--- 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