Maybe there are more ways to formulate initiality than anyone realized.

On Friday, October 13, 2017 at 12:23:37 PM UTC-4, Michael Shulman wrote:

To my understanding, there are two different essentially-algebraic
theories involved: type theory (or more precisely, its derivations) is
essentially by its definition the initial object in one of them, but
the one we're interested in (the appropriate sort of category) is a
different theory with different operations.  For instance, in a
category we have composition as a basic operation, but in type theory
composition is admissible rather than primitive.  So there is always
something to prove in relating the two, even when we know that both
are essentially-algebraic.

But my main point was that the essentially-algebraic theory to which
the syntax belongs consists of derivations rather than terms, so it
can be essentially-algebraic even if terms don't have unique types.

On Fri, Oct 13, 2017 at 9:17 AM, Steve Awodey <stev...@gmail.com> wrote:
>
> On Oct 13, 2017, at 11:50 AM, Michael Shulman <shu...@sandiego.edu> wrote:
>
> On Thu, Oct 12, 2017 at 5:09 PM, Steve Awodey <stev...@gmail.com> wrote:
>
> in order to have an (essentially) algebraic notion of type theory, which
> will then automatically have initial algebras, etc., one should have the
> typing of terms be an operation, so that every term has a unique type. In
> particular, your (R1) violates this. Cumulativity is a practical convenience
> that can be added to the system by some syntactic conventions, but the real
> system should have unique typing of terms.