module Chapter8.AlgebraicOrnament.Examples.Interval where open import Level hiding (zero ; suc) open import Data.Unit open import Data.Nat open import Data.Fin hiding (lift) open import Data.Product open import Relation.Binary.PropositionalEquality open import Chapter5.IDesc open import Chapter5.IDesc.Fixpoint open import Chapter5.IDesc.InitialAlgebra open import Chapter5.IDesc.Examples.Nat import Chapter8.AlgebraicOrnament α+m : Nat → Alg NatD (λ _ → Nat) α+m m {tt} (zero , lift tt) = m α+m m {tt} (suc zero , n , lift tt) = su n α+m m {tt} (suc (suc ()) , _) [_∶_] : Nat → Nat → Set [ m ∶ n ] = μ algOrnD (tt , n) where open Chapter8.AlgebraicOrnament.Func NatD (α+m m) ize : ∀{m} → [ m ∶ m ] ize = ⟨ (zero , lift tt) , refl , lift tt ⟩ isu : ∀{m n} → [ m ∶ n ] → [ m ∶ su n ] isu {m}{n} ik = ⟨ (suc zero , n , lift tt) , refl , ik , lift tt ⟩