open import DS.IR

module DS.InitialPleasingAgda {D : Set1}{c : DS D D} where

open import Prelude.Basic
open import Prelude.Fam

-- Formation and introduction rules

-- variant of ⟦_⟧₀ where the family has been split up into two arguments
-- to help Agda see that U below is strictly positive
⟦_⟧'₀ : {D E : Set1} -> DS D E -> (X : Set)(Y : X -> D) -> Set
⟦ ι e ⟧'₀ X Y = ⊤
⟦ σ A f ⟧'₀ X Y = Σ[ a ∈ A ] ⟦ f a ⟧'₀ X Y
⟦ δ A F ⟧'₀ X Y = Σ[ g ∈ (A -> X) ] ⟦ F (λ x → Y (g x)) ⟧'₀ X Y

mutual

  data U  : Set where
    intro : ⟦ c ⟧'₀ U T -> U

  T : U -> D
  T (intro x) = ⟦ c ⟧'₁ x

  -- variant of ⟦_⟧₁ specialised to this U and T to help Agda see that
  -- T above is terminating
  ⟦_⟧'₁ : (c' : DS D D) -> ⟦ c' ⟧'₀ U T  -> D
  ⟦ ι e ⟧'₁ _ = e
  ⟦ σ A f ⟧'₁ (a , x) = ⟦ f a ⟧'₁ x
  ⟦ δ A F ⟧'₁ (g , x) = ⟦ F (λ x → T (g x)) ⟧'₁ x

-- Elimination rules

IH : ∀ {a}{D E : Set1}(c : DS D E){X : Set}{Y : X -> D} ->
     (P : X -> Set a) -> ⟦ c ⟧'₀ X Y -> 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

mutual

  elim : ∀ {a}(P : U -> 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 step x)

  -- variant of mapIH specialised to U, T and elim to help Agda see
  -- that elim is terminating
  mapIH' : ∀ {a}(c' : DS D D) ->
          (P : U -> Set a) ->
          (step : (x : ⟦ c ⟧'₀ U T) -> IH c P x -> P (intro x)) ->
          (x : ⟦ c' ⟧'₀ U T) -> IH c' P x
  mapIH' (ι e) P step _ = lift tt
  mapIH' (σ A f) P step (a , x) = mapIH' (f a) P step x
  mapIH' (δ A F) P step (h , x)
    = ((λ x → elim P step (h x)), mapIH' (F _) P step x)