module Calf.Computation.Power where

open import Calf.Value
open import Calf.Value.Pi
open import Calf.Computation

Πᢜ : (X : 𝒱) β†’ (X β†’ π’ž) β†’ π’ž
Πᢜ X A .U = (x : X) β†’ U (A x)
Πᢜ X A .is-set = isSetΞ  Ξ» x β†’ A x .is-set
Πᢜ X A .charge c e x = A x .charge c (e x)
Πᢜ X A .charge/0 {e} = funExt Ξ» x β†’ A x .charge/0 {e x}
Πᢜ X A .charge/+ {e} {c₁} {cβ‚‚} = funExt Ξ» x β†’ A x .charge/+ {e x} {c₁} {cβ‚‚}

syntax Πᢜ X (Ξ» x β†’ A) = [ x ∈ X ] ⇀ A

infixr 2 _⇀_

_⇀_ : 𝒱 β†’ π’ž β†’ π’ž
X ⇀ A = [ _ ∈ X ] ⇀ A

opaque
  powlam : (X β†’ A ⊸ B) β†’ A ⊸ (X ⇀ B)
  powlam e .U a x = e x .U a
  powlam e .charge c a = funExt Ξ» x β†’ e x .charge c a

  powapp : A ⊸ (X ⇀ B) β†’ X β†’ A ⊸ B
  powapp e x .U a = e .U a x
  powapp e x .charge c a = cong (_$ x) (e .charge c a)