Merged two lists of ways to introduce new kinds of types.

The material from the list in the section notes for chapter 1 has
been merged with the list in the section on function types, which
is Remark 1.5.1, and the list in the section notes is no longer
there.  The analogous list in A.2.4 is still there, but the two
lists refer to each other.

I've taken the opportunity to eliminate the section of A.2 devoted
to the eta rule for functions, which is now treated in A.2.4 and
named Pi-uniq.  The advantage is that function types display, in
section A.2.4, all 5 types of rules.

( 5273bcc8757942474cd184195a13f78ed37c5f6e#commitcomment-3338813 )