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

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

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

On Monday, October 16, 2017 at 1:10:20 AM UTC-4, Michael Shulman wrote:
>
> What you call "intrinsically typed syntax" is what I favor.  I want 
> initiality theorems that are proven by a straightforward structural 
> induction over something that is inductively generated, and 
> derivations are the basic inductively generated object of a deductive 
> system.


I want to set up some terminology, which we should try to use consistently 
for this thread. (I mean Mike and me, but others could follow along too. It 
might be helpful.)

In the extrinsic style of syntax, which is the usual one, there are 
"preterms" and "derivations". To notate types, there are either separate 
"pretypes", or else pretypes are a subset of the preterms. The thing to the 
left of the turnstile is a "precontext".

In the intrinsic style of syntax, there are contexts, types, and terms. (In 
principle, you should be able to make types a subset of terms, but I 
haven't seen that, and it doesn't seem appropriate for categorical 
semantics.) There may also be other things defined mutually.

In the intrinsic style, there are no derivations. One could have opinions 
on whether intrinsic terms are more like preterms or typing derivations, 
but they aren't actually either of those.

Techniques like bidirectional type checking don't seem to apply to 
intrinsic syntax. You don't type check intrinsic syntax; it's intrinsically 
well-typed. I'm not sure there's even any analogue of bidirectional 
judgments for intrinsic syntax. Maybe you know one. I bring this up because 
you were talking about interpreting derivations of bidirectional typing. 
That sounds interesting, but it's totally not interpreting intrinsic syntax.

So you're saying you like intrinsic syntax, and how it lets you interpret 
with one structural induction. That makes sense. But that's not 
interpreting derivations. If you interpret derivations, then you also have 
preterms to worry about, since they are what appear in judgments.

It seems most natural to me to introduce terms as a 
> convenient 1-dimensional notation for derivations, and departing from 
> that is what causes all the problems.
>

What's a 1-dimensional notation?


> On Sun, Oct 15, 2017 at 2:00 PM, Matt Oliveri <atm...@gmail.com 
> <javascript:>> wrote: 
> > 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> 
> >> 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> 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: 6860 bytes --]