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)