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

module SP
  (Usc : Set)(Tsc : Usc → Set)
  (Uar : Set)(Tar : Uar → Set)
  where

  data SP : Set1 where
    done : SP
    non-ind : (A : Usc) → (Tsc A → SP) → SP
    ind : Uar → SP → SP

  Arg : SP  → Set → Set
  Arg done X = ⊤
  Arg (non-ind A s) X = Σ[ a ∈ (Tsc A) ] Arg (s a) X
  Arg (ind A s) X = (Tar A → X) × Arg s X

  data D (s : SP) : Set where
    inn : Arg s (D s) → D s


  All : ∀ {a} → {X : Set} → (s : SP) → (P : X → Set a) → Arg s X → Set a
  All done P _ = ⊤
  All (non-ind A s) P (a , y) = All (s a) P y
  All (ind a s) P (f , y) = ((x : Tar a) → P (f x)) × All s P y

  every : {X : Set} → (s : SP) → (P : X → Set) →
          (f : (x : X) → P x) →
          (y : Arg s X) → All s P y
  every done P f y = y
  every (non-ind A s) P f (a , y) = every (s a) P f y
  every (ind A s) P f (g , y) = ((λ x → f (g x)) , every s P f y)

  elim : ∀ {a} →
         {s : SP} → (P : D s → Set a) →
         (step : (y : Arg s (D s)) → All s P y → P (inn y)) →
         (x : D s) → P x
  elim {s = s'} P step (inn y) = step y (every' s' y) where
    every' : (s : SP) → (y : Arg s (D s')) → All s P y
    every' done _ = _
    every' (non-ind A s) (a , y) = every' (s a) y
    every' (ind A s) (g , y) = (λ x → elim P step (g x)) , (every' s y)

  inn-inj : {s : SP} → {x y : Arg s (D s)} → inn x ≡ inn y → x ≡ y
  inn-inj {s} {x} {y} p = subst (λ y → Code (inn x) y) p refl
    where
      Code : D s -> D s -> Set
      Code = elim {s = s} (λ x → D s → Set)
                  (λ x' _ → elim {s = s} (λ _ → Set) (λ y' _ → x' ≡ y'))
      -- Code (inn x') (inn y') = x' ≡ y'