From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Fri, 13 Oct 2017 09:36:08 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <8dce09b8-a4d4-48e6-a6bb-85a45421c88f@googlegroups.com> In-Reply-To: References: <7ACEB87C-CF6E-4ACC-A803-2E44D7D0374A@gmail.com> <489BE14C-B343-49D1-AB51-19CD54B04761@gmail.com> Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_17853_729436441.1507912568561" ------=_Part_17853_729436441.1507912568561 Content-Type: multipart/alternative; boundary="----=_Part_17854_1885506006.1507912568561" ------=_Part_17854_1885506006.1507912568561 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit 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 > wrote: > > > > On Oct 13, 2017, at 11:50 AM, Michael Shulman > wrote: > > > > On Thu, Oct 12, 2017 at 5:09 PM, Steve Awodey > 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. > ------=_Part_17854_1885506006.1507912568561 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Maybe there are more ways to formulate initiality than any= one realized.

On Friday, October 13, 2017 at 12:23:37 PM UTC-4, Mich= ael Shulman wrote:
To my unders= tanding, 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. =C2=A0For instance, in a
category we have composition as a basic operation, but in type theory
composition is admissible rather than primitive. =C2=A0So there is alwa= ys
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 ha= ve the
> typing of terms be an operation, so that every term has a unique t= ype. In
> particular, your (R1) violates this. Cumulativity is a practical c= onvenience
> that can be added to the system by some syntactic conventions, but= the real
> system should have unique typing of terms.
------=_Part_17854_1885506006.1507912568561-- ------=_Part_17853_729436441.1507912568561--