# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1649811241 -32400
# Node ID dfcb98151273d917d2eaeacfaf81e4fe19fef859
# Parent  5fcd2863317d00af4e1ee621ee97cba578d4d371
2 cases in 3 cases

diff -r 5fcd2863317d -r dfcb98151273 src/zorn.agda
--- a/src/zorn.agda	Wed Apr 13 08:16:16 2022 +0900
+++ b/src/zorn.agda	Wed Apr 13 09:54:01 2022 +0900
@@ -91,6 +91,8 @@
 A∋x-irr : (A : HOD) {x y : HOD} → x ≡ y → (A ∋ x) ≡ (A ∋ y )
 A∋x-irr A {x} {y} refl = refl
 
+me-elm-refl : (A : HOD) → (x : Element A) → elm (me {A} (d→∋ A (is-elm x))) ≡ elm x
+me-elm-refl A record { elm = ex ; is-elm = ax } = *iso 
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
@@ -121,12 +123,29 @@
     ifirst : {ox : Ordinal} → odef A ox → IChain A ox
     inext  : {ox oy : Ordinal} → odef A oy → * ox < * oy → IChain A ox → IChain A oy
 
-ic-connet :  {A : HOD} {x : Ordinal} → (x : IChain A x) → Ordinal →  Set n
-ic-connet {A} (ifirst {ox} ax) oy = ox ≡ oy
-ic-connet {A} (inext {ox} {oy} ay x<y iy) oz = (ox ≡ oz) ∨ ic-connet iy oz
+--   * ox < .. < * oy
+ic-connect :  {A : HOD} {oy : Ordinal} → (ox : Ordinal) →  (iy : IChain A oy) → Set n 
+ic-connect {A} ox (ifirst {oy} ay) = Lift n ⊥
+ic-connect {A} ox (inext {oy} {oz} ay y<z iz) = (ox ≡ oy) ∨ ic-connect ox iz 
+
+ic→odef : {A : HOD} {ox : Ordinal} → IChain A ox → odef A ox
+ic→odef {A} {ox} (ifirst ax) = ax
+ic→odef {A} {ox} (inext ax x<y ic) = ax
+
+ic→< :  {A : HOD} → (IsPartialOrderSet A) → (x : Ordinal) → odef A x → {y : Ordinal} → (iy : IChain A y) → ic-connect {A} {y} x iy → * x < * y
+ic→< {A} PO x ax {y} (ifirst ay) ()
+ic→< {A} PO x ax {y} (inext ay x<y iy) (case1 refl) = x<y
+ic→< {A} PO x ax {y} (inext {oy} ay x<y iy) (case2 ic) = IsStrictPartialOrder.trans PO 
+     {me (subst (λ k → odef A k) (sym &iso) ax )} {me (subst (λ k → odef A k) (sym &iso) (ic→odef {A} {oy} iy) ) }  {me (subst (λ k → odef A k) (sym &iso) ay) }
+    (ic→< {A} PO x ax iy ic ) x<y
+
+record IChained (A : HOD) (x y : Ordinal) : Set n where
+   field
+      iy : IChain A y
+      ic : ic-connect x iy 
 
 IChainSet : {A : HOD} → Element A → HOD
-IChainSet {A} ax = record { od = record { def = λ y → odef A y ∧ ( (iy : IChain A y ) → ic-connet iy (& (elm ax)))  }
+IChainSet {A} ax = record { od = record { def = λ y → odef A y ∧ IChained A (& (elm ax)) y }
     ; odmax = & A ; <odmax = λ {y} lt → subst (λ k → k o< & A) &iso (c<→o< (subst (λ k → odef A k) (sym &iso) (proj1 lt))) } 
 
 -- there is a y, & y > & x
@@ -188,11 +207,7 @@
         zc3 :  odef ( IChainSet x ) (& y) ∧  ( & (elm x) o< (& y ))
         zc3  = ODC.x∋minimal O Gtx  (λ eq → not (=od∅→≡o∅ eq))
         zc4 : odef (IChainSet (me (subst (OD.def (od A)) (sym &iso) (is-elm x)))) (& y)
-        zc4 = ⟪ proj1 (proj1 zc3) , (λ ic → zc6 (* (& (elm x))) (sym *iso) ic) ⟫ where 
-          zc5 : odef (IChainSet (me (is-elm x))) (& y)
-          zc5 = proj1 zc3
-          zc6 : (ax : HOD) → elm x ≡ ax → (iy : IChain A (& y)) →  ic-connet iy  (& ax)
-          zc6 ax refl iy = proj2 (proj1 zc3) iy
+        zc4 = ⟪ proj1 (proj1 zc3) , subst (λ k → IChained A (& k) (& y) ) (sym *iso) (proj2 (proj1 zc3)) ⟫ 
     ... | yes nogt with is-o∅ (& HG)
     ... | no  finite-chain = case2 (case1 record { maximal = y ; A∋maximal = proj1 zc3 ; ¬maximal<x = zc4 } ) where
         y : HOD
@@ -202,9 +217,14 @@
         zc5 : odef (IChainSet {A} (me (d→∋ A (is-elm x) ))) (& y)
         zc5 = IsFC.icy (proj2 zc3)
         zc4 : {z : HOD} → A ∋ z → ¬ (y < z)
-        zc4 {z} az y<z = IsFC.c-finite (proj2 zc3) record { y = & z ; A∋y =  az ; y>x = {!!} } where
+        zc4 {z} az y<z = IsFC.c-finite (proj2 zc3) record { y = & z ; A∋y =  az ; y>x = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) zc6 } where
+            zc8 : ic-connect (& (* (& (elm x)))) (IChained.iy (proj2 zc5)) 
+            zc8 = IChained.ic (proj2 zc5)
+            zc7 : elm x < y
+            zc7 = subst₂ (λ j k → j < k ) *iso *iso ( ic→< {A} PO (& (elm x)) (is-elm x) (IChained.iy (proj2 zc5))
+                (subst (λ k → ic-connect (& k) (IChained.iy (proj2 zc5)) ) (me-elm-refl A x) (IChained.ic (proj2 zc5)) )  )
             zc6 : elm x < z
-            zc6 = {!!}
+            zc6 = IsStrictPartialOrder.trans PO {x} {me (proj1 zc3)} {me az} zc7 y<z
     ... | yes  nohg = case2 (case2 {!!} )