module Orn.AlgebraicOrnament.Examples.Leq where

open import Logic.IProp

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

open import Relation.Binary.PropositionalEquality

open import IDesc.IDesc
open import IDesc.Fixpoint
open import IDesc.InitialAlgebra

open import IDesc.Examples.Nat

import  Orn.AlgebraicOrnament
import  Orn.AlgebraicOrnament.Coherence

-- Paper: Example 4.23

α+m : Nat  Alg NatD  _  Nat)
α+m m {tt} (zero , tt) = m
α+m m {tt} (suc zero , n) = su n
α+m m {tt} (suc (suc ()) , _)

_+_ : Nat  Nat  Nat
m + n = fold NatD (α+m m) n

_≦_ : Nat  Nat  Set
m  n = μ algOrnD (tt , n)
  where open Orn.AlgebraicOrnament.Func NatD (α+m m)

ize : ∀{m}  m  m 
ize =  (zero , tt) , refl , tt 

isu : ∀{m n}  m  n  m  su n
isu {m}{n} ik =  (suc zero , n) , refl , ik  

forgetOrnament : ∀{m n}  m  n  Nat
forgetOrnament {m} = forgetAlgOrn
    where open Orn.AlgebraicOrnament.Coherence NatD (α+m m)

lemma-coherence :  {m n}  (t : m  n)   n  m + forgetOrnament t
lemma-coherence {m} = coherentOrn 
  where open Orn.AlgebraicOrnament.Coherence NatD (α+m m)