module Chapter9.Functions.Examples.Le where

open import Level 
  renaming ( zero to zeroL 
           ; suc to sucL )

open import Data.Unit
open import Data.Fin hiding (_<_ ; fold ; lift)
open import Data.Product

open import Relation.Binary.PropositionalEquality

open import Chapter5.IDesc.Fixpoint
open import Chapter5.IDesc.Lifting
open import Chapter5.IDesc.InitialAlgebra
open import Chapter5.IDesc.Induction

open import Chapter5.IDesc.Examples.Nat 
open import Chapter5.IDesc.Examples.Bool

open import Chapter9.Functions

type< : Type zeroL
type< = μ NatD [ tt ]→ μ NatD [ tt ]→ μ BoolD [ tt ]× `⊤

infix  _<_ 

β : (Nat → Bool × Lift ⊤) → DAlg NatD (λ _ → Bool × Lift ⊤)
β <n {i}{zero , lift tt} _ = true , lift tt
β <n {i}{suc zero , m , lift tt} _ = <n m
β <n {i}{suc (suc ()) , _} _


α : DAlg NatD (λ _ → Nat → Bool × Lift ⊤)
α {i} {zero , lift tt} (lift tt) = λ m → false , lift tt
α {i} {suc zero , n , lift tt} (<n , lift tt) = 
  induction NatD (λ _ → Bool × Lift ⊤) (λ {i}{xs} → β <n {i}{xs})
α {i} {suc (suc ()) , _} _

_<_ : ⟦ type< ⟧Type
m < n = induction NatD (λ _ → Nat → Bool × Lift ⊤) (λ {i}{xs} → α {i}{xs}) n m

private
  module Test where

    test-m<0 : ∀{m} → m < ze ≡ false , lift tt
    test-m<0 = refl

    test-0<su : ∀{n} → ze < su n ≡ true , lift tt
    test-0<su = refl
        
    test-su<suze : ∀{m} → su m < su ze ≡ false , lift tt
    test-su<suze = refl

    test-suze<su : ∀{n} → su ze < su (su n) ≡ true , lift tt
    test-suze<su = refl


{-
pattern ze = ⟨ zero , tt ⟩
pattern su n = ⟨ suc zero , n , tt ⟩ 

_<_ : ⟦ type< ⟧Type
m < ze = false , tt
ze < su n = true , tt 
su m < su n = m < n
⟨ suc (suc ()) , _ ⟩ < _
m < ⟨ suc (suc ()) , _ ⟩
-}