From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Sun, 15 Oct 2017 13:06:33 -0700 (PDT)
From: Matt Oliveri <atm...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <cb7a27ff-7c06-4b04-8e4e-a10622fb0936@googlegroups.com>
In-Reply-To: <CAOvivQy9HZykAErxd9UkV3LA9WnJchM9cWbat3jdh3cRtLKQ0Q@mail.gmail.com>
References: <F2106ADB-D78F-4228-B0A9-DBC6EC69E96A@princeton.edu> <7ACEB87C-CF6E-4ACC-A803-2E44D7D0374A@gmail.com>
 <CAOvivQy9HZykAErxd9UkV3LA9WnJchM9cWbat3jdh3cRtLKQ0Q@mail.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_22675_1943378934.1508097993357"

------=_Part_22675_1943378934.1508097993357
Content-Type: multipart/alternative; 
	boundary="----=_Part_22676_217404633.1508097993357"

------=_Part_22676_217404633.1508097993357
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 7bit

On Friday, October 13, 2017 at 11:50:40 AM UTC-4, Michael Shulman wrote:
>
> In an ideal world, a judgment x:A |- t:B 
> would have at most one derivation, so that we could induct on 
> derivations and still consider the syntactic model to be built out of 
> terms rather than derivations.
>

I think this can practically always be arranged. But it's not clear that it 
actually makes things easier. So I think you might be confused about when 
and why the interpreter would actually look at derivations.

------=_Part_22676_217404633.1508097993357
Content-Type: text/html; charset=utf-8
Content-Transfer-Encoding: 7bit

<div dir="ltr">On Friday, October 13, 2017 at 11:50:40 AM UTC-4, Michael Shulman wrote:<blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">In an ideal world, a judgment x:A |- t:B
<br>would have at most one derivation, so that we could induct on
<br>derivations and still consider the syntactic model to be built out of
<br>terms rather than derivations.<br></blockquote><div><br>I think this can practically always be arranged. But it&#39;s not clear that it actually makes things easier. So I think you might be confused about when and why the interpreter would actually look at derivations.<br></div></div>
------=_Part_22676_217404633.1508097993357--

------=_Part_22675_1943378934.1508097993357--