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

[Michael Shulman <shu...@sandiego.edu>]

I would rather characterize intrinsic style by saying there are no
*terms*: all you have are judgments and derivations.  Look at an
inductive-inductive encoding: its meta-language types are the
object-language judgments, and its meta-language terms are the
object-language derivations.  Some of the judgment forms may be put
together out of a context (another judgment) and a type in that
context (a third judgment), but not all of them (e.g. not the judgment
for "is a context"); and you can also call a derivation a "term", but
that could be misleading.  In particular, this perspective makes it
more clear that there is a bidirectional version of intrinsic style:
the two "directions" become simply two different judgment forms, and
the derivations are inductively generated by the bidirectional
"typing" rules.

On Mon, Oct 16, 2017 at 6:45 AM, Matt Oliveri <atm...@gmail.com> wrote:
> 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> 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
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.