The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Here's a start: a function to compute the type of a [Tn].  I have a 
suspicion that your actual [Tn] values are not too hard to define, 
guided by this type family.

Inductive telescope : Type :=
| tNil : telescope
| tCons : forall A, (A -> telescope) -> telescope.

Fixpoint telescopeOut (t : telescope) : Type :=
  match t with
    | tNil => Type
    | tCons A t' => forall x : A, telescopeOut (t' x)
  end.

Fixpoint telescopeApp (t : telescope) : telescopeOut t -> telescope :=
  match t with
    | tNil => fun to => tCons to (fun _ => tNil)
    | tCons A t' => fun to => tCons A (fun x => telescopeApp (t' x) (to x))
  end.

Fixpoint funcType (t : telescope) : telescopeOut t -> Type :=
  match t with
    | tNil => option
    | tCons A t' => fun to => forall x : A, funcType (t' x) (to x)
  end.

Fixpoint bindTypes (n : nat) (index : telescope) : Type :=
  match n with
    | O => forall A : telescopeOut index, funcType index A -> 
telescopeOut index
    | S n' => forall A : telescopeOut index, bindTypes n' (telescopeApp 
index A)
  end.

Definition type (n : nat) := bindTypes n tNil.


Paolo Herms wrote:
> Hello,
> any ideas of how to generalise this sequence, ie. define Tn?
>
> Definition T0
>    (A: Type)
>    (f: option (A))
>    :=
>    { x : (A) | f  = Some x }.
>
> Definition T1
>    (A: Type)
>    (B: forall (a:A), Type)
>    (f: forall (a:A), option (B a))
>    (a:A) :=
>    { x : (B a) | f a  = Some x }.
>
> Definition T2
>    (A: Type)
>    (B: forall (a:A), Type)
>    (C: forall (a:A) (b: B a), Type)
>    (f: forall (a:A) (b: B a), option (C a b))
>    (a:A) (b: B a) :=
>    { x : (C a b) | f a b  = Some x }.
>
> Definition T3
>    (A: Type)
>    (B: forall (a:A), Type)
>    (C: forall (a:A) (b: B a), Type)
>    (D: forall (a:A) (b: B a) (c: C a b), Type)
>    (f: forall (a:A) (b: B a) (c: C a b), option (D a b c))
>    (a:A) (b: B a) (c: C a b) :=
>    { x : (D a b c) | f a b c  = Some x }.
>
> Thanks in advance,