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 ψ