# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1657410061 -32400
# Node ID 6826883cfbf848e5ffc150ee414fc21111284624
# Parent  822fce8af5796be1c8f1a127ed6e9e734b73f61c
chain-total done

diff -r 822fce8af579 -r 6826883cfbf8 src/zorn.agda
--- a/src/zorn.agda	Sun Jul 10 08:10:34 2022 +0900
+++ b/src/zorn.agda	Sun Jul 10 08:41:01 2022 +0900
@@ -297,18 +297,33 @@
 
 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) 
    {s s1 a b : Ordinal } ( ca : Chain A f mf ay s a ) ( cb : Chain A f mf ay s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
-chain-total A f mf {y} ay {s} {s1} {a} {b} ca cb = TransFinite 
-   {λ x → {s1 a b : Ordinal } ( ca : Chain A f mf ay x a ) ( cb : Chain A f mf ay s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )} ct-ind s ca cb where
-     ct-ind : (x : Ordinal) →
-       ((y₁ : Ordinal) → y₁ o< x → {s1 a b : Ordinal} → Chain A f mf ay y₁ a → Chain A f mf ay s1 b → Tri (* a < * b) (* a ≡ * b) (* b < * a)) 
-       → {s1 a b : Ordinal} → Chain A f mf ay x a → Chain A f mf ay s1 b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
-     ct-ind x prev {s1} {a} {b} (ch-init s a x=0 fca) (ch-init s1 b x=0' fcb) = fcn-cmp y f mf fca fcb
-     ct-ind x prev {s1} {a} {b} (ch-init s a x=0 fca) (ch-is-sup 0<x as supb fcb) = ?
-     ct-ind x prev {s1} {a} {b} (ch-is-sup 0<x as supa fca) (ch-init s1 b x=0' fcb) = ?
-     ct-ind x prev {s1} {a} {b} (ch-is-sup 0<x as supa fca) (ch-is-sup 0<x' as' supb fcb) with trio< x s1
-     ... | tri< a₁ ¬b ¬c = ?
+chain-total A f mf {y} ay {s} {s1} {a} {b} ca cb = ct-ind s ca cb where
+     ct-ind : (x : Ordinal) → {s1 a b : Ordinal} → Chain A f mf ay x a → Chain A f mf ay s1 b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
+     ct-ind x {s1} {a} {b} (ch-init s a x=0 fca) (ch-init s1 b x=0' fcb) = fcn-cmp y f mf fca fcb
+     ct-ind x {s1} {a} {b} (ch-init s a x=0 fca) (ch-is-sup 0<x as supb fcb) = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
+         ct00 : * a < * s1
+         ct00 = supb _ _ 0<x (subst (λ k → Chain A f mf ay k a) x=0 (ch-init s a x=0 fca) )
+         ct01 : * a < * b 
+         ct01 with s≤fc s1 f mf fcb 
+         ... | case1 eq =  subst (λ k → * a < k ) eq ct00
+         ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
+     ct-ind x {s1} {a} {b} (ch-is-sup 0<x as supa fca) (ch-init s1 b x=0' fcb) = ?
+     ct-ind x {s1} {a} {b} (ch-is-sup 0<x as supa fca) (ch-is-sup 0<x' as' supb fcb) with trio< x s1
+     ... | tri< a₁ ¬b ¬c = tri< ct02  (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt)  where
+         ct03 : * a < * s1
+         ct03 = supb _ _ a₁ (ch-is-sup 0<x as supa fca)
+         ct02 : * a < * b 
+         ct02 with s≤fc s1 f mf fcb 
+         ... | case1 eq =  subst (λ k → * a < k ) eq ct03
+         ... | case2 lt =  IsStrictPartialOrder.trans POO ct03 lt
      ... | tri≈ ¬a  refl ¬c = fcn-cmp s1 f mf fca fcb
-     ... | tri> ¬a ¬b c = ?
+     ... | tri> ¬a ¬b c = tri> (λ lt → <-irr (case2 ct04) lt) (λ eq → <-irr (case1 (eq)) ct04) ct04    where
+         ct05 : * b < * x
+         ct05 = supa _ _ c (ch-is-sup 0<x' as' supb fcb)
+         ct04 : * b < * a 
+         ct04 with s≤fc x f mf fca 
+         ... | case1 eq =  subst (λ k → * b < k ) eq ct05
+         ... | case2 lt =  IsStrictPartialOrder.trans POO ct05 lt
 
 Zorn-lemma : { A : HOD } 
     → o∅ o< & A