```module DS.powerFromComposition where

-- Conversely, if we have composition, we have powers

open import Prelude.Basic
open import Prelude.Equality
open import Prelude.Fam
open import Prelude.Equivalences

open import DS.IR

------------------------------------------------------------------
postulate
-- assuming there is a composition combinator for Dybjer-Setzer IR codes...
_○_ : {C D E : Set1} -> DS D E -> DS C D -> DS C E
-- ...with the right decoding...
_○_-equiv : {C D E : Set1} -> (c : DS D E) -> (d : DS C D) -> {Z : Fam C} ->
⟦ c ○ d ⟧ Z ≃ (⟦ c ⟧ ∘ ⟦ d ⟧) Z
-- ...we can define powers of DS codes

_⟶_ : {D E : Set1} -> (S : Set) -> DS D E -> DS D (S -> E)
S ⟶ c = δ S (λ h → ι h) ○ c

⟶-equiv : ∀ {D E} -> (S : Set)(c : DS D E) -> {Z : Fam D} ->
⟦ S ⟶ c ⟧ Z ≃ (S Fam⟶ (⟦ c ⟧ Z))
⟶-equiv S c {Z} = transEq (_○_-equiv (δ S ι) c {Z}) sigmaUnitEquiv
where sigmaUnitEquiv : {D : Set1}{A : Set}{T : A -> D} ->
((Σ[ x ∈ A ] ⊤) , T ∘ proj₁) ≃ (A , T)
sigmaUnitEquiv
= record { left = proj₁ , (λ x → refl)
; right = (λ a → a , tt) , (λ a → refl)
; leftright = refl
; rightleft = refl
}
```