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 )