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

module Uniform.Initial where

open import Prelude.Basic
open import Prelude.Fam

open import Uniform.IR

-- formation and introduction rules

module _ {D : Set1}{c : UF 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 : Uni D){Z : Fam D} ->
     (P : ind Z -> Set a) -> ⟦ c ⟧Uni Z -> Set a
IH ι P _ = Lift ⊤
IH (σ c A) P (x , a) = IH c P x
IH {D = D} (δ c A) {Z} P (x , h)
   = Σ[ y ∈ (IH c P x) ] ((a : A (⟦ c ⟧Info Z x)) -> P (h a))

mapIH : ∀ {a}{D : Set1}(c : Uni D){Z : Fam D} ->
        (P : ind Z -> Set a) -> (g : (x : ind Z) -> P x) ->
        (x : ⟦ c ⟧Uni Z) -> IH c P x
mapIH ι P g _ = lift tt
mapIH (σ c A) P g (x , a) = mapIH c P g x
mapIH (δ c A) P g (x , h) = (mapIH c P g x , g ∘ h)

module _ {D : Set1}{c : UF 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)