Re: [HoTT] A small observation on cumulativity and the failure of initiality

[Matt Oliveri <atm...@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 2940 bytes --]

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 <shu...@sandiego.edu 
> <javascript:>> 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 
> > <str...@mathematik.tu-darmstadt.de <javascript:>> 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
>

[-- Attachment #1.2: Type: text/html, Size: 3745 bytes --]