# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1669194203 -32400
# Node ID 8025c5d01153ca3c182171515281e90a9a4dc5ac
# Parent  2362c2d89d3623edebdb4c1ca773309f770a3090
...

diff -r 2362c2d89d36 -r 8025c5d01153 src/zorn.agda
--- a/src/zorn.agda	Wed Nov 23 16:12:51 2022 +0900
+++ b/src/zorn.agda	Wed Nov 23 18:03:23 2022 +0900
@@ -475,6 +475,12 @@
    ... | tri≈ ¬a b ¬c = o≤-refl0 b
    ... | tri> ¬a ¬b c = ⊥-elim (<-irr (case2 sx<sy ) (supf-< c) )
 
+   supf-<inject : {x y : Ordinal } → supf x << supf  y → supf x o< supf y
+   supf-<inject {x} {y} sx<sy with trio< (supf x) (supf y)
+   ... | tri< a ¬b ¬c = a
+   ... | tri≈ ¬a b ¬c = ⊥-elim (<-irr (case1 (cong (*) (sym b)) ) sx<sy )
+   ... | tri> ¬a ¬b c = ⊥-elim (<-irr (case2 sx<sy ) (supf-< c) )
+
    supf-inject : {x y : Ordinal } → supf x o< supf y → x o<  y
    supf-inject {x} {y} sx<sy with trio< x y
    ... | tri< a ¬b ¬c = a
@@ -531,14 +537,29 @@
        z52 : supf (supf b) ≡ supf b
        z52 = sup=u asupf sfb≤x ⟪ record { x≤sup = z54  } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ 
 
-   fc-inject :    ( {a : Ordinal } → odef A a → a << f a )
-      →  {x y wx wy  : Ordinal} →  FClosure A f (supf x) wx  →  FClosure A f (supf y) wy → wx ≡ wy → supf x ≡ supf y
-   fc-inject mf< (init xa eqa) (init ya eqb) refl = trans eqa (sym eqb)
-   fc-inject mf< {x} (init xa eqx) (fsuc ya fcy) eq = ⊥-elim ( supf-¬hp ? mf< record { ax = asupf ; y = ya ; ay = ? ; x=fy = trans eqx eq } ) where
+   fc-inject : {x y : Ordinal }  →  (mf< : <-monotonic-f A f) → x o≤ z → y o≤ z → supf x o< z → supf y o< z
+      →  { wx wy  : Ordinal} →  FClosure A f (supf x) wx  →  FClosure A f (supf y) wy → wx ≡ wy → supf x ≡ supf y
+   fc-inject mf< x≤z y≤z sx<z sy<z (init xa eqa) (init ya eqb) refl = trans eqa (sym eqb)
+   fc-inject {x} {y} mf< x≤z y≤z sx<z sy<z (init xa eqx) (fsuc ya fcy) eq = 
+     ⊥-elim ( supf-¬hp x≤z (λ xa → proj1 (mf< _ xa)) record { ax = asupf ; y = ya ; ay = z53 ; x=fy = trans eqx eq } ) where
+        sy<sx : supf y << supf x
+        sy<sx =  ftrans<=-<  (≤to<= (s≤fc (supf y) f mf fcy)) (subst₂ (λ j k → j << k ) refl (trans (sym eq) (sym eqx)) 
+            (proj1 ( mf< _ (A∋fc (supf y) f mf fcy) )))
         z53 : odef (UnionCF A f mf ay supf x) ya
-        z53 = cfcs ? ? ? ? fcy
-   fc-inject mf< (fsuc xa fcx) (init ya eqy) eq = ?
-   fc-inject mf< (fsuc xa fcx) (fsuc ya fcy) eq = fc-inject mf< fcx fcy ? 
+        z53 = cfcs mf< (supf-inject (supf-<inject sy<sx)) x≤z sy<z fcy
+   fc-inject {x} {y} mf< x≤z y≤z sx<z sy<z (fsuc xa fcx) (init ya eqy) eq = 
+     ⊥-elim ( supf-¬hp y≤z (λ xa → proj1 (mf< _ xa)) record { ax = asupf ; y = xa ; ay = z53 ; x=fy = trans eqy (sym eq) } ) where
+        sx<sy : supf x << supf y
+        sx<sy =  ftrans<=-<  (≤to<= (s≤fc (supf x) f mf fcx)) (subst₂ (λ j k → j << k ) refl (trans eq (sym eqy)) 
+            (proj1 ( mf< _ (A∋fc (supf x) f mf fcx) )))
+        z53 : odef (UnionCF A f mf ay supf y) xa
+        z53 = cfcs mf< (supf-inject (supf-<inject sx<sy))  y≤z sx<z fcx
+   fc-inject mf< x≤z y≤z sx<z sy<z (fsuc xa fcx) (fsuc ya fcy) eq = fc-inject mf< x≤z y≤z sx<z sy<z  fcx fcy (z54 eq)  where
+        z54 : f xa ≡ f ya  → xa ≡ ya
+        z54 fa=fb with trio< xa ya
+        ... | tri< a ¬b ¬c = ?
+        ... | tri≈ ¬a b ¬c = b
+        ... | tri> ¬a ¬b c = ?
 
 supf-unique :  ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f)
         {y xa xb : Ordinal} → (ay : odef A y) →  (xa o≤ xb ) → (za : ZChain A f mf ay xa ) (zb : ZChain A f mf ay xb )