The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

defined. So this is still a fixpoint which uses structural recursion
on the structure of a type. Why would you be unhappy with that?

There are 2 reasons why I am not fully satisfied with your definitions.

1) You have defined non-dependent function types. Therefore,

     you were able define "which terms denote types" independently of

     "which terms are equal members of a given type" (for a theory like Nuprl)

      or "which terms are members of a given type" (for a theory like Coq).

     (In other words, you were able to define ty and ty_eq separately.)

     When defining dependent function types, I don't know of a way to define them

     separately. This is because for a term of the form (PI A v B) to denote a PI type,

     B[v\a1] and B[v\a2] have to be equal types for all a1 and a2 which are equal members of A.

     Even for a theory like Coq, one has to ensure in the above case that B[v\t] is a type for all t such that t is a member of A.

     In other words, the definition of typehood refers to the definition of equality/membership in types (and vice-versa).

2) I want to be able to prove type-preservation. With the definition in my email, type preservation was a direct consequence of the definitions

     of equalTypes and equalMembersInType.

    Can you somehow use your definitions to create another definition of a type system which satisfies type preservation?
    PI types might again be problematic.

You are right when you say "equality on PI_{x:A} B(x) is defined in terms of equality on A and equality on B, where these two equalities have been previously defined". Therefore, Stuart said these mutual definitions are "half-positive". In Agda, once can define these by using mutual  induction-recursion

where equalTypes is defined by induction and equalTermsInType is defined by structural recursion.

Thanks,

Abhishek