```module Polynomial.InitialPleasingAgda 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

-- specialised variants so that Agda can see that U is strictly
-- positive and T terminating
Node' : Poly D -> Set
Node' idPN = U
Node' (con A) = A
Node' (sigma S T) = Σ[ s ∈ Node' S ] Node' (T (info' S s))
Node' (pi A T) = (x : A) -> Node' (T x)

info' : (T : Poly D) -> Node' T -> Info T
info' idPN x = T x
info' (con A) a = lift a
info' (sigma S T) (s , x) = info' S s , info' (T (info' S s)) x
info' (pi A T) g = λ a → info' (T a) (g a)

data U  : Set where
intro : Node' (proj₁ c) -> U

T : U -> D
T (intro x) = (proj₂ c) (info' (proj₁ c) x)

-- Elimination rules

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

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

mutual

elim : ∀ {a}(P : U {c = c} -> Set a) ->
(step : (x : Node' (proj₁ c)) -> IH (proj₁ c) P x -> P (intro x)) ->
(x : U) -> P x
elim P step (intro x) = step x (mapIH (proj₁ c) P step x)

mapIH : ∀ {a}(c' : Poly D) ->
(P : U {c = c} -> Set a) ->
(step : (x : Node' (proj₁ c)) -> IH (proj₁ c) P x -> P (intro x)) ->
(x : Node' {c = c} c') -> IH c' P x
mapIH idPN P step x = elim P step x
mapIH (con A) P step a = lift tt
mapIH (sigma S T) P step (x , y) = mapIH S P step x , mapIH (T _) P step y
mapIH (pi A T) P step f = λ a → mapIH (T a) P step (f a)

```