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 ψ