# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1565253141 -32400
# Node ID 1709c80b72754abadfbb34d8e26852ad40c9d9df
# Parent  95a26d1698f4db3d86c2168221a4d8c31fd62501
fix Ordinals

diff -r 95a26d1698f4 -r 1709c80b7275 Ordinals.agda
--- a/Ordinals.agda	Wed Aug 07 10:28:33 2019 +0900
+++ b/Ordinals.agda	Thu Aug 08 17:32:21 2019 +0900
@@ -15,175 +15,184 @@
 
 
 
-record IsOrdinal {n : Level} (Ord : Set n) (_O<_ : Ord → Ord → Set n) : Set n where
+record IsOrdinals {n : Level} (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) : Set n where
    field
-     Otrans :  {x y z : Ord }  → x O< y → y O< z → x O< z
-     OTri : Trichotomous {n} _≡_  _O<_ 
+     Otrans :  {x y z : ord }  → x o< y → y o< z → x o< z
+     OTri : Trichotomous {n} _≡_  _o<_ 
+     ¬x<0 :   { x  : ord  } → ¬ ( x o< o∅  )
+     <-osuc :  { x : ord  } → x o< osuc x
+     osuc-≡< :  { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)  
 
-record Ordinal {n : Level} : Set (suc n) where
+record Ordinals {n : Level} : Set (suc n) where
    field
      ord : Set n
-     O< : ord → ord → Set n
-     isOrdinal : IsOrdinal ord O<
+     o∅ : ord
+     osuc : ord → ord
+     _o<_ : ord → ord → Set n
+     isOrdinal : IsOrdinals ord o∅ osuc _o<_
 
-open Ordinal
-
-_o<_ : {n : Level} ( x y : Ordinal {n}) → Set n
-_o<_ x y =  O< x {!!} {!!} -- (ord x) (ord y)
+module inOrdinal  {n : Level} (O : Ordinals {n} ) where
 
-o<-dom :  {n : Level} { x y : Ordinal {n}} → x o< y → Ordinal 
-o<-dom {n} {x} _ = x
+        Ordinal : Set n
+        Ordinal  = Ordinals.ord O 
+
+        _o<_ :  Ordinal  → Ordinal  → Set n
+        _o<_ = Ordinals._o<_ O 
 
-o<-cod :  {n : Level} { x y : Ordinal {n}} → x o< y → Ordinal 
-o<-cod {n} {_} {y} _ = y
+        osuc :   Ordinal  → Ordinal 
+        osuc  = Ordinals.osuc O 
 
-o<-subst : {n : Level } {Z X z x : Ordinal {n}}  → Z o< X → Z ≡ z  →  X ≡ x  →  z o< x
-o<-subst df refl refl = df
+        o∅ :   Ordinal  
+        o∅ = Ordinals.o∅ O
 
-o∅ : {n : Level} → Ordinal {n}
-o∅  = {!!}
-
-osuc : {n : Level} ( x : Ordinal {n} ) → Ordinal {n}
-osuc = {!!}
-
-<-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x
-<-osuc = {!!}
+        ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O)
+        osuc-≡< = IsOrdinals.osuc-≡<  (Ordinals.isOrdinal O)
+        <-osuc = IsOrdinals.<-osuc  (Ordinals.isOrdinal O)
+        
+        o<-dom :   { x y : Ordinal } → x o< y → Ordinal 
+        o<-dom  {x} _ = x
 
-osucc : {n : Level} {ox oy : Ordinal {n}} → oy o< ox  → osuc oy o< osuc ox
-osucc = {!!}
+        o<-cod :   { x y : Ordinal } → x o< y → Ordinal 
+        o<-cod  {_} {y} _ = y
 
-o<¬≡ : {n : Level } { ox oy : Ordinal {suc n}} → ox ≡ oy  → ox o< oy  → ⊥
-o<¬≡ = {!!}
+        o<-subst : {Z X z x : Ordinal }  → Z o< X → Z ≡ z  →  X ≡ x  →  z o< x
+        o<-subst df refl refl = df
 
-¬x<0 : {n : Level} →  { x  : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} )
-¬x<0  = {!!}
+        ordtrans :  {x y z : Ordinal  }   → x o< y → y o< z → x o< z
+        ordtrans = IsOrdinals.Otrans (Ordinals.isOrdinal O)
 
-o<> : {n : Level} →  {x y : Ordinal {n}  }  →  y o< x → x o< y → ⊥
-o<> = {!!}
+        trio< : Trichotomous  _≡_  _o<_ 
+        trio< = IsOrdinals.OTri (Ordinals.isOrdinal O)
 
-osuc-≡< : {n : Level} { a x : Ordinal {n} } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)  
-osuc-≡< = {!!}
-
-osuc-< : {n : Level} { x y : Ordinal {n} } → y o< osuc x  → x o< y → ⊥
-osuc-< = {!!}
-
-_o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n)
-a o≤ b  = (a ≡ b)  ∨ ( a o< b )
+        o<¬≡ :  { ox oy : Ordinal } → ox ≡ oy  → ox o< oy  → ⊥
+        o<¬≡ {ox} {oy} eq lt with trio< ox oy
+        o<¬≡ {ox} {oy} eq lt | tri< a ¬b ¬c = ¬b eq
+        o<¬≡ {ox} {oy} eq lt | tri≈ ¬a b ¬c = ¬a lt
+        o<¬≡ {ox} {oy} eq lt | tri> ¬a ¬b c = ¬b eq
 
-ordtrans : {n : Level} {x y z : Ordinal {n} }   → x o< y → y o< z → x o< z
-ordtrans = {!!}
-
-trio< : {n : Level } → Trichotomous {suc n} _≡_  _o<_ 
-trio< = {!!}
+        o<> :   {x y : Ordinal   }  →  y o< x → x o< y → ⊥
+        o<> {ox} {oy} lt tl with trio< ox oy
+        o<> {ox} {oy} lt tl | tri< a ¬b ¬c = ¬c lt
+        o<> {ox} {oy} lt tl | tri≈ ¬a b ¬c = ¬a tl
+        o<> {ox} {oy} lt tl | tri> ¬a ¬b c = ¬a tl
 
-xo<ab : {n : Level} {oa ob : Ordinal {suc n}} → ( {ox : Ordinal {suc n}} → ox o< oa  → ox o< ob ) → oa o< osuc ob
-xo<ab {n}  {oa} {ob} a→b with trio< oa ob
-xo<ab {n}  {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc
-xo<ab {n}  {oa} {ob} a→b | tri≈ ¬a refl ¬c = <-osuc
-xo<ab {n}  {oa} {ob} a→b | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c )  )
+        osuc-< :  { x y : Ordinal  } → y o< osuc x  → x o< y → ⊥
+        osuc-< {x} {y} y<ox x<y with osuc-≡< y<ox
+        osuc-< {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y
+        osuc-< {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x
 
-maxα : {n : Level} →  Ordinal {suc n} →  Ordinal  → Ordinal
-maxα x y with trio< x y
-maxα x y | tri< a ¬b ¬c = y
-maxα x y | tri> ¬a ¬b c = x
-maxα x y | tri≈ ¬a refl ¬c = x
+        osucc :  {ox oy : Ordinal } → oy o< ox  → osuc oy o< osuc ox  
+        ----   y < osuc y < x < osuc x
+        ----   y < osuc y = x < osuc x
+        ----   y < osuc y > x < osuc x   -> y = x ∨ x < y → ⊥
+        osucc {ox} {oy} oy<ox with trio< (osuc oy) ox
+        osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc
+        osucc {ox} {oy} oy<ox | tri≈ ¬a refl ¬c = <-osuc
+        osucc {ox} {oy} oy<ox | tri> ¬a ¬b c with  osuc-≡< c
+        osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy<ox)
+        osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy<ox)
+
+        open _∧_
 
-minα : {n : Level} →  Ordinal {n} →  Ordinal  → Ordinal
-minα {n} x y with trio< {n} x  y
-minα x y | tri< a ¬b ¬c = x
-minα x y | tri> ¬a ¬b c = y
-minα x y | tri≈ ¬a refl ¬c = x
+        osuc2 :  ( x y : Ordinal  ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
+        proj2 (osuc2 x y) lt = osucc lt
+        proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy
+        proj1 (osuc2 x y) ox<ooy | case1 ox=oy = o<-subst <-osuc refl ox=oy
+        proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy 
 
-min1 : {n : Level} →  {x y z : Ordinal {n} } → z o< x → z o< y → z o< minα x y
-min1 {n} {x} {y} {z} z<x z<y with trio< {n} x y
-min1 {n} {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x
-min1 {n} {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x
-min1 {n} {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y
+        _o≤_ :  Ordinal → Ordinal → Set  n
+        a o≤ b  = (a ≡ b)  ∨ ( a o< b )
+
 
---
---  max ( osuc x , osuc y )
---
+        xo<ab :  {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa  → ox o< ob ) → oa o< osuc ob
+        xo<ab   {oa} {ob} a→b with trio< oa ob
+        xo<ab   {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc
+        xo<ab   {oa} {ob} a→b | tri≈ ¬a refl ¬c = <-osuc
+        xo<ab   {oa} {ob} a→b | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c )  )
 
-omax : {n : Level} ( x y : Ordinal {suc n} ) → Ordinal {suc n}
-omax {n} x y with trio< x y
-omax {n} x y | tri< a ¬b ¬c = osuc y
-omax {n} x y | tri> ¬a ¬b c = osuc x
-omax {n} x y | tri≈ ¬a refl ¬c  = osuc x
+        maxα :   Ordinal  →  Ordinal  → Ordinal
+        maxα x y with trio< x y
+        maxα x y | tri< a ¬b ¬c = y
+        maxα x y | tri> ¬a ¬b c = x
+        maxα x y | tri≈ ¬a refl ¬c = x
 
-omax< : {n : Level} ( x y : Ordinal {suc n} ) → x o< y → osuc y ≡ omax x y
-omax< {n} x y lt with trio< x y
-omax< {n} x y lt | tri< a ¬b ¬c = refl
-omax< {n} x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt )
-omax< {n} x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt )
+        minα :    Ordinal  →  Ordinal  → Ordinal
+        minα  x y with trio<  x  y
+        minα x y | tri< a ¬b ¬c = x
+        minα x y | tri> ¬a ¬b c = y
+        minα x y | tri≈ ¬a refl ¬c = x
 
-omax≡ : {n : Level} ( x y : Ordinal {suc n} ) → x ≡ y → osuc y ≡ omax x y
-omax≡ {n} x y eq with trio< x y
-omax≡ {n} x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq )
-omax≡ {n} x y eq | tri≈ ¬a refl ¬c = refl
-omax≡ {n} x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq )
+        min1 :   {x y z : Ordinal  } → z o< x → z o< y → z o< minα x y
+        min1  {x} {y} {z} z<x z<y with trio<  x y
+        min1  {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x
+        min1  {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x
+        min1  {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y
 
-omax-x : {n : Level} ( x y : Ordinal {suc n} ) → x o< omax x y
-omax-x {n} x y with trio< x y
-omax-x {n} x y | tri< a ¬b ¬c = ordtrans a <-osuc
-omax-x {n} x y | tri> ¬a ¬b c = <-osuc
-omax-x {n} x y | tri≈ ¬a refl ¬c = <-osuc
+        --
+        --  max ( osuc x , osuc y )
+        --
+
+        omax :  ( x y : Ordinal  ) → Ordinal 
+        omax  x y with trio< x y
+        omax  x y | tri< a ¬b ¬c = osuc y
+        omax  x y | tri> ¬a ¬b c = osuc x
+        omax  x y | tri≈ ¬a refl ¬c  = osuc x
 
-omax-y : {n : Level} ( x y : Ordinal {suc n} ) → y o< omax x y
-omax-y {n} x y with  trio< x y
-omax-y {n} x y | tri< a ¬b ¬c = <-osuc
-omax-y {n} x y | tri> ¬a ¬b c = ordtrans c <-osuc
-omax-y {n} x y | tri≈ ¬a refl ¬c = <-osuc
+        omax< :  ( x y : Ordinal  ) → x o< y → osuc y ≡ omax x y
+        omax<  x y lt with trio< x y
+        omax<  x y lt | tri< a ¬b ¬c = refl
+        omax<  x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt )
+        omax<  x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt )
 
-omxx : {n : Level} ( x : Ordinal {suc n} ) → omax x x ≡ osuc x
-omxx {n} x with  trio< x x
-omxx {n} x | tri< a ¬b ¬c = ⊥-elim (¬b refl )
-omxx {n} x | tri> ¬a ¬b c = ⊥-elim (¬b refl )
-omxx {n} x | tri≈ ¬a refl ¬c = refl
-
-omxxx : {n : Level} ( x : Ordinal {suc n} ) → omax x (omax x x ) ≡ osuc (osuc x)
-omxxx {n} x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc ))
-
-open _∧_
+        omax≡ :  ( x y : Ordinal  ) → x ≡ y → osuc y ≡ omax x y
+        omax≡  x y eq with trio< x y
+        omax≡  x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq )
+        omax≡  x y eq | tri≈ ¬a refl ¬c = refl
+        omax≡  x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq )
 
-osuc2 : {n : Level} ( x y : Ordinal {suc n} ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
-osuc2 = {!!}
-
-OrdTrans : {n : Level} → Transitive {suc n} _o≤_
-OrdTrans (case1 refl) (case1 refl) = case1 refl
-OrdTrans (case1 refl) (case2 lt2) = case2 lt2
-OrdTrans (case2 lt1) (case1 refl) = case2 lt1
-OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y)
+        omax-x :  ( x y : Ordinal  ) → x o< omax x y
+        omax-x  x y with trio< x y
+        omax-x  x y | tri< a ¬b ¬c = ordtrans a <-osuc
+        omax-x  x y | tri> ¬a ¬b c = <-osuc
+        omax-x  x y | tri≈ ¬a refl ¬c = <-osuc
 
-OrdPreorder : {n : Level} → Preorder (suc n) (suc n) (suc n)
-OrdPreorder {n} = record { Carrier = Ordinal
-   ; _≈_  = _≡_ 
-   ; _∼_   = _o≤_
-   ; isPreorder   = record {
-        isEquivalence = record { refl = refl  ; sym = sym ; trans = trans }
-        ; reflexive     = case1 
-        ; trans         = OrdTrans 
-     }
- }
+        omax-y :  ( x y : Ordinal  ) → y o< omax x y
+        omax-y  x y with  trio< x y
+        omax-y  x y | tri< a ¬b ¬c = <-osuc
+        omax-y  x y | tri> ¬a ¬b c = ordtrans c <-osuc
+        omax-y  x y | tri≈ ¬a refl ¬c = <-osuc
+
+        omxx :  ( x : Ordinal  ) → omax x x ≡ osuc x
+        omxx  x with  trio< x x
+        omxx  x | tri< a ¬b ¬c = ⊥-elim (¬b refl )
+        omxx  x | tri> ¬a ¬b c = ⊥-elim (¬b refl )
+        omxx  x | tri≈ ¬a refl ¬c = refl
+
+        omxxx :  ( x : Ordinal  ) → omax x (omax x x ) ≡ osuc (osuc x)
+        omxxx  x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc ))
+
+        open _∧_
 
-TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m }
-  → {!!}
-  → {!!}
-  →  ∀ (x : Ordinal)  → ψ x
-TransFinite {n} {m} {ψ} = {!!}
+        OrdTrans :  Transitive  _o≤_
+        OrdTrans (case1 refl) (case1 refl) = case1 refl
+        OrdTrans (case1 refl) (case2 lt2) = case2 lt2
+        OrdTrans (case2 lt1) (case1 refl) = case2 lt1
+        OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y)
 
--- we cannot prove this in intutionistic logic 
---  (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p )  → p
--- postulate 
---  TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) 
---   → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
---   → {p : Set l} ( P : { y : Ordinal {n} } →  ψ y → p )
---   → p
---
--- Instead we prove
---
-TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) 
-  → {p : Set l} ( P : { y : Ordinal {n} } →  ψ y → ¬ p )
-  → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
-  → ¬ p
-TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 
+        OrdPreorder :   Preorder n n n
+        OrdPreorder  = record { Carrier = Ordinal
+           ; _≈_  = _≡_ 
+           ; _∼_   = _o≤_
+           ; isPreorder   = record {
+                isEquivalence = record { refl = refl  ; sym = sym ; trans = trans }
+                ; reflexive     = case1 
+                ; trans         = OrdTrans 
+             }
+         }
 
+        TransFiniteExists : {m l : Level} → ( ψ : Ordinal  → Set m ) 
+          → {p : Set l} ( P : { y : Ordinal  } →  ψ y → ¬ p )
+          → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
+          → ¬ p
+        TransFiniteExists  {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 
+