From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Sun, 15 Oct 2017 14:00:10 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <37664950-3045-4570-af39-5f44bfc13a1b@googlegroups.com> In-Reply-To: References: <7ACEB87C-CF6E-4ACC-A803-2E44D7D0374A@gmail.com> <489BE14C-B343-49D1-AB51-19CD54B04761@gmail.com> <20171015074530.GA29437@mathematik.tu-darmstadt.de> <20171015135740.GA7845@mathematik.tu-darmstadt.de> Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_22649_1709158298.1508101210472" ------=_Part_22649_1709158298.1508101210472 Content-Type: multipart/alternative; boundary="----=_Part_22650_251001343.1508101210472" ------=_Part_22650_251001343.1508101210472 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit In order to assign meanings to derivations, one would have to define derivations. Technically, to assign meanings to derivable terms, one would only need to define derivability. All information needed to pick the right meaning would then need to be included in the terms. This might explain the disagreement over whether unique typing is necessary. In the middle, you could assign meanings to derivable judgments... Given the usual raw-terms-then-derivations approach, interpreting derivations is the most flexible. Gabirel Scherer brought up functor semantics of refinement type systems, which seems to be studying the general situation, with a category of derivation meanings and a category of term meanings, and a functor from the former to the latter. With intrinsically typed syntax--what Thorsten is talking about--there is no separation between terms and derivations in the first place. This is a style of syntax for type systems where--as a design constraint--all "relevant" information is included in the terms. Mike, I'm surprised that you favor interpreting derivations. For a categorical semantics, there is only one "level" of meaning. (Not two, like with a functor.) So I figured you would find it more elegant to stick to systems where the meaning can be assigned to derivable terms. Even when this sort of system is not directly amenable to implementation, it provides an interface to separate syntactic and semantic concerns. On Sunday, October 15, 2017 at 12:00:36 PM UTC-4, Michael Shulman wrote: > > I mean, it seems to me kind of like the difference between proving a > type A is contractible by > > Sigma(a:A) Pi(x:A) (x=a) > > and by > > A x Pi(x y:A) (x=y) > > i.e. not much. But maybe I am missing something? > > On Sun, Oct 15, 2017 at 7:53 AM, Michael Shulman > wrote: > > I'm not saying to do anything different mathematically, just to > > *think* about "using a partial interpretation function on prejudgments > > and showing that all derivable judgments get a meaning" as *being a > > way of* "assigning meanings to derivations and showing that distinct > > derivations of the same judgment get the same meaning". > > > > On Sun, Oct 15, 2017 at 6:57 AM, Thomas Streicher > > > wrote: > >>> > When writing my thesis in the second half of the 80s I found this > too > >>> > difficult and instead used an a priori partial interpretation > >>> > function assigning meaning to prejudgements. It was then part of the > >>> > correctness theorem that all derivable judgements get assigned a > meaning. > >>> > >>> Couldn't one consider the latter to be a way of doing the former? > >> > >> In principle yes but it is very laborious. First of all you have to > >> formalize derivations and do a double induction on them which I don't > >> know how to to perform. > >> > >> Thomas > ------=_Part_22650_251001343.1508101210472 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
In order to assign meanings to derivations, one would have= to define derivations. Technically, to assign meanings to derivable terms,= one would only need to define derivability. All information needed to pick= the right meaning would then need to be included in the terms. This might = explain the disagreement over whether unique typing is necessary. In the mi= ddle, you could assign meanings to derivable judgments...

Given the = usual raw-terms-then-derivations approach, interpreting derivations is the = most flexible. Gabirel Scherer brought up functor semantics of refinement t= ype systems, which seems to be studying the general situation, with a categ= ory of derivation meanings and a category of term meanings, and a functor f= rom the former to the latter.

With intrinsically typed syntax--what = Thorsten is talking about--there is no separation between terms and derivat= ions in the first place. This is a style of syntax for type systems where--= as a design constraint--all "relevant" information is included in= the terms.

Mike, I'm surprised that you favor interpreting deri= vations. For a categorical semantics, there is only one "level" o= f meaning. (Not two, like with a functor.) So I figured you would find it m= ore elegant to stick to systems where the meaning can be assigned to deriva= ble terms. Even when this sort of system is not directly amenable to implem= entation, it provides an interface to separate syntactic and semantic conce= rns.

On Sunday, October 15, 2017 at 12:00:36 PM UTC-4, Michael Shulm= an wrote:
I mean, it seems to m= e kind of like the difference between proving a
type A is contractible by

Sigma(a:A) Pi(x:A) (x=3Da)

and by

A x Pi(x y:A) (x=3Dy)

i.e. not much. =C2=A0But maybe I am missing something?

On Sun, Oct 15, 2017 at 7:53 AM, Michael Shulman <shu...@sandiego.edu= > wrote:
> I'm not saying to do anything different mathematically, just t= o
> *think* about "using a partial interpretation function on pre= judgments
> and showing that all derivable judgments get a meaning" as *b= eing a
> way of* "assigning meanings to derivations and showing that d= istinct
> derivations of the same judgment get the same meaning".
>
> On Sun, Oct 15, 2017 at 6:57 AM, Thomas Streicher
> <stre...@mathematik.tu-darmstadt.de> wrote:
>>> > When writing my thesis in the second half of the 80s = I found this too
>>> > difficult and instead used an a priori partial interp= retation
>>> > function assigning meaning to prejudgements. It was t= hen part of the
>>> > correctness theorem that all derivable judgements get= assigned a meaning.
>>>
>>> Couldn't one consider the latter to be a way of doing = the former?
>>
>> In principle yes but it is very laborious. First of all you ha= ve to
>> formalize derivations and do a double induction on them which = I don't
>> know how to to perform.
>>
>> Thomas
------=_Part_22650_251001343.1508101210472-- ------=_Part_22649_1709158298.1508101210472--