descriptions.txt

Desc : *
End : Desc
Arg : (A : *) -> (A -> Desc) -> Desc
Rec : (A : *) -> Desc -> Desc

interp : Desc -> * -> *
interp End X = U
interp (Arg A f) X = (x : A) ** interp (f x)
interp (Rec A d) X = (A -> X) ** interp d

Data : Desc -> *
Con : (d : Desc) -> interp d (Data d) -> Data d

ind :
  (d : Desc)
  -> (P : Data d -> *)
  -> (
    (y : interp d (Data d))
    -> All d (Data d) P y
    -> P (Con d y)
  )
  -> (x : Data d)
  -> P x
ind d P i (Con _ c) = i c (all d (Data d) P (id d P i) c)

E3 = (b : Bool) ** elimB {\_. *} Unit Bool b
E3i0 = (False, ())
E3i1 = (True, False)
E3i2 = (True, True)

elimE3 : (P : E3 -> *) -> P E3i0 -> P E3i1 -> P E3i2 -> (e : E3) -> P e
  = \P p0 p1 p2 e. elimB (\b. P (b, e.snd)) p0 (elimB (\b. P (True, b)) p1 p2 x.snd) x.fst

All : (d : Desc) -> (X : *) -> (P : X -> *) -> (xs : interp d X) -> *
All End X P () = U
All (Arg A f) X P (x, y) = All (f x) X P y
All (Rec A d) X P (f, y) = ((x : A) -> P (f x)) ** All d X P y

all : (d : Desc) -> (X : *) -> (P : X -> *) -> ((x : X) -> P x) -> (xs : interp d X) -> All d X P xs
all End X P p () = ()
all (Arg A f) X P p (x, y) = all (f x) X P p y
all (Rec A d) X P p (f, y) = (\(h : A). p (f h), all d X P p y)

Desc = Data DescD
DescD = Arg E3 \e. elimE3 (\_. Desc) End (Arg * \A. Rec A End) (Arg * \_. Rec U End) e
End = ((False, ()), ())
Arg A f = ((True, False), A, f)
Rec A d = ((True, True), A, d)

-- indexed

IDesc : * -> *
IEnd : I -> IDesc I
IArg : (A : *) -> (A -> IDesc I) -> IDesc I
IFOArg : * -> IDesc I -> IDesc I
IRec : I -> IDesc I -> IDesc I
IHRec : (A : *) -> (A -> I) -> IDesc I -> IDesc I

elimIDesc :
  (I : *)
  -> (P : IDesc I -> *)
  -> ((i : I) -> P (IEnd i))
  -> ((A : *) -> (f : A -> IDesc I) -> ((a : A) -> P (f a)) -> P (IArg A f))
  -> ((A : *) -> (d : IDesc I) -> P d -> P (IFOArg A d))
  -> ((i : I) -> (d : IDesc I) -> P d -> P (IRec i d))
  -> ((A : *) -> (f : A -> I) -> (d : IDesc I) -> P d -> P (IHRec A f d))
  -> (d : IDesc I)
  -> P d

interpI : (I : *) -> IDesc I -> (I -> *) -> I -> *

AllI : (I : *) -> (d : IDesc I) -> (X : I -> *) -> (P : (i : I) -> X i -> *) -> (i : I) -> (xs : interpI I d X i) -> *
allI : (I : *) -> (d : IDesc I) -> (X : I -> *) -> (P : (i : I) -> X i -> *) -> ((i : I) -> (x : X i) -> P i x) -> (i : I) -> (xs : interpI I d X i) -> All I d X P i xs

IData : (I : *) -> IDesc I -> I -> *
ICon : (I : *) -> (d : IDesc I) -> (i : I) -> interpI I d (IData I d) i -> IData I d i
indI :
  (I : *)
  -> (d : IDesc I)
  -> (P : (i : I) -> IData I d i -> *)
  -> (
    (i : I)
    -> (y : interpI I d (IData I d) i)
    -> AllI I d (IData I d) P i y
    -> P i (ICon I d i y)
  )
  -> (i : I)
  -> (x : IData I d i)
  -> P i x