# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1565544392 -32400
# Node ID 5e36744b8dcec39bd43028bbe98b3af9326ff3f2
# Parent  49736efc822bb5f72d1f34e7fbe09557f700283a
...

diff -r 49736efc822b -r 5e36744b8dce cardinal.agda
--- a/cardinal.agda	Sun Aug 11 20:42:48 2019 +0900
+++ b/cardinal.agda	Mon Aug 12 02:26:32 2019 +0900
@@ -87,14 +87,20 @@
     cardinal-p x with p∨¬p ( Onto (Ord x) X ) 
     cardinal-p x | case1 True = record { proj1 = x ; proj2 = yes True }
     cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False }
-    lemma1 :  (x : Ordinal) → ((y : Ordinal) → y o< x → Lift (suc n) (y o< (osuc (sup-o (λ x₁ → proj1 (cardinal-p x₁)))) → Onto (Ord y) X)) →
-                    Lift (suc n) (x o< (osuc  (sup-o (λ x₁ → proj1 (cardinal-p x₁)))) → Onto (Ord x) X)
-    lemma1 = {!!}
-    onto : Onto (Ord (sup-o (λ x → proj1 (cardinal-p x)))) X
-    onto with TransFinite {λ x → Lift (suc n) ( x o< osuc (sup-o (λ x → proj1 (cardinal-p x))) → Onto (Ord x) X ) } lemma1 (sup-o (λ x → proj1 (cardinal-p x))) 
+    S = sup-o (λ x → proj1 (cardinal-p x))
+    lemma1 :  (x : Ordinal) → ((y : Ordinal) → y o< x → Lift (suc n) (y o< (osuc S) → Onto (Ord y) X)) →
+                    Lift (suc n) (x o< (osuc S) → Onto (Ord x) X)
+    lemma1 x prev with trio< x (osuc S)
+    lemma1 x prev | tri< a ¬b ¬c with osuc-≡< a
+    lemma1 x prev | tri< a ¬b ¬c | case1 x=S = {!!}
+    lemma1 x prev | tri< a ¬b ¬c | case2 x<S = {!!}
+    lemma1 x prev | tri≈ ¬a b ¬c = lift ( λ lt → ⊥-elim ( o<¬≡ b lt ))
+    lemma1 x prev | tri> ¬a ¬b c = lift ( λ lt → ⊥-elim ( o<> c lt ))
+    onto : Onto (Ord S) X
+    onto with TransFinite {λ x → Lift (suc n) ( x o< osuc S → Onto (Ord x) X ) } lemma1 S 
     ... | lift t = t <-osuc  where
-    cmax : (y : Ordinal) → sup-o (λ x → proj1 (cardinal-p x)) o< y → ¬ Onto (Ord y) X
-    cmax y lt ontoy = o<> lt (o<-subst  {_} {_} {y} {sup-o (λ x → proj1 (cardinal-p x))}
+    cmax : (y : Ordinal) → S o< y → ¬ Onto (Ord y) X
+    cmax y lt ontoy = o<> lt (o<-subst  {_} {_} {y} {S}
        (sup-o<  {λ x → proj1 ( cardinal-p x)}{y}  ) lemma refl ) where
           lemma : proj1 (cardinal-p y) ≡ y
           lemma with  p∨¬p ( Onto (Ord y) X )