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

module IR
  (D : Set)
  where

  data IR : Set1 where
    done : D → IR
    non-ind : (A : Set) → (A → IR) → IR
    ind : (A : Set) → ((A → D) → IR) → IR

  record Fam (X : Set) : Set1 where
    constructor _,_
    field
      idx : Set
      fam : idx → X

  record FamMorphism {X : Set} (A B : Fam X) : Set1 where
    constructor _,_
    open Fam
    field
      idxfun : idx A → idx B
      famfun : (x : idx A) → fam A x ≡ fam B (idxfun x)

  Arg : IR  → Fam D → Set
  Arg (done d) XT = ⊤
  Arg (non-ind A γ) XT = Σ[ a ∈ A ] (Arg (γ a) XT)
  Arg (ind A γ) XT@(X , T) = Σ[ f ∈ ((x : A) → X) ] (Arg (γ (T ∘ f)) XT)

  Val : (γ : IR)  → (XT : Fam D) → Arg γ XT → D
  Val (done d) XT x = d
  Val (non-ind A γ) XT (a , x) = Val (γ a) XT x
  Val (ind A γ) XT@(X , T) (g , x) = Val (γ (λ x → T (g x))) XT x

  ArgVal : (γ : IR) → Fam D → Fam D
  ArgVal γ XT = (Arg γ XT , Val γ XT)

  mutual

    {-# NO_POSITIVITY_CHECK #-}
    data U (γ : IR) : Set where
      inn : Arg γ (U γ , T γ) → U γ

    {-# TERMINATING #-}
    T : (γ : IR) → U γ → D
    T γ (inn x) = Val γ (U γ , T γ) x

  private
    inn-morphism : ∀ γ → FamMorphism (ArgVal γ (U γ , T γ)) (U γ , T γ)
    inn-morphism γ = (inn , λ x → refl)