module Chapter9.Functions.Examples.Plus where

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

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

open import Chapter5.IDesc
open import Chapter5.IDesc.Fixpoint
open import Chapter5.IDesc.Induction
open import Chapter5.IDesc.Examples.Nat hiding (ze ; su)

open import Chapter9.Functions

type+ : Type zeroL
type+ = μ NatD [ tt ]→ μ NatD [ tt ]→ μ NatD [ tt  `⊤

infix 40 _+_ 

pattern ze = ⟨ zero , lift tt ⟩
pattern su n = ⟨ suc zero , n , lift tt ⟩ 

_+'_ :  type+ ⟧Type
m +' ze = m , lift tt
m +' su n = su (proj₁ (m +' n)) , lift tt 
m +'  suc (suc ()) , _ 


α : Nat  DAlg NatD  _  Nat × Lift )
α m {tt} {zero , lift tt} (lift tt) = m , lift tt
α m {tt} {suc zero , n , lift tt} ((m+n , lift tt) , lift tt) = su m+n , lift tt
α m {tt} {suc (suc ()) , _} _

_+_ :  type+ ⟧Type
m + n = induction NatD  _  Nat × Lift )  {i}{xs}  α m {i}{xs}) n

private
  module Test where

    open import Relation.Binary.PropositionalEquality

    test-0+0 : ze + ze  ze +' ze
    test-0+0 = refl
  
    test-m+0 : ∀{m}  m + ze  (m , lift tt)
    test-m+0 = refl

    test-m+1 : ∀{m}  m + (su ze)  m +' (su ze)
    test-m+1 = refl

    test-m+2 : ∀{m}  m + (su (su ze))  m +' (su (su ze))
    test-m+2 = refl