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
                   }