# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1651283303 -32400
# Node ID e0cd3ac0087d16d3fbb56f38ad406d3af19c0eae
# Parent  d09f9a1d6c2f93c4441423df5fefd7dbbc9e2c9b
...

diff -r d09f9a1d6c2f -r e0cd3ac0087d src/zorn.agda
--- a/src/zorn.agda	Sat Apr 30 05:11:53 2022 +0900
+++ b/src/zorn.agda	Sat Apr 30 10:48:23 2022 +0900
@@ -68,6 +68,8 @@
 <-irr {a} {b} (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO   refl
           (IsStrictPartialOrder.trans PO     b<a a<b)
 
+ptrans =  IsStrictPartialOrder.trans PO
+
 open _==_
 open _⊆_
 
@@ -198,7 +200,7 @@
       chain : HOD
       chain⊆A : chain ⊆ A
       chain∋x : odef chain x
-      initial : {y : Ordinal } → odef chain y → * x < * y
+      initial : {y : Ordinal } → odef chain y → * x ≤ * y
       f-total : IsTotalOrderSet chain 
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
       f-immediate : { x y : Ordinal } → odef chain x → odef chain y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) )
@@ -363,12 +365,51 @@
                      ; initial = ZChain.initial zc0 ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17 }  -- no extention
           ... | case2 ¬fy<x with ODC.p∨¬p O ( x ≡ & ( SUP.sup ( supP ( ZChain.chain zc0 ) (ZChain.chain⊆A zc0 ) (ZChain.f-total zc0) ) ))
           ... | case1 x=sup = -- previous ordinal is a sup of a smaller ZChain
-                 record { chain = schain ; chain⊆A = {!!} ; f-total = {!!} ; f-next =  {!!}
-                     ; initial = {!!} ; f-immediate =  {!!} ; chain∋x  = case1 (ZChain.chain∋x zc0) ; is-max = {!!} } where -- x is sup
-                sp = SUP.sup ( supP ( ZChain.chain zc0 ) (ZChain.chain⊆A zc0 ) (ZChain.f-total zc0) ) 
+                 record { chain = schain ; chain⊆A = record { incl = A∋schain } ; f-total = scmp ; f-next = scnext 
+                     ; initial = scinit ; f-immediate =  {!!} ; chain∋x  = case1 (ZChain.chain∋x zc0) ; is-max = {!!} } where -- x is sup
+                sup0 = supP ( ZChain.chain zc0 ) (ZChain.chain⊆A zc0 ) (ZChain.f-total zc0) 
+                sp = SUP.sup sup0 
                 chain = ZChain.chain zc0
+                sc<A : {y : Ordinal} → odef chain y ∨ FClosure A f (& sp) y → y o< & A
+                sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< ( incl (ZChain.chain⊆A zc0) (subst (λ k → odef chain k) (sym &iso) zx )))
+                sc<A {y} (case2 fx) = subst (λ k → k o< (& A)) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fc (& sp) f mf fx )) )
                 schain : HOD
-                schain = record { od = record { def = λ x → odef chain x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = {!!} }
+                schain = record { od = record { def = λ x → odef chain x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy  }
+                A∋schain : {x : HOD } → schain ∋ x → A ∋ x
+                A∋schain (case1 zx ) = subst (λ k → odef A k ) &iso (incl (ZChain.chain⊆A zc0) (subst (λ k → odef chain k) (sym &iso) zx ))
+                A∋schain {y} (case2 fx ) = A∋fc (& sp) f mf fx 
+                cmp  : {a b : HOD} (za : odef chain (& a)) (fb : FClosure A f (& sp) (& b)) → Tri (a < b) (a ≡ b) (b < a )
+                cmp {a} {b} za fb  with SUP.x<sup sup0 za | s≤fc (& sp) f mf fb  
+                ... | case1 sp=a | case1 sp=b = tri≈ (λ lt → <-irr (case1 (sym eq)) lt ) eq (λ lt → <-irr (case1 eq) lt ) where
+                        eq : a ≡ b
+                        eq = trans sp=a (subst₂ (λ j k → j ≡ k ) *iso *iso sp=b )
+                ... | case1 sp=a | case2 sp<b = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b) lt ) where
+                        a<b : a < b
+                        a<b = subst (λ k → k < b ) (sym sp=a) (subst₂ (λ j k → j < k ) *iso *iso sp<b )
+                ... | case2 a<sp | case1 sp=b = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b) lt ) where
+                        a<b : a < b
+                        a<b = subst (λ k → a < k ) (trans sp=b *iso ) (subst (λ k → a < k ) (sym *iso) a<sp )
+                ... | case2 a<sp | case2 sp<b  = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b) lt ) where
+                        a<b : a < b
+                        a<b = ptrans  (subst (λ k → a < k ) (sym *iso) a<sp ) ( subst₂ (λ j k → j < k ) refl *iso sp<b )
+                scmp : {a b : HOD} → odef schain (& a) → odef schain (& b) → Tri (a < b) (a ≡ b) (b < a )
+                scmp (case1 za) (case1 zb) = ZChain.f-total zc0 za zb
+                scmp {a} {b} (case1 za) (case2 fb) = cmp za fb 
+                scmp  (case2 fa) (case1 zb) with  cmp zb fa
+                ... | tri< a ¬b ¬c = tri> ¬c (λ eq → ¬b (sym eq))  a
+                ... | tri≈ ¬a b ¬c = tri≈ ¬c (sym b) ¬a
+                ... | tri> ¬a ¬b c = tri< c (λ eq → ¬b (sym eq))  ¬a
+                scmp (case2 fa) (case2 fb) = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp (& sp) f mf fa fb)
+                scnext : {a : Ordinal} → odef schain a → odef schain (f a)
+                scnext {x} (case1 zx) = case1 (ZChain.f-next zc0 zx)
+                scnext {x} (case2 sx) = case2 ( fsuc x sx )
+                scinit :  {x : Ordinal} → odef schain x → * y ≤ * x
+                scinit {x} (case1 zx) = ZChain.initial zc0 zx
+                scinit {x} (case2 sx) with  (s≤fc (& sp) f mf sx ) |  SUP.x<sup sup0 (subst (λ k → odef chain k ) (sym &iso) ( ZChain.chain∋x zc0 ) )
+                ... | case1 sp=x | case1 y=sp = case1 {!!}
+                ... | case1 sp=x | case2 y<sp = case2 {!!}
+                ... | case2 sp<x | case1 y=sp = case2 {!!}
+                ... | case2 sp<x | case2 y<sp = case2 {!!}
           ... | case2 ¬x=sup =  -- x is not f y' nor sup of former ZChain from y
                    record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0
                      ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = {!!} }  where -- no extention