parameters.fv

IDescP : Set -> Set -> Set 1
IDescP P I = I -> IDesc (P + I)

IDescP:fork : (P I : Set) ->
              (P -> Set) ->
              P + I ->
              IDesc I
IDescP:fork P I X x =
  case x with { inl p. “K” (X p); inr i. “IId” i }

IDescP:code : (P I : Set) ->
              IDescP P I ->
              (P -> Set) ->
              I -> IDesc I
IDescP:code P I D X =
  λi. bind x <- D i in IDescP:fork P I X x

muP : (P I : Set) ->
      IDescP P I ->
      (P -> Set) ->
      I ->
      Set
muP P I D X = µI I (IDescP:code P I D X)

--------------------------------------------------------------------------------
algebra : (I : Set) -> (D : I -> IDesc I) -> Set 1
algebra I D =
  (A : I -> Set) ×
  (i : I) -> semI[D i, i. A i] -> A i

drop : (I : Set) ->
       (D : IDesc I) ->
       (A B : I -> Set) ->
       (x : semI[D, i. A i]) ->
       liftI[D, i. A i, i x. B i, x] ->
       semI[D, i. B i]
drop I D A B =
  elimID I
    (λD'. (x : semI[D', i. A i]) ->
          liftI[D', i. A i, i x. B i, x] ->
          semI[D', i. B i])
    (λi x a. a)
    (λX x u. x)
    (λD₁ D₂ drop₁ drop₂ x a.
      «drop₁ (fst x) (fst a), drop₂ (snd x) (snd a)»)
    (λX D drop x a. «fst x, drop (fst x) (snd x) a»)
    (λX D drop f a. λx. drop x (f x) (a x))
    D

cata : (I : Set) ->
       (D : I -> IDesc I) ->
       («A,k» : algebra I D) ->
       (i : I) -> µI I D i -> A i
cata I D «A,k» i x =
  eliminate x then i x φ.
    k i (drop I (D i) (µI I D) A x φ)

––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––
map : (P I : Set) ->
      (D : IDescP P I) ->
      (X Y : P -> Set) ->
      ((p : P) -> X p -> Y p) ->
      (i : I) -> muP P I D X i -> muP P I D Y i
map P I D X Y f =
  cata I (IDescP:code P I D X)
     « muP P I D Y
     , λi x. construct (mapI[D i, x. semI[IDescP:fork P I X x, i. muP P I D Y i]
                                , x. semI[IDescP:fork P I Y x, i. muP P I D Y i]
                                , λx. case x with { inl p. f p; inr i. λx. x }
                                , x])
     »

--------------------------------------------------------------------------------
– shouldn't expect the map laws to hold, due to functional extensionality problems.
– need a way of defining a sub-universe of descriptions that doesn't have “Π”

– would like to prove that (λx. case x with { inl p. λx. x; inr
– i. λx. x }) is the identity. Then if the appropriate thing held for
– mapI, we would have the right functorialty laws.

assume ext : (A : Set) ->
             (B : A -> Set) ->
             (f g : (a : A) -> B a) ->
             ((a : A) -> f a ≡ g a) ->
             f ≡ g

internal-id : (P I : Set) ->
              (D : IDescP P I) ->
              (X : P -> Set) ->
              (Y : I -> Set) ->
              (i : I) ->
              (x : semI[IDescP:code P I D X i, i. Y i]) ->
              x ≡ mapI[ D i
                      , x. semI[IDescP:fork P I X x, i. Y i]
                      , x. semI[IDescP:fork P I X x, i. Y i]
                      , λx. case x with { inl p. λx. x; inr i. λx. x }
                      , x]
internal-id P I D X Y i = ?
{-  elimID (P + I)
    (λD'. (x : semI[D', x. semI[IDescP:fork P I X x, i. Y i]]) ->
          x ≡ mapI[D'
                  , x. semI[IDescP:fork P I X x, i. Y i]
                  , x. semI[IDescP:fork P I X x, i. Y i]
                  , λx. case x with { inl p. λx. x; inr i. λx. x }
                  , x])
    (λd. case d with { inl _. λx. refl; inr _. λx. refl })
    (λA a. refl)
    (λD₁ D₂ ih₁ ih₂ «x₁,x₂». rewriteBy ih₁ x₁ then rewriteBy ih₂ x₂ then refl)
    (λA D ih «a,x». rewriteBy ih a x then refl)
    (λA D' ih f.
      ext A (λa. semI[D' a, x. semI[IDescP:fork P I X x, i. Y i]])
          f (λa. mapI[D' a
                     , x. semI[IDescP:fork P I X x, i. Y i]
                     , x. semI[IDescP:fork P I X x, i. Y i]
                     , λx. case x with { inl p. λx. x; inr i. λx. x }
                     , f a])
          (λa. ih a (f a)))
    (D i)-}

-- even with mapI being definitionally a functor, we'd still end up with
--    mapI[λi x. x, x] ≡ mapI[λd. case d of { inl _. λx. x; inr _. λx. x }, x]
-- as the goal, which we wouldn't be able to do anything with

– what happens if you try to prove that 
–  bind x <- D in “IId” x ≡ D, by induction on 'D'? probably still works, because it will just keep normalising.

map-id : (P I : Set) ->
         (D : IDescP P I) ->
         (X : P -> Set) ->
         (i : I) ->
         (x : muP P I D X i) ->
         (map P I D X X (λi x. x) i x) == x
map-id P I D X i x =
  eliminate x then i x φ. ?

--------------------------------------------------------------------------------
list:code : IDescP Unit Unit
list:code _ =
  “Σ” (Unit + Unit)
      (λc. case c with { inl _. “K” Unit
                       ; inr _. “IId” (inl ()) “×” “IId” (inr ()) })

list : Set -> Set
list A = muP Unit Unit list:code (λ_. A) ()

maplist : (A B : Set) -> (A -> B) -> list A -> list B
maplist A B f =
  map Unit Unit list:code (λ_. A) (λ_. B) (λ_. f) ()



;