Hi Mike,

This is all I can think of right now.  Are there others?  Are there
other choices we can make in the case of dependent type theory that
are not visible in this simple case?

I think there are at least the following categories:

Typing can be:
  I. intrinsic (only well-typed terms)
  II. extrinsic (preterms and typing relations).
Conversion can be given:
  1. by equality
  2. by an inductive relation
  3. not given, if we only have normal forms in the syntax (hereditary substitution)
Substitution can be:
  A. explicit (substitution is a constructor)
  B. implicit (it is defined recursively)

Your variants are categorised as below:

1 I,1,A
2 I,2,A
3 I,1,B
4 I,2,B
5 II,2,B
6 I,3,B
7 II,3,B

In the extrinsic case, I can think about the following additional choices:
 - Conversion and typing can be merged into a PER
 - use universes a la Russel or Tarski (in the Russel case, types and terms are identified)
 - you can have paranoid/relaxed variants of constructors (do you have Pi A B or Pi Gamma A B)
 - do you have conversion for contexts or not

In the above simple case of unary type theory with products, it should
be easy to show that all these definitions construct the initial
category with products.  (There should be some generating/axiomatic
types and terms too, to make the result nontrivial, but I've left them
out for brevity.)  My main question is, where do things become hard in
the case of dependent type theory?

It seems to me that the main difference between (1) and (2), and
between (3) and (4), is convenience; is that right?  Type theory has
no infinitary constructors, so there shouldn't be axiom-of-choice
issues with descending algebraic operations to a quotient; it's just
that the bookkeeping involved in dealing with setoids everywhere
becomes unmanageable in the case of DTT.  Right?  

Thorsten said that (1) in the case of dependent type theory is
tautologically the initial CwF, which seems eminently plausible.  I
don't think this solves the "initiality conjecture", but where is the
sticking point?  Is it between (1) and (3), or between (3) and (5)?

I think the hard part is between (3) and (5). However I haven't seen a definition of  (3) for type theory, e.g. CwF+Pi. It is very intricate, you have to prove substitution laws mutually with substitution, but you also shouldn't depend on the proofs etc.

There is a nice presentation of Streicher's initiality proof using the extrinsic, PER encoding in http://www.cse.chalmers.se/~peterd/papers/Lmcs-2016.pdf

Cheers,
Ambrus