# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687825255 -32400
# Node ID 873924d06ff7c385ef73c7ac9063bc4f12dc8b19
# Parent  c67ecdf89e778b77a7881ddb006c0e30d489832f
...

diff -r c67ecdf89e77 -r 873924d06ff7 src/cardinal.agda
--- a/src/cardinal.agda	Tue Jun 27 08:48:41 2023 +0900
+++ b/src/cardinal.agda	Tue Jun 27 09:20:55 2023 +0900
@@ -170,12 +170,25 @@
           b-UC⊆b : * (& b-UC) ⊆ * b
           b-UC⊆b {x} lt = proj1 ( subst (λ k → odef k x) *iso lt )
 
+          open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
+
+          fab-refl : {x : Ordinal } → {ax ax1 : odef (* a) x}  → fab x ax ≡ fab x ax1
+          fab-refl {x} {ax} {ax1} = cong (λ k → fab x k) ( HE.≅-to-≡ ( ∋-irr {* a} ax ax1 ))  
+
+          fba-refl : {x : Ordinal } → {bx bx1 : odef (* b) x}  → fba x bx ≡ fba x bx1
+          fba-refl {x} {bx} {bx1} = cong (λ k → fba x k) ( HE.≅-to-≡ ( ∋-irr {* b} bx bx1 ))  
+
           be10 : Injection (& b-UC) (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g) ))
-          be10 = record { i→ = be12 ; iB = ? ; inject = ? } where
+          be10 = record { i→ = be12 ; iB = be13 ; inject = ? } where
               be12 : (x : Ordinal) → odef (* (& b-UC)) x → Ordinal
               be12 x lt = i→ g x (proj1 be02) where
                     be02 : odef (* b) x ∧ ( ¬ CN x )
                     be02 = subst (λ k → odef k x) *iso lt
+              be13 : (x : Ordinal) (lt : odef (* (& b-UC)) x) → odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) (be12 x lt)
+              be13 x lt = subst (λ k → odef k (be12 x lt)) (sym *iso) record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fba-refl } where
+                    be02 : odef (* b) x ∧ ( ¬ CN x )
+                    be02 = subst (λ k → odef k x) *iso lt
+
 
           be11 : Injection (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g) )) (& b-UC)
           be11 = record { i→ = be13 ; iB = ? ; inject = ? } where
@@ -185,11 +198,6 @@
                     be02 : odef (* b) y ∧ ( ¬ CN y )
                     be02 = subst (λ k → odef k y) *iso ay
 
-          open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
-
-          fab-refl : {x : Ordinal } → {ax ax1 : odef (* a) x}  → fab x ax ≡ fab x ax1
-          fab-refl {x} {ax} {ax1} = cong (λ k → fab x k) ( HE.≅-to-≡ ( ∋-irr {* a} ax ax1 ))  
-
           fUC = & (Image (& UC) {b} (Injection-⊆ UC⊆a  f) )
           --   C n → f (C n) 
           fU : Injection (& UC) (& (Image (& UC) {b} (Injection-⊆ UC⊆a  f) ))