The Coq mailing list

[roconnor AT theorem.ca]

I don't understand why

Inductive Lambda : Set -> Set :=
 | var : forall A:Set, A -> Lambda A
 | app : forall A:Set, Lambda A -> Lambda A -> Lambda A.

is considered impredicative, but

Inductive Lambda (A:Set) : Set :=
 | var : A -> Lambda A
 | app : Lambda A -> Lambda A -> Lambda A.

is considered predicative.  The two types seem isomorphic to me.

I really want to define

Inductive Lambda : Set -> Set :=
 | var : forall A:Set, A -> Lambda A
 | app : forall A:Set, Lambda A -> Lambda A -> Lambda A
 | lambda : forall A:Set, Lambda (option A) -> Lambda A.

which is almost uniformly parametric polymorpic.  This definition strikes
me as just as safe as polymorphic lists.

I cannot fix this my changing Set to Type because then the statement of
the join function:

Definition joinStatement :=
   forall (T:Type)(l:Lambda (Lambda T)),(Lambda T).

causes a universe inconsistency.

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''