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)