module DS.DSPi where

open import Prelude.Basic
open import Prelude.Equality
open import Prelude.Fam

------------ A two-level presentation of DS with π ----------

-- names inspired by two-level presentation in DS 1999 paper

data SPπ (D : Set₁) : Set₁ where
   nil : SPπ D
   σ : (A : Set) -> (A -> SPπ D) -> SPπ D
   δ : (A : Set) -> ((A -> D) -> SPπ D) -> SPπ D
   π : (A : Set) -> (A -> SPπ D) -> SPπ D

Arg : {D : Set₁} → SPπ D → Set₁
Arg nil = Lift ⊤
Arg (σ A f) = Σ[ x ∈ A ] Arg (f x)
Arg {D} (δ A F) = Σ[ g ∈ (A -> D) ] Arg (F g)
Arg (π A f) = (x : A) -> Arg (f x)

DSπ : (D E : Set₁) → Set₁
DSπ D E = Σ[ c ∈ SPπ D ] (Arg c → E)

-- Decoding

arg : {D : Set1} -> SPπ D -> Fam D -> Set
arg nil Z = ⊤
arg (σ A f) Z = Σ[ x ∈ A ] arg (f x) Z
arg (δ A F) Z@(U , T) = Σ[ g ∈ (A -> U) ] arg (F (T ∘ g)) Z
arg (π A f) Z = (x : A) -> arg (f x) Z

mapSP : {D : Set1} -> (c : SPπ D) -> (Z : Fam D) -> arg c Z -> Arg c
mapSP nil Z tt = lift tt
mapSP (σ A f) Z (a , x) = a , mapSP (f a) Z x
mapSP (δ A F) Z@(U , T) (g , x) = T ∘ g , mapSP (F (T ∘ g)) Z x
mapSP (π A f) Z g = λ a → mapSP (f a) Z (g a)

-- putting it together

ds : {D E : Set1} -> DSπ D E -> Fam D -> Fam E
ds (c , α) Z = arg c Z , α ∘ mapSP c Z

ds₀ : {D E : Set1} -> DSπ D E -> Fam D -> Set
ds₀ c Z = ind (ds c Z)

ds₁ : {D E : Set1} -> (c : DSπ D E) -> (Z : Fam D) -> ds₀ c Z -> E
ds₁ c Z = fib (ds c Z)


------------ Functoriality ----------------------------------

-- DSπ D _ is functorial

DSπ-map : {D E E' : Set₁} → (E -> E') -> DSπ D E -> DSπ D E'
DSπ-map f (c , α) = (c , (f ∘ α))

-- DSπ _ E is opfunctorial

SP-opmap : {D D' : Set₁} -> (D -> D') -> SPπ D'  -> SPπ D
SP-opmap h nil = nil
SP-opmap h (σ A f) = σ A (λ a → SP-opmap h (f a))
SP-opmap h (δ A F) = δ A (λ g → SP-opmap h (F (h ∘ g)))
SP-opmap h (π A f) = π A (λ a → SP-opmap h (f a))

Arg-opmap : {D D' : Set₁} -> (h : D -> D') -> (c : SPπ D') ->
            Arg (SP-opmap h c) -> Arg c
Arg-opmap h nil x = x
Arg-opmap h (σ A f) (a , x) = a , Arg-opmap h (f a) x
Arg-opmap h (δ A F) (g , x) = (h ∘ g) , Arg-opmap h (F (h ∘ g)) x
Arg-opmap h (π A f) g a = Arg-opmap h (f a) (g a)

DSπ-opmap : {D D' E : Set₁} -> (D -> D') -> DSπ D' E  -> DSπ D E
DSπ-opmap h (c , α) = SP-opmap h c , α ∘ Arg-opmap h c

-- however, DSπ does not seem monadic

------------ One-level Dybjer-Setzer codes with π -----------

data DS+π (D : Set1) : (E : Set1) -> Set2 where
   ι : ∀ {E} → E →  DS+π D E
   σ : ∀ {E} → (A : Set) → (A → DS+π D E) → DS+π D E
   δ : ∀ {E} → (A : Set) → ((A → D) → DS+π D E) → DS+π D E
   π : ∀ {E} → (A : Set) → (A → DS+π D E) → DS+π D (A -> E)

⟦_⟧₀ : {D E : Set1} -> DS+π D E -> Fam D -> Set
⟦ ι e ⟧₀ X = ⊤
⟦ σ A f ⟧₀ X = Σ[ a ∈ A ] ⟦ f a ⟧₀ X
⟦ δ A F ⟧₀ (U , T) = Σ[ g ∈ (A -> U) ] ⟦ F (T ∘ g) ⟧₀ (U , T)
⟦ π A f ⟧₀ X = (a : A) -> ⟦ f a ⟧₀ X

⟦_⟧₁ : {D E : Set1} -> (c : DS+π D E) -> (Z : Fam D) -> ⟦ c ⟧₀ Z -> E
⟦ ι e ⟧₁ X _ = e
⟦ σ A f ⟧₁ X (a , x) = ⟦ f a ⟧₁ X x
⟦ δ A F ⟧₁ Z@(U , T) (g , x) = ⟦ F (T ∘ g) ⟧₁ Z x
⟦ π A f ⟧₁ X g a = ⟦ f a ⟧₁ X (g a)

⟦_⟧ : {D E : Set1} -> DS+π D E -> Fam D -> Fam E
⟦ c ⟧ X = ⟦ c ⟧₀ X , ⟦ c ⟧₁ X

{-
-- DS+π D does not seem to be functorial
DS+π-map : {D E E' : Set₁} -> (E -> E') -> DS+π D E  -> DS+π D E'
DS+π-map h (ι e) = ι (h e)
DS+π-map h (σ A f) = σ A (λ a → DS+π-map h (f a))
DS+π-map h (δ A F) = δ A (λ g → DS+π-map h (F g))
DS+π-map {D} {E} {E'} h (π {E''} A f) = ?
-}

------------ Initiality rules -------------------------------

-- (because of the translation DS+π -> DSπ below, this also gives rules
-- for DS+π)

------ formation and introduction rules -----

mutual

  {-# NO_POSITIVITY_CHECK #-}
  data U {D : Set1} (c : DSπ D D) : Set where
    intro : ds₀ c (U c , T c) -> U c

  {-# TERMINATING #-}
  T : {D : Set1} (c : DSπ D D) -> U c -> D
  T c (intro x) = ds₁ c (U c , T c) x

------ elimination rules --------------------

IH : ∀ {a}{D : Set1}(c : SPπ D){Z : Fam D} ->
     (P : ind Z -> Set a) -> arg c Z -> Set a
IH nil P x = Lift ⊤
IH (σ A f) P (a , x) = IH (f a) P x
IH (δ A F) P (g , x) = ((a : A) -> P (g a)) × IH (F _) P x
IH (π A f) P g = (a : A) -> IH (f a) P (g a)

mapIH : ∀ {a}{D : Set1}(c : SPπ D){Z : Fam D} ->
        (P : ind Z -> Set a) -> (h : (x : ind Z) -> P x) ->
        (x : arg c Z) -> IH c P x
mapIH nil P h x = lift x
mapIH (σ A f) P h (a , x) = mapIH (f a) P h x
mapIH (δ A F) P h (g , x) = h ∘ g , mapIH (F _) P h x
mapIH (π A f) P h g = λ a → mapIH (f a) P h (g a)

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

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

------------ Inititiality from elim -------------------------

rec : ∀ {D : Set1}(c : DSπ D D) -> {Z : Fam D} -> (f : ds c Z Fam⇒ Z) ->
      (U c , T c) Fam⇒ Z
rec {D} (c , α) {Z} f = proj₁ ∘ mediate , proj₂ ∘ mediate
  where
    open _Fam⇒_
    -- motive of the elimination
    E : ∀ {D}{c : DSπ D D}{Z : Fam D} -> U c -> Set₁
    E {D} {c} {Z} u = Σ[ u' ∈ ind Z ] T c u ≡ fib Z u'

    -- for this motive, Σ (arg c' (U c , T c)) (IH c' E) is arg c' Z
    lemma0 : ∀ {D} → (c' : SPπ D){c : DSπ D D}{Z : Fam D} ->
            (x : arg c' (U c , T c)) -> IH c' E x -> arg c' Z
    lemma0 nil x y = x
    lemma0 (σ A f) (a , x) y = a , lemma0 (f a) x y
    lemma0 (δ A F) {Z = Z} (g , x) (h , y)
      = proj₁ ∘ h , subst (λ z → arg (F z) Z)
                          (ext (λ a → proj₂ (h a)) )
                          (lemma0 (F _) x y)
    lemma0 (π A f) g h = λ a → lemma0 (f a) (g a) (h a)

    lemma1 : {D : Set1}(c' : SPπ D){c : DSπ D D}{Z : Fam D} ->
             (x : arg c' (U c , T c))(y : IH c' (E {D} {c} {Z}) x) ->
             mapSP c' (U c , T c) x ≡ mapSP c' Z (lemma0 c' x y)
    lemma1 nil x y = refl
    lemma1 (σ A f) (a , x) y = Σ-≡ refl (lemma1 (f a) x y)
    lemma1 {D} (δ A F) {c} {Z} (g , x) (h , y)
      = Σ-≡ (ext (λ a → proj₂ (h a)))
            (trans (cong (subst (Arg ∘ F) (ext (proj₂ ∘ h)))
                         (lemma1 (F _) x y))
                   (subst-natural (mapSP (F _) Z) (ext (proj₂ ∘ h))))
    lemma1 (π A f) g h = ext (λ a → lemma1 (f a) (g a) (h a))

    mediate = elim E (λ x y → indmor f (lemma0 c x y) ,
                              trans (cong α (lemma1 c x y))
                                    (indmor= f (lemma0 c x y)))

-- We need to define the action of ds c on morphism to state that the
-- diagram commutes. Then prove uniqueness by proving for any
-- candidate mediating morphism g that (ds c)(g) = (ds c)(rec c' k) by
-- using the elimination rule with motive E(u) = [g u = rec c k u],
-- together with induction on c. Hence for any x : arg c, we have
--
--   g (intro x) = k (ds c)(g)(x)
--               = k (ds (rec c' k)(x))
--               = rec c' k (intro x)
--
-- so that g = rec c' k by the elimination principle.

------------ Translation from DS+pi to DSπ ------------------

DS+πtoSPπ : {D E : Set₁} -> DS+π D E -> SPπ D
DS+πtoSPπ (ι e) = nil
DS+πtoSPπ (σ A f) = σ A (λ a → DS+πtoSPπ (f a))
DS+πtoSPπ (δ A F) = δ A (λ g → DS+πtoSPπ (F g))
DS+πtoSPπ (π A f) = π A (λ a → DS+πtoSPπ (f a))

DS+πtoArg : {D E : Set₁} -> (c : DS+π D E) -> Arg (DS+πtoSPπ c) -> E
DS+πtoArg (ι e) _ = e
DS+πtoArg (σ A f) (a , x) = DS+πtoArg (f a) x
DS+πtoArg (δ A F) (g , x) = DS+πtoArg (F g) x
DS+πtoArg (π A f) g a = DS+πtoArg (f a) (g a)

DS+πtoDSπ : {D E : Set₁} → DS+π D E → DSπ D E
DS+πtoDSπ c = (DS+πtoSPπ c , DS+πtoArg c)

{-
-- other direction does not seem possible, again because of index issues
DSπtoDS+π : {D E : Set₁} → DSπ D E → DS+π D E
DSπtoDS+π (c , α) = DSπtoDS+π' c α
  where DSπtoDS+π' : ∀ {D E} → (c : SPπ D)(α : Arg c -> E) -> DS+π D E
        DSπtoDS+π' nil α = ι (α _)
        DSπtoDS+π' (σ A f) α = σ A (λ a → DSπtoDS+π' (f a) (λ x → α (a , x)))
        DSπtoDS+π' (δ A F) α = δ A (λ g → DSπtoDS+π' (F g) (λ x → α (g , x)))
        DSπtoDS+π' (π A f) α = ?
-}