--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Ordinals.agda	Wed Aug 07 10:28:33 2019 +0900
@@ -0,0 +1,189 @@
+open import Level
+module Ordinals where
+
+open import zf
+
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+open import Data.Empty
+open import  Relation.Binary.PropositionalEquality
+open import  logic
+open import  nat
+open import Data.Unit using ( ⊤ )
+open import Relation.Nullary
+open import Relation.Binary
+open import Relation.Binary.Core
+
+
+
+record IsOrdinal {n : Level} (Ord : Set n) (_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<_ 
+
+record Ordinal {n : Level} : Set (suc n) where
+   field
+     ord : Set n
+     O< : ord → ord → Set n
+     isOrdinal : IsOrdinal ord O<
+
+open Ordinal
+
+_o<_ : {n : Level} ( x y : Ordinal {n}) → Set n
+_o<_ x y =  O< x {!!} {!!} -- (ord x) (ord y)
+
+o<-dom :  {n : Level} { x y : Ordinal {n}} → x o< y → Ordinal 
+o<-dom {n} {x} _ = x
+
+o<-cod :  {n : Level} { x y : Ordinal {n}} → x o< y → Ordinal 
+o<-cod {n} {_} {y} _ = y
+
+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∅ : {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 = {!!}
+
+osucc : {n : Level} {ox oy : Ordinal {n}} → oy o< ox  → osuc oy o< osuc ox
+osucc = {!!}
+
+o<¬≡ : {n : Level } { ox oy : Ordinal {suc n}} → ox ≡ oy  → ox o< oy  → ⊥
+o<¬≡ = {!!}
+
+¬x<0 : {n : Level} →  { x  : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} )
+¬x<0  = {!!}
+
+o<> : {n : Level} →  {x y : Ordinal {n}  }  →  y o< x → x o< y → ⊥
+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 )
+
+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< = {!!}
+
+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 )  )
+
+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
+
+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
+
+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
+
+--
+--  max ( osuc x , osuc y )
+--
+
+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
+
+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 )
+
+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 )
+
+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
+
+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
+
+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 _∧_
+
+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)
+
+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 
+     }
+ }
+
+TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m }
+  → {!!}
+  → {!!}
+  →  ∀ (x : Ordinal)  → ψ x
+TransFinite {n} {m} {ψ} = {!!}
+
+-- 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 ) 
+