open import Level

module Chapter5.IDesc.Algebra.Composition
         { k : Level}
         {A B C : Set k}
       where

open import Chapter5.IDesc

private 
  compose : func  A B  IDesc  B  IDesc  A
  compose E (`var b) = func.out E b
  compose E `1 = `1
  compose E (D  D') = compose E D  compose E D'
  compose E ( n T) =  n λ k  compose E (T k)
  compose E ( S T) =  S λ s  compose E (T s)
  compose E ( S T) =  S λ s  compose E (T s)

_∘_ : func  B C  func  A B  func  A C
D  E = func.mk λ c  compose E (func.out D c)