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

module DS.Initial where

open import Prelude.Basic
open import Prelude.Fam

open import DS.IR

-- Formation and introduction rules

module _ {D : Set1}{c : DS 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 E : Set1}(c : DS D E){Z : Fam D} ->
     (P : ind Z -> Set a) -> ⟦ c ⟧₀ Z -> Set a
IH (ι e) P _ = Lift ⊤
IH (σ A f) P (a , x) = IH (f a) P x
IH (δ A F) {X , Y} P (h , x) = ((x : A) -> P (h x)) × IH (F (Y ∘ h)) P x

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

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

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