```-- See Polynomial.InitialPleasingAgda for a version of this file not bypassing
-- the positivity and termination checkers

module Polynomial.Initial where

open import Function
open import Data.Product
open import Data.Unit
open import Level

open import Prelude.Fam
open import Polynomial.IR

-- formation and introduction rules

module _ {D : Set1}{c : IR D D} where

mutual

{-# NO_POSITIVITY_CHECK #-}
data U  : Set where
intro : ⟦ c ⟧₀ (U , T) -> U

{-# TERMINATING #-}
T : U -> D
T (intro x) = ⟦ c ⟧₁ (U , T) x

-- Elimination rules

IH : ∀ {a}{D : Set1}(c : Poly D){Z : Fam D} ->
(P : ind Z -> Set a) -> Node c Z -> Set a
IH idPN P x = P x
IH (con A) P a = Lift ⊤
IH (sigma S T) {Z} P (x , y) = (IH S P x) × IH (T (info S Z x)) P y
IH (pi A T) P f = (a : A) -> IH (T a) P (f a)

mapIH : ∀ {a}{D : Set1}(c : Poly D){Z : Fam D} ->
(P : ind Z -> Set a) -> (g : (x : ind Z) -> P x) ->
(x : Node c Z) -> IH c P x
mapIH idPN P g x = g x
mapIH (con A) P g a = lift tt
mapIH (sigma S T) P g (x , y) = mapIH S P g x , mapIH (T _) P g y
mapIH (pi A T) P g f = λ a → mapIH (T a) P g (f a)

module _ {D : Set1}{c : IR D D} where

{-# TERMINATING #-}
elim : ∀ {a}(P : U {D} {c} -> Set a) ->
(step : (x : ⟦ c ⟧₀ (U , T)) -> IH (proj₁ c) P x -> P (intro x)) ->
(x : U) -> P x
elim P step (intro x) = step x (mapIH (proj₁ c) P (elim P step) x)
```