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
α+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)