open import Data.Product
open import Data.Unit.Polymorphic
open import Relation.Binary.PropositionalEquality
open import Data.Bool


module SPF
  (I : Set)
  where

  data SPF : Set1 where
    done : I → SPF
    non-ind : (A : Set) → (A → SPF) → SPF
    ind : (A : Set) → (A → I) → SPF → SPF

  Arg : SPF  → (I → Set) → (I → Set)
  Arg (done i) X j = i ≡ j
  Arg (non-ind A s) X j = Σ[ a ∈ A ] (Arg (s a) X j)
  Arg (ind A f s) X j = ((x : A) → X (f x)) × Arg s X j

  data D (s : SPF) : I → Set where
    inn : ∀ {i} → Arg s (D s) i → D s i

  _+SPF_ : SPF → SPF → SPF
  γ +SPF ψ = non-ind Bool λ x → if x then γ else ψ