# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1565516253 -32400
# Node ID a4cdfc84f65f130542a8b61da5dfc60b6dfad91c
# Parent  176ff97547b429c581de0fca539c10074de592b3
...

diff -r 176ff97547b4 -r a4cdfc84f65f cardinal.agda
--- a/cardinal.agda	Sun Aug 11 13:05:17 2019 +0900
+++ b/cardinal.agda	Sun Aug 11 18:37:33 2019 +0900
@@ -48,6 +48,34 @@
    lemma y | case1 refl = _⊗_.π2 lt
    lemma y | case2 not = o∅
 
+-- contra position of sup-o<
+--
+
+record Sup ( ψ : Ordinal  →  Ordinal )  : Set n where
+   field
+        sup-x  : Ordinal 
+        sup-lb : {z : Ordinal }  →  z o< sup-o ψ → z o< osuc (ψ sup-x )
+
+sup-o> : ( ψ : Ordinal  →  Ordinal )  → Sup ψ
+sup-o> ψ = record {
+        sup-x = od→ord ( minimul (Ord (osuc (sup-o ψ))) lemma )
+      ; sup-lb = λ {z} z<sψ → lemma1 z<sψ
+   } where
+       lemma0 : {x : Ordinal} → o∅ o< osuc x
+       lemma0 {x} with trio< o∅ (osuc x)
+       lemma0 {x} | tri< a ¬b ¬c = a
+       lemma0 {x} | tri≈ ¬a refl ¬c = ⊥-elim (¬x<0 <-osuc )
+       lemma0 {x} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
+       lemma : ¬ (Ord (osuc (sup-o ψ)) == od∅)
+       lemma record { eq→ = eq→ ; eq← = eq← } = ¬x<0 {o∅} ( eq→  lemma0 )
+       lemma1 :  {z : Ordinal} → z o< sup-o ψ → z o< osuc (ψ (od→ord (minimul (Ord (osuc (sup-o ψ))) lemma)))
+       lemma1 {z} lt with trio< z (ψ (od→ord (minimul (Ord (osuc (sup-o ψ))) lemma)))
+       lemma1 {z} lt | tri< a ¬b ¬c = ordtrans a <-osuc
+       lemma1 {z} lt | tri≈ ¬a refl ¬c = <-osuc
+       lemma1 {z} lt | tri> ¬a ¬b c = ⊥-elim (o<> c lemma2 ) where
+           lemma2 :  z o< ψ (od→ord (minimul (Ord (osuc (sup-o ψ))) lemma))
+           lemma2 = ordtrans sup-o< ( o<-subst (x∋minimul (Ord (osuc (sup-o ψ))) lemma ) ? ?)
+
 ------------
 --
 -- Onto map