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 
> <javascript:>> wrote: 
> > 
> > On Oct 13, 2017, at 11:50 AM, Michael Shulman <shu...@sandiego.edu 
> <javascript:>> wrote: 
> > 
> > On Thu, Oct 12, 2017 at 5:09 PM, Steve Awodey <stev...@gmail.com 
> <javascript:>> 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.
>