A small observation on cumulativity and the failure of initiality

[Dimitris Tsementzis]

Dear all,

Let’s say a type theory TT is initial if its term model C_TT is initial among TT-models, where TT-models are models of the categorical semantics of type theory (e.g. CwFs/C-systems etc.) with enough extra structure to model the rules of TT.

Then we have the following, building on an example of Voevodsky’s.

OBSERVATION. Any type theory which contains the following rules (admissible or otherwise) 

Γ |- T Type
————————  (C)
Γ |- B(T) Type

Γ |- t : T
————————  (R1)
Γ |- t : B(T)

Γ |- t : T
————————  (R2)
Γ |- p(t) : B(T)

together with axioms that there is a type T0 in any context and a term t0 : T0 in any context, is not initial. 

PROOF SKETCH. Let TT be such a type theory. Consider the type theory TT* which replaces (R1) with the rule

Γ |- t : T
————————  (R1*)
Γ |- q(t) : B(T)

i.e. the rule which adds an “annotation” to a term t from T that becomes a term of B(T). Then the category of TT-models is isomorphic (in fact, equal) to the category of TT*-models and in particular the term models C_TT and C_TT* are both TT-models. But there are two distinct TT-model homomorphisms from C_TT to C_TT*, one which sends p(t0) to pq(t0) and one which sends p(t0) to qp(t0) (where p(t0) is regarded as an element of Tm_{C_TT} (empty, B(B(T0))), i.e. of the set of terms of B(B(T0)) in the empty context as they are interpreted in the term model C_TT). 

COROLLARY. Any (non-trivial) type theory with a “cumulativity" rule for universes, i.e. a rule of the form

Γ |- A : U0
————————  (U-cumul)
Γ |- A : U1 

is not initial. In particular, the type theory in the HoTT book is not initial (because of (U-cumul)), and two-level type theory 2LTT as presented here is not initial (because of the rule (FIB-PRE)).

The moral of this small observation, if correct, is not of course that type theories with the guilty rules cannot be made initial by appropriate modifications to either the categorical semantics or the syntax, but rather that a bit of care might be required for this task. One modification would be to define their categorical semantics to be such that certain identities hold that are not generally included in the definitions of CwF/C-system/…-gadgets (e.g. that the inclusion operation on universes is idempotent). Another modification would be to add annotations (by replacing (R1) with (R1*) as above) and extra definitional equalities ensuring that annotations commute with type constructors. 

But without some such explicit modification, I think that the claim that e.g. Book HoTT or 2LTT is initial cannot be considered obvious, or even entirely correct.

Best,

Dimitris

PS: Has something like the above regarding cumulativity rules has been observed before — if so can someone provide a relevant reference?

[Michael Shulman]

On Thu, Oct 12, 2017 at 11:43 AM, Dimitris Tsementzis
<dtse...@princeton.edu> wrote:
> But there are two distinct TT-model homomorphisms
> from C_TT to C_TT*, one which sends p(t0) to pq(t0) and one which sends
> p(t0) to qp(t0) (where p(t0) is regarded as an element of Tm_{C_TT} (empty,
> B(B(T0))), i.e. of the set of terms of B(B(T0)) in the empty context as they
> are interpreted in the term model C_TT).

I don't know how to interpret this. What is T0? What is t0? If
t0:T0 then p(t0) : B(T0), so it seems that it can't be sent to qp(t0)
or pq(t0) which belong to B(B(T0)).

> COROLLARY. Any (non-trivial) type theory with a “cumulativity" rule for
> universes, i.e. a rule of the form
>
> Γ |- A : U0
> ———————— (U-cumul)
> Γ |- A : U1
>
> is not initial.

How does this yield an instance of the previous claim? What is B? What is p?

[Steve Awodey]

in order to have an (essentially) algebraic notion of type theory, which will then automatically have initial algebras, etc., one should have the typing of terms be an operation, so that every term has a unique type. In particular, your (R1) violates this. Cumulativity is a practical convenience that can be added to the system by some syntactic conventions, but the real system should have unique typing of terms.

Steve

--
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.

[Alexander Altman]

How does outright explicit subtyping play into this?  E.g., if you had a type theory with judgemental subtyping, not just judgemental equality, and one of the subtyping rules given was that each universe is a subtype of the next, would that still violate the conditions needed for initiality?

Steve

To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.

[Dimitris Tsementzis]

What is T0?  What is t0?

A primitive type expression (e.g. Nat) and a primitive term expression (e.g. 0). This just ensures that there is at least something in the type theory for the rules to be applied to.

If t0:T0 then p(t0) : B(T0), so it seems that it can't be sent to qp(t0)
or pq(t0) which belong to B(B(T0)).

p(t0) is regarded as a term of (the interpretation of) B(B(T0)) by an application of the (interpretation of the) rule (R)

How does this yield an instance of the previous claim?  What is B?  What is p?

With TT=book HoTT take T0=U_0, B(T)=U_1 (which also means B(B(T))=U_1), t0=1 (singleton type) and take p(t) == t -> t.

There are then two distinct homomorphisms from C_TT to C_TT*, one which sends 1->1 to q(1->1) and one which sends it to q(1)->q(1).

Dimitris

[Peter LeFanu Lumsdaine]

On Thu, Oct 12, 2017 at 8:43 PM, Dimitris Tsementzis <dtse...@princeton.edu> wrote:

Dear all,

Let’s say a type theory TT is initial if its term model C_TT is initial among TT-models, where TT-models are models of the categorical semantics of type theory (e.g. CwFs/C-systems etc.) with enough extra structure to model the rules of TT.

I like the examples, but I would give a different analysis of what they tell us.

The definition of “initial” presupposes that we have already defined what “TT-models” means — i.e. what the categorical semantics should be.  There is as yet no proposed general definition of this (as far as I know).

Heuristically, there’s certainly a large class of type theories where we understand what the categorical semantics are, and all clearly agree.  But rules like un-annotated cumulativity are *not* in this class.  It’s not clear what should correspond to un-annotated cumulativity, as a rule in CwA’s (or CwF’s, C-systems, etc).  A certain operation on terms?  An operation, plus the condition that it’s mono?  An assumption that terms of one type are literally a subset of terms of the other?  Some of these will make initiality clearly false; others may make it true but very non-obviously so (that is, more non-obviously than usual).

So I don’t think we can say “These theories aren’t initial.” — but more like “We’re not sure what the correct initiality statement is for these theories, and some versions one might try are false.”  But I definitely agree that they show 

>  the claim that e.g. Book HoTT or 2LTT is initial cannot be considered obvious

–p.

[Thomas Streicher]

unnotated cumulativity just means that we syntactically omit the
inclusions of U_n into U_{n+1} but semantically they are there
and have to be inserted when interpreting syntax

that's similar to universes `a la Russell which are just a shorthand
for universes `a la Tarski

but what is true is that there are syntaxes where terms don't have
unique types, but those always consider terms together with a type

but generally in CS and logic one distinguishes between typing `a la
Church and `a la Curry, the first is used in ML-like type theories,
the latter when typing terms of out of an untyped collection of
preterms

Thomas

On Fri, Oct 13, 2017 at 10:03:06AM +0200, Peter LeFanu Lumsdaine wrote:
> On Thu, Oct 12, 2017 at 8:43 PM, Dimitris Tsementzis <dtse...@princeton.edu
> > wrote:
>
> > Dear all,
> >

> > Let???s say a type theory TT is *initial* if its term model C_TT is initial

> > among TT-models, where TT-models are models of the categorical semantics of
> > type theory (e.g. CwFs/C-systems etc.) with enough extra structure to model
> > the rules of TT.
> >
>
> I like the examples, but I would give a different analysis of what they
> tell us.
>

> The definition of ???initial??? presupposes that we have already defined what
> ???TT-models??? means ??? i.e. what the categorical semantics should be. There

> is as yet no proposed general definition of this (as far as I know).
>

> Heuristically, there???s certainly a large class of type theories where we

> understand what the categorical semantics are, and all clearly agree. But

> rules like un-annotated cumulativity are *not* in this class. It???s not

> clear what should correspond to un-annotated cumulativity, as a rule in

> CwA???s (or CwF???s, C-systems, etc). A certain operation on terms? An
> operation, plus the condition that it???s mono? An assumption that terms of

> one type are literally a subset of terms of the other? Some of these will
> make initiality clearly false; others may make it true but very
> non-obviously so (that is, more non-obviously than usual).
>

> So I don???t think we can say ???These theories aren???t initial.??? ??? but more
> like ???We???re not sure what the correct initiality statement is for these
> theories, and some versions one might try are false.??? But I definitely

> agree that they show
>
> > the claim that e.g. Book HoTT or 2LTT is initial cannot be considered
> obvious
>

> ???p.
>
>
>
> Then we have the following, building on an example of Voevodsky???s.
> >
>
>
>
>
> > *OBSERVATION*. Any type theory which contains the following rules
> > (admissible or otherwise)
> >
> > ?? |- T *Type*
> > ???????????????????????? (C)
> > ?? |- B(T) *Type*
> >
> > ?? |- t : T
> > ???????????????????????? (R1)
> > ?? |- t : B(T)
> >
> > ?? |- t : T
> > ???????????????????????? (R2)
> > ?? |- p(t) : B(T)

> >
> > together with axioms that there is a type T0 in any context and a term t0
> > : T0 in any context, is not initial.
> >

> > *PROOF SKETCH.* Let TT be such a type theory. Consider the type theory

> > TT* which replaces (R1) with the rule
> >

> > ?? |- t : T
> > ???????????????????????? (R1*)
> > ?? |- q(t) : B(T)
> >
> > i.e. the rule which adds an ???annotation??? to a term t from T that becomes a

> > term of B(T). Then the category of TT-models is isomorphic (in fact, equal)
> > to the category of TT*-models and in particular the term models C_TT and
> > C_TT* are both TT-models. But there are two distinct TT-model homomorphisms
> > from C_TT to C_TT*, one which sends p(t0) to pq(t0) and one which sends
> > p(t0) to qp(t0) (where p(t0) is regarded as an element of Tm_{C_TT} (empty,
> > B(B(T0))), i.e. of the set of terms of B(B(T0)) in the empty context as
> > they are interpreted in the term model C_TT).
> >

> > *COROLLARY. *Any (non-trivial) type theory with a ???cumulativity" rule for

> > universes, i.e. a rule of the form
> >

> > ?? |- A : U0
> > ???????????????????????? (U-cumul)
> > ?? |- A : U1

> >
> > is not initial. In particular, the type theory in the HoTT book is not
> > initial (because of (U-cumul)), and two-level type theory 2LTT as presented

> > here <https://arxiv.org/abs/1705.03307> is not initial (because of the

> > rule (FIB-PRE)).
> >
> > The moral of this small observation, if correct, is not of course that
> > type theories with the guilty rules cannot be made initial by appropriate
> > modifications to either the categorical semantics or the syntax, but rather
> > that a bit of care might be required for this task. One modification would
> > be to define their categorical semantics to be such that certain identities
> > hold that are not generally included in the definitions of

> > CwF/C-system/???-gadgets (e.g. that the inclusion operation on universes is

> > idempotent). Another modification would be to add annotations (by replacing
> > (R1) with (R1*) as above) and extra definitional equalities ensuring that
> > annotations commute with type constructors.
> >
> > But without some such explicit modification, I think that the claim that
> > e.g. Book HoTT or 2LTT is initial cannot be considered obvious, or even
> > entirely correct.
> >
> > Best,
> >
> > Dimitris
> >
> > PS: Has something like the above regarding cumulativity rules has been

> > observed before ??? if so can someone provide a relevant reference?
> >
> >
> >
> >
> >
>

[Robin Adams]

On Thursday, 12 October 2017 20:43:01 UTC+2, Dimitris Tsementzis wrote:

But there are two distinct TT-model homomorphisms from C_TT to C_TT*, one which sends p(t0) to pq(t0) and one which sends p(t0) to qp(t0) (where p(t0) is regarded as an element of Tm_{C_TT} (empty, B(B(T0))), i.e. of the set of terms of B(B(T0)) in the empty context as they are interpreted in the term model C_TT). 

There seems to be a gap in the proof here.  In a term model we quotient out by judgemental equality (correct me if this is wrong), so this step does not give a contradiction: rather, we conclude |- qp(t0) = pq(t0) : B(B(T0))

I would expect this equality to hold in the examples you have in mind.  If T = Type_0, B(T) = Type_1, and p(t) = t -> t, then the equality is q(t -> t) = q(t) -> q(t).  This holds if TT* includes the rule

G |- A : Type_0           G |- B : Type_0
-------------------------------------------------------
G |- q(A -> B) = q(A) -> q(B) : Type_1

which I would expect you need in order for the category of TT-models to be isomorphic to the category of TT*-models.  So I suggest you also check the proof of this isomorphism in more detail.

--
Robin

[Michael Shulman]

On Thu, Oct 12, 2017 at 9:30 PM, Dimitris Tsementzis
<dtse...@princeton.edu> wrote:
> With TT=book HoTT take T0=U_0, B(T)=U_1 (which also means B(B(T))=U_1), t0=1
> (singleton type) and take p(t) == t -> t.

If you mean B(T) = U_1 for all types T, then you can't derive (R1),
since for instance if T = Nat then you don't get 0 : U_1. Also your
example p(t) == t -> t doesn't make sense unless T is a universe. You
seem to be confusing rules about arbitrary types T with rules about
specific types like T0=U_0.

[Michael Shulman]

On Thu, Oct 12, 2017 at 5:09 PM, Steve Awodey <steve...@gmail.com> wrote:
> in order to have an (essentially) algebraic notion of type theory, which
> will then automatically have initial algebras, etc., one should have the
> typing of terms be an operation, so that every term has a unique type. In
> particular, your (R1) violates this. Cumulativity is a practical convenience
> that can be added to the system by some syntactic conventions, but the real
> system should have unique typing of terms.

I'm not convinced of that. When we define the syntactic model, a
morphism from A to B (say) is defined to be a term x:A |- t:B, where
the types A and B are given. So it's not clear that it matters
whether the same syntactic object t can also be typed as belonging to
some other type. I thought that the fundamental structure that we
induct over to prove initiality is the *derivation* of a typing
judgment, which includes the type that the term belongs to: two
derivations of x:A |- t:B and x:A |- t:C will necessarily be different
if B and C are different. 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. If not, then we need a separate step
of showing that different derivations of the same judgment yield the
same interpretation; but still, it's not clear to me that the
simultaneous derivability of x:A |- t:C is fatal.

Moreover, I'm not an expert in this, but my understanding is that type
theorists often think of typing as having two "modes": type checking,
in which t and B are both given and a derivation of t:B is to be
found, and type synthesis or inference, in which t is given and B has
to be found along with a derivation of t:B. Which mode you are in at
which point in an algorithm depends on the structure of t and B. This
is not irrelevant to the question of initiality, since this sort of
"bidirectional type checking" can also be encoded in the judgmental
structure.

Mike

[Steve Awodey]

On Oct 13, 2017, at 11:50 AM, Michael Shulman <shu...@sandiego.edu> wrote:

On Thu, Oct 12, 2017 at 5:09 PM, Steve Awodey <steve...@gmail.com> wrote:

in order to have an (essentially) algebraic notion of type theory, which
will then automatically have initial algebras, etc., one should have the
typing of terms be an operation, so that every term has a unique type. In
particular, your (R1) violates this. Cumulativity is a practical convenience
that can be added to the system by some syntactic conventions, but the real
system should have unique typing of terms.

I'm not convinced of that.  When we define the syntactic model, a
morphism from A to B (say) is defined to be a term x:A |- t:B, where
the types A and B are given.  So it's not clear that it matters
whether the same syntactic object t can also be typed as belonging to
some other type.  I thought that the fundamental structure that we
induct over to prove initiality is the *derivation* of a typing
judgment, which includes the type that the term belongs to: two
derivations of x:A |- t:B and x:A |- t:C will necessarily be different
if B and C are different.  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.  If not, then we need a separate step
of showing that different derivations of the same judgment yield the
same interpretation; but still, it's not clear to me that the
simultaneous derivability of x:A |- t:C is fatal.

well, good luck with that : - )

I’m just saying that if you want to represent type theory in an essentially algebraic form — so that you automatically know you have free algebras, finitely-presented ones, products, sheaves of algebras, etc. — then typing of terms should be an operation.

sure, it may be that there are other ways to get the syntactic category to be initial w/resp. to some other notion of morphisms, but the algebraic approach is how it’s done for other categorical logics, like topos, CCC, coherent category, etc.  I think Peter Dybjer has also shown explicitly that this works for CwFs, too.

Steve

[Michael Shulman]

To my understanding, there are two different essentially-algebraic
theories involved: type theory (or more precisely, its derivations) is
essentially by its definition the initial object in one of them, but
the one we're interested in (the appropriate sort of category) is a
different theory with different operations. For instance, in a
category we have composition as a basic operation, but in type theory
composition is admissible rather than primitive. So there is always
something to prove in relating the two, even when we know that both
are essentially-algebraic.

But my main point was that the essentially-algebraic theory to which
the syntax belongs consists of derivations rather than terms, so it
can be essentially-algebraic even if terms don't have unique types.

[Matt Oliveri]

Maybe there are more ways to formulate initiality than anyone realized.

[Dimitris Tsementzis]

> You
> seem to be confusing rules about arbitrary types T with rules about
> specific types like T0=U_0.

Fair enough, I was conflating them. In the statement of my OBSERVATION I allow for versions of (R1) where T is possibly a fixed type (expression).

Indeed, as you point out, in the book HoTT example the version of (R1) is one where T is a specific type expression U_0, otherwise (R1) is not admissible.

In any case, hopefully the point I was trying to make with the (purposefully contrived) rules in the OBSERVATION is somewhat clear.

Dimitris

[Dimitris Tsementzis]

So I don’t think we can say “These theories aren’t initial.” — but more like “We’re not sure what the correct initiality statement is for these theories, and some versions one might try are false.” 

Yes, fair enough. This is a much better way to put the point and I agree.

(As Robin Adams’ message also shows, for example, there are perfectly reasonable alternative definitions of the notion of a TT-model such that the categories of TT-models and TT*-models are not isomorphic, in which case the argument would not go through.)

Dimitris

[Thorsten Altenkirch]

Thank you, Thomas!

Any form of subtyping is syntactic sugar for coercion functions we want to
omit for the sake of readability. They are defined by their translation -
I don't think it makes sense to assign any independent semantics to
notational conventions.

My view of Type Theory is that we always consider typed objects hence we
shouldn't really talk about the preterms. In our recent work on intrinsic
syntax of Type Theory we present a typed syntax that never refers to
preterms. In this framework theories with coercions cannot be expressed
and the syntax is the initial algebra of the corresponding notion of
algebras.

Thorsten

On 13/10/2017, 09:10, "homotopyt...@googlegroups.com on behalf of
Thomas Streicher" <homotopyt...@googlegroups.com on behalf of

>--
>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.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it.

Please do not use, copy or disclose the information contained in this
message or in any attachment. Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.

[Andrej Bauer]

> In our recent work on intrinsic
> syntax of Type Theory we present a typed syntax that never refers to
> preterms. In this framework theories with coercions cannot be expressed
> and the syntax is the initial algebra of the corresponding notion of
> algebras.

This is quite cool, but I'd just like to point out that there are
levels of abstraction, some of which cannot be ignored.

At a very banal level, we need to know how to convert concrete syntax
into abstract syntax.

At a slightly less banal level, we have to admit that preterms
(expressed as abstract syntax) are unavoidable. An important aspect of
type theory revolves around making sure that the thing written down
makes sense. The "thing written down" is a preterm (something that
survived parsing but has yet to be type checked).

There is also the question of breaking the vicious circle: we express
type theory inside type theory, but where did the original type theory
come from? I think it is quite reasonable to take the possition that
type theory is primitive, but it is also equally reasonable to take
the position that one should analyse how type theory arises from a
more concrete setup, for instance, there is some value in knowing that
the syntactic models based on concrete syntax are initial for type
theory.

With kind regards,

Andrej

[Thomas Streicher]

Andrej,

you are right in the sense that the free model of a certain type
theory T is not trivially isomorphic the syntax modulo. The late
Voevodsky suggested this to be an important problem and Peter
Lumsdaine has worked on it for some time.
It feels a bit like a non-mathematical problem in the sense of being
more organizational or CS like. But maybe one should think about ways
to introduce variables in a systematic way for making categorical
combinator based syntax more palatable. There is more hope this way
get something than strating from raw syntax and how to tame it
semantically.

Thomas

[Alexander Altman]

Forwarding this reply to the list, since it wasn’t sent there initially.

Begin forwarded message:

From: Dimitris Tsementzis <dtse...@princeton.edu>

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

Date: October 13, 2017 at 4:53:35 PM CDT

To: Alexander Altman <alexand...@me.com>

E.g., if you had a type theory with judgemental subtyping, not just judgemental equality, and one of the subtyping rules given was that each universe is a subtype of the next, would that still violate the conditions needed for initiality?

As far as I can understand the terminology yes I believe the observation would still apply even with sub-typing rules of this kind.

Dimitris

On Oct 12, 2017, at 20:44, Alexander Altman <alexand...@me.com> wrote:

How does outright explicit subtyping play into this?  E.g., if you had a type theory with judgemental subtyping, not just judgemental equality, and one of the subtyping rules given was that each universe is a subtype of the next, would that still violate the conditions needed for initiality?

On Thursday, October 12, 2017 at 7:09:06 PM UTC-5, Steve Awodey wrote:

in order to have an (essentially) algebraic notion of type theory, which will then automatically have initial algebras, etc., one should have the typing of terms be an operation, so that every term has a unique type. In particular, your (R1) violates this. Cumulativity is a practical convenience that can be added to the system by some syntactic conventions, but the real system should have unique typing of terms.

Steve

On Oct 12, 2017, at 2:43 PM, Dimitris Tsementzis <dtse...@princeton.edu> wrote:

Dear all,

Let’s say a type theory TT is initial if its term model C_TT is initial among TT-models, where TT-models are models of the categorical semantics of type theory (e.g. CwFs/C-systems etc.) with enough extra structure to model the rules of TT.

Then we have the following, building on an example of Voevodsky’s.

OBSERVATION. Any type theory which contains the following rules (admissible or otherwise) 

Γ |- T Type
————————  (C)
Γ |- B(T) Type

Γ |- t : T
————————  (R1)
Γ |- t : B(T)

Γ |- t : T
————————  (R2)

Γ |- p(t) : B(T)

together with axioms that there is a type T0 in any context and a term t0 : T0 in any context, is not initial. 

PROOF SKETCH. Let TT be such a type theory. Consider the type theory TT* which replaces (R1) with the rule

Γ |- t : T
————————  (R1*)
Γ |- q(t) : B(T)

i.e. the rule which adds an “annotation” to a term t from T that becomes a term of B(T). Then the category of TT-models is isomorphic (in fact, equal) to the category of TT*-models and in particular the term models C_TT and C_TT* are both TT-models. But there are two distinct TT-model homomorphisms from C_TT to C_TT*, one which sends p(t0) to pq(t0) and one which sends p(t0) to qp(t0) (where p(t0) is regarded as an element of Tm_{C_TT} (empty, B(B(T0))), i.e. of the set of terms of B(B(T0)) in the empty context as they are interpreted in the term model C_TT). 

COROLLARY. Any (non-trivial) type theory with a “cumulativity" rule for universes, i.e. a rule of the form

Γ |- A : U0
————————  (U-cumul)

Γ |- A : U1 

is not initial. In particular, the type theory in the HoTT book is not initial (because of (U-cumul)), and two-level type theory 2LTT as presented here is not initial (because of the rule (FIB-PRE)).

The moral of this small observation, if correct, is not of course that type theories with the guilty rules cannot be made initial by appropriate modifications to either the categorical semantics or the syntax, but rather that a bit of care might be required for this task. One modification would be to define their categorical semantics to be such that certain identities hold that are not generally included in the definitions of CwF/C-system/…-gadgets (e.g. that the inclusion operation on universes is idempotent). Another modification would be to add annotations (by replacing (R1) with (R1*) as above) and extra definitional equalities ensuring that annotations commute with type constructors. 

But without some such explicit modification, I think that the claim that e.g. Book HoTT or 2LTT is initial cannot be considered obvious, or even entirely correct.

Best,

Dimitris

PS: Has something like the above regarding cumulativity rules has been observed before — if so can someone provide a relevant reference?

-- 
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 HomotopyTypeTheory+unsub...@googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

[Erik Palmgren]

A simplistic suggestion for introducing names in contextual categories
is to replace the assignment of length to contexts, by an assignment
of a string of distinct symbols (variable name). The challenge is then
to find a stripping/simplification function that could make the
combinators more readable. Some preliminary explorations of this
idea is in

http://staff.math.su.se/palmgren/Named_variables_in_cwfs_v02.pdf

________________________________________
Från: homotopyt...@googlegroups.com <homotopyt...@googlegroups.com> för Thomas Streicher <stre...@mathematik.tu-darmstadt.de>
Skickat: den 14 oktober 2017 11:52
Till: Andrej Bauer
Kopia: Homotopy Type Theory; Univalent Mathematics
Ämne: Re: [HoTT] A small observation on cumulativity and the failure of initiality

Andrej,

Thomas

--

[Gabriel Scherer]

In type theory, we care about coherence: if a judgment has
several derivations, then those derivations should have the same
meaning (in the denotational semantics we have in mind). (This is
a different requirement from the requirement that the untyped
semantics of the term, if it exists, be compatible with the
semantics of the typed derivation, which is also interesting.)
This means that having a derivation system with rules that are
not reflected in the term syntax give you *more* information, in
a sense, about the designer's intent: stronger constraints on
what would be a valid semantics for the type system.
(I am no expert of categorical semantics, but I suppose one could
regain initiality by restricting the class of models, adding
strictness conditions that guarantee that the coherence property
holds in any model of the class.)

In "Functors are Type Refinement Systems", 2015, Paul-André
Melliès and Noam Zeilberger give a categorical presentation of
the relation between the fully-typed derivations (or Church-style
fully-typed terms) and untyped
terms (or uni-typed derivations). They also reformulate
a coherence result from Reynolds, about subtyping, in their
framework -- coherence is obtained by relating the meaning
of any derivation to the meaning of the untyped term.

Finally, if a type theory comes with strong enough computation
rules (or in general equivalences), then the coherence property
may be shown internally, by showing that any two derivations of
the same term reduce to (or are equivalent to) a canonical
derivation. Then I would suppose that the very natural
requirement that models should respect these
computation (or equivalence) rules suffices to avoid initiality
issues. This would even work for higher-dimensional notions of
coherence -- seeing the computation rules as 2-cells in the model
instead of equalities between morphisms.

[Thomas Streicher]

It is certainly tempting to assign meanings to derivations and then to
show that different derivations of the same judgement get assigned the
same meaning.
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.

Most people have gone this way at least when they took pains to write
down the interpretation function at all.

BTW the above allows one to show that assigning a meaning to derivations
just depends on the judgement: one jyust has to show that the meaning
assigned to a derivation of a judgement J coincides with the meaning
assigned to J beforehand.

Thomas

[Thierry Coquand]

 A quite detailed interpretation of type theory in set theory is presented

in the paper of Peter Aczel "On Relating Type Theories and Set Theories".

On can define directly the interpretation of lambda terms (provided that abstraction is

typed), and using set theoretic coding, one can use a global application operation

(so that the interpretation is total). One can then checked by induction on derivations

that all judgements are valid for this interpretation.

 Thierry

---

From: homotopyt...@googlegroups.com <homotopyt...@googlegroups.com> on behalf of Thomas Streicher <stre...@mathematik.tu-darmstadt.de>
Sent: Sunday, October 15, 2017 9:45:30 AM
To: Gabriel Scherer
Cc: Michael Shulman; Steve Awodey; Dimitris Tsementzis; Homotopy Type Theory
Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality

 

[Thomas Streicher]

> A quite detailed interpretation of type theory in set theory is presented
>
> in the paper of Peter Aczel "On Relating Type Theories and Set Theories".
>
> On can define directly the interpretation of lambda terms (provided that abstraction is
>
> typed), and using set theoretic coding, one can use a global application operation
>
> (so that the interpretation is total). One can then checked by induction on derivations
>
> that all judgements are valid for this interpretation.

Thanks, Thierry, for pointing this out. But Peter's method does not
extend to arbitrary split models of dependent type theory. What Peter
uses here intrinsically is that everything is a set since otherwise he
couldn't interpret type theoretic quantification.
My interpretation got partial on pseudoexpressions since pseudoterms
can't be understood as pseudo-type-expressions.

I don't see how Peter's method extends to interpretation of
realizability or (pre)sheaf models of dependent type theories not to
speak of arbitrary contextual cats or other split categorical models
of dependent type theories.

Thomas

[Michael Shulman]

On Sun, Oct 15, 2017 at 12:45 AM, Thomas Streicher
<stre...@mathematik.tu-darmstadt.de> wrote:
> It is certainly tempting to assign meanings to derivations and then to
> show that different derivations of the same judgement get assigned the
> same meaning.
> 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?

> Most people have gone this way at least when they took pains to write
> down the interpretation function at all.
>
> BTW the above allows one to show that assigning a meaning to derivations
> just depends on the judgement: one jyust has to show that the meaning
> assigned to a derivation of a judgement J coincides with the meaning
> assigned to J beforehand.
>
> Thomas
>
>
>
>
>
>
>
>
>
>
>
>
>

[Thorsten Altenkirch]

On 14/10/2017, 10:37, "homotopyt...@googlegroups.com on behalf of
Andrej Bauer" <homotopyt...@googlegroups.com on behalf of

andrej...@andrej.com> wrote:

>> In our recent work on intrinsic
>> syntax of Type Theory we present a typed syntax that never refers to
>> preterms. In this framework theories with coercions cannot be expressed
>> and the syntax is the initial algebra of the corresponding notion of
>> algebras.
>
>This is quite cool, but I'd just like to point out that there are
>levels of abstraction, some of which cannot be ignored.
>
>At a very banal level, we need to know how to convert concrete syntax
>into abstract syntax.
>
>At a slightly less banal level, we have to admit that preterms
>(expressed as abstract syntax) are unavoidable. An important aspect of
>type theory revolves around making sure that the thing written down
>makes sense. The "thing written down" is a preterm (something that
>survived parsing but has yet to be type checked).

Indeed, but it isn't even preterms but strings we really see (or bits?).
The theorem that beta-reduction preserves matching brackets is mixing
levels of abstraction in bad way. As we are happy to reason about terms as
trees knowing that we can parse strings into trees, we should think about
intrinsic terms (what Thomas calls "derivations") knowing that by type
checking and scope checking we can convert trees into derivations.
Assigning meaning to purely syntactic entities is a confusing levels of
abstractions in the same way as the matching brackets theorem.

>
>There is also the question of breaking the vicious circle: we express
>type theory inside type theory, but where did the original type theory
>come from? I think it is quite reasonable to take the possition that
>type theory is primitive, but it is also equally reasonable to take
>the position that one should analyse how type theory arises from a
>more concrete setup, for instance, there is some value in knowing that
>the syntactic models based on concrete syntax are initial for type
>theory.

The original type theory is in our mind and we may use english or any
other natural language to express it and then we want to be more precise
and use the type theory in our minds to explain the type theory we
implement, which then in turn can be implemented. No vicious circle.

Thorsten


>
>With kind regards,
>
>Andrej

[Thomas Streicher]

> > 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

[Michael Shulman]

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".

[Michael Shulman]

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?

[Matt Oliveri]

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.

[Matt Oliveri]

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.

[Andrej Bauer]

> you are right in the sense that the free model of a certain type
> theory T is not trivially isomorphic the syntax modulo. The late
> Voevodsky suggested this to be an important problem and Peter
> Lumsdaine has worked on it for some time.

I absolutely agree with Vladimir's insisting that actually proving
good, robust, and general theorems about initiality of syntactic
models is not only important, but also an open problem. We have
*instances* of such theorems (with many thanks to you, Thomas), but no
general theory.

I would warn against repeating or spreading the opinion that such
general theorems either exist, or are somehow not worth proving, or
worse, that they are easy. And the reason for this is that I am
working with Peter on them, and it's really not as easy or as boring
as many would seem to presume.

> It feels a bit like a non-mathematical problem in the sense of being
> more organizational or CS like.

Call it what you like. Isn't all of logic organizational?

With kind regards,

Andrej

P.S. Why are we cross-posting everything between HoTT and Univalent
mathematics lists?

[Michael Shulman]

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. 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.

[Andrew Polonsky]

In the set-thoretic model -- which is the simplest, most "standard" model one can think of -- the universes are indeed cumulative, and "coherence" is just the observation that conversion (definitional equality) of raw terms is preserved by the interpretation function.

In categorical models, strict equality between interpreted objects is perhaps a more subtle concept.

Still, it would seem to be a natural requirement of *ANY* class or flavor of semantics, that expressions which are definitionally equal in the object language, are evaluated to entities which are again (judgmentally) equal on the meta-level.

This really amounts to nothing more than asking that the semantics in question actually validate the conversion rule -- one of the structural rules of the theory.

Best,

Andrew

[Thomas Streicher]

> 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".

You can assign meaning to derivations AND define a partial
interpretation function for prejudgements and then show by single
induction on derivations that the meaning assigned to a derivation
coincides with the meaning assigned to the judgement it derives.

So things can be reconciled though assigning meaning to derivations is
a bit of overkill...

Thomas

[Thorsten Altenkirch]

 

Sent from my iPhone

On 16 Oct 2017, at 06:31, Andrew Polonsky <andrew....@gmail.com> wrote:

In the set-thoretic model -- which is the simplest, most "standard" model one can think of -- the universes are indeed cumulative, and "coherence" is just the observation that conversion (definitional equality) of raw terms is preserved by the interpretation function.

 

Set theory is a form of a mathematical assembly language where you cannot hide anything. Equalities in the set theoretic translation of Type Theory are accidents of implementation choices. Making them the guideline for the design of Type Theory seems to to put the cart in front of the horse.

 

In categorical models, strict equality between interpreted objects is perhaps a more subtle concept.

 

Still, it would seem to be a natural requirement of *ANY* class or flavor of semantics, that expressions which are definitionally equal in the object language, are evaluated to entities which are again (judgmentally) equal on the meta-level.

 

This really amounts to nothing more than asking that the semantics in question actually validate the conversion rule -- one of the structural rules of the theory.

 

Best,

Andrew

On Sunday, October 15, 2017 at 11:26:22 AM UTC+2, Thomas Streicher wrote:

>  A quite detailed interpretation of type theory in set theory is presented
>
> in the paper of Peter Aczel "On Relating Type Theories and Set Theories".
>
> On can define directly the interpretation of lambda terms (provided that abstraction is
>
> typed), and using set theoretic coding, one can use a global application operation
>
> (so that the interpretation is total). One can then checked by induction on derivations
>
> that all judgements are valid for this interpretation.

Thanks, Thierry, for pointing this out. But Peter's method does not
extend to arbitrary split models of dependent type theory. What Peter
uses here intrinsically is that everything is a set since otherwise he
couldn't interpret type theoretic quantification.
My interpretation got partial on pseudoexpressions since pseudoterms
can't be understood as pseudo-type-expressions.

I don't see how Peter's method extends to interpretation of
realizability or (pre)sheaf models of dependent type theories not to
speak of arbitrary contextual cats or other split categorical models
of dependent type theories.

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.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.

[Thorsten Altenkirch]

Sent from my iPhone

On 16 Oct 2017, at 00:49, Andrej Bauer <andrej...@andrej.com> wrote:

The theorem that beta-reduction preserves matching brackets is  mixing

levels of abstraction in bad way. As we are happy to reason about terms as

trees knowing that we can parse strings into trees, we should think about

intrinsic terms (what Thomas calls "derivations") knowing that by type

checking and scope checking we can convert trees into derivations.

Assigning meaning to purely syntactic entities is a confusing levels of

abstractions in the same way as the matching brackets theorem.

I do not understand these remarks. Did I say somewhere that we should
worry about matching brackets in beta-reductions, or that we should do
semantics at the wrong level of abstraction?

 

Sorry if this was not very clear. I was trying to make an analogy. Some novice programmers seem to think that strings are the only data structure. From this point of view we may define beta reduction as an operation on strings and then prove that it preserves matching brackets.

 

I hope we all agree that this makes little sense. Instead beta reduction should be defined on trees or even better alpha-equivalence classes of trees. Analogously we should think of derivations and not preterms when studying the semantics of Type Theory.

[Andrew Polonsky]

Equalities in the set theoretic translation of Type Theory are accidents of implementation choices. Making them the guideline for the design of Type Theory seems to to put the cart in front of the horse.

No.

The fact that equalities corresponding to beta reduction, etc. are validated is not "an accident of implementation choices".

It is a consequences of the fact that standard type constructors (function space, products, ...) are interpreted by their native meaning in the meta-level.

For example, if the metatheory is again type theory, and interpretation is done by recursion over the universes of object types, reifying all type constructors by themselves (like in an inductive-recursive universe), then all conversions in the object language will again be valid in the metatheory, and coherence issues won't arise.

I suspect that (sufficiently split) categorical models could also be presented this way, but it might be less natural because equality of types would then have to refer to (actual) equality of objects.

Cheers,

Andrew

[Neel Krishnaswami]

On 16/10/17 06:09, 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. 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.

For this to be true, it seems like you would want to arrange that there
is at most one derivation of judgmental equality for any pair of terms.

What leads me to this reading is the idea that if there are multiple
possible derivations of judgemental equality (for instance, if
conversion contains the symmetry rule), then you have to prove a
coherence theorem, which is what you seemingly to want to avoid.

This doesn't seem *impossible*, but it does seem challenging. A
plausible line of attack:

1. Give bidirectional typing rules to ensure only beta-normal, eta-long
terms are typeable.
2. Hence, a conversion rule can be omitted, since all terms (including
types) are in normal form.
3. Prove a bunch of lemmas, eventually culminating in proofs of
(a) hereditary substitution and (b) identity expansion. (This
basically ends up making normalization part of the definition of
substitution.)

This seems plausible, since Harper and Pfenning worked it out in the
case of LF, but there are two outstanding issues, in order of
difficulty:

1. The addition of universes is an open problem. Basically the logical
strength of the theory goes up and the proof of Harper and Pfenning
needs to be redone. (They exploited the fact that LF doesn't have
large eliminations to do a recursion on the size of the type.)

I would be rather surprised if this couldn't be made to work, though.

2. The beta-eta theory of sum types (and naturals numbers) involves
commuting conversions.

This is a very complex problem, and I would want to know if the
desired initiality theorem could be proved without the commuting
conversions?

If memory serves, book HoTT assumes judgmental eta for pi and sigma,
but not for natural numbers? What is the desired relation between
judgmental equality and propositional equality at the natural number
type?

Best,
Neel

[Matt Oliveri]

Hi, Neelakantan.

I don't think the coherence problem of having multiple derivations of a judgment is a serious problem when working in a set-level theory. But I think Mike's planning ahead for what will generalize to initiality theorems internal to HoTT. He has talked about the possibility of using hereditary substitutions, and interpreting only normal forms. (Recently, actually: https://golem.ph.utexas.edu/category/2017/10/vladimir_voevodsky_19662017.html#c052824)

What's this business about commuting conversions? I don't think I've heard of that.

[Matt Oliveri]

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?

[Thorsten Altenkirch]

Just to clarify: by set theory we mean ZFC, not the set-level fragment of HoTT.

 

I am not sure what is in general the “native meaning” of type constructors. Ok, it is pretty clear for function types but not in general.

 

Choosing a clever encoding you could make products strictly monoidal, that is Ax(BxC) = (AxB)xC. Is this now the true equality or not?

 

Looking at inductive types you can have representations where F(mu F) = mu F or you choose that this is just an isomorphism. Either of them can be justified by set theoretic encodings which is no help in deciding which ones should hold.

 

Thorsten

 

From: <homotopyt...@googlegroups.com> on behalf of Andrew Polonsky <andrew....@gmail.com>
Date: Monday, 16 October 2017 at 11:42
To: Homotopy Type Theory <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality

 

Equalities in the set theoretic translation of Type Theory are accidents of implementation choices. Making them the guideline for the design of Type Theory seems to to put the cart in front of the horse.

--

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.

[Michael Shulman]

On Mon, Oct 16, 2017 at 5:30 AM, Neel Krishnaswami
<neelakantan....@gmail.com> wrote:
> 1. Give bidirectional typing rules to ensure only beta-normal, eta-long
> terms are typeable.
> 2. Hence, a conversion rule can be omitted, since all terms (including
> types) are in normal form.
> 3. Prove a bunch of lemmas, eventually culminating in proofs of
> (a) hereditary substitution and (b) identity expansion. (This
> basically ends up making normalization part of the definition of
> substitution.)

Yes, that's what I'm proposing.

> 1. The addition of universes is an open problem. Basically the logical
> strength of the theory goes up and the proof of Harper and Pfenning
> needs to be redone. (They exploited the fact that LF doesn't have
> large eliminations to do a recursion on the size of the type.)
>
> I would be rather surprised if this couldn't be made to work, though.

Me too.

> 2. The beta-eta theory of sum types (and naturals numbers) involves
> commuting conversions.
>
> This is a very complex problem, and I would want to know if the
> desired initiality theorem could be proved without the commuting
> conversions?
>
> If memory serves, book HoTT assumes judgmental eta for pi and sigma,
> but not for natural numbers? What is the desired relation between
> judgmental equality and propositional equality at the natural number
> type?

Book HoTT (and HoTT in general) doesn't include any eta rules for
positive/inductive types.

[Michael Shulman]

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.

[Matt Oliveri]

I understand your argument as a good reason to consider intrinsic syntax as being more analogous to derivations than to preterms. But still, trying to consistently call all those things judgments and derivations, and having nothing syntactic called terms or types seems impractical. Like I said, one could have opinions about whether (the things I call) intrinsic terms are more like preterms or derivations, but my terminology recommendation is not dependent on that. The existing papers on intrinsic syntax always seem to call them terms, even when they point out that they're a lot like derivations.

I realized my terminology proposal didn't include anything convenient for the metalanguage types of intrinsic syntax objects. Normally, "judgments" would be OK, since that's what they correspond to. But for now I want to distinguish them easily from the extrinsic judgments, which involve preterms. I'll call them "classes". They are strongly-typed versions of the things often called "syntactic classes" or "syntactic categories" in CS. (Of course, calling them "categories" here would be super confusing.)

So now let's try out your opening sentence in my terminology:
[I would rather characterize intrinsic style by saying there are no *preterms*: all you have are classes and terms.]
That's not so bad, is it? I feel like what makes you want to reject the term "term" is that you want to emphasize that *preterms* are not involved at all.

Anyway, now I think I know what you meant before, about interpreting derivations. But I think it wasn't clear, because it sounded like you were talking about the usual extrinsic derivations.

[Matt Oliveri]

On Monday, October 16, 2017 at 11:01:13 AM UTC-4, Michael Shulman wrote:

On Mon, Oct 16, 2017 at 5:30 AM, Neel Krishnaswami
<neelakantan....@gmail.com> wrote:
> 1. The addition of universes is an open problem. Basically the logical
>    strength of the theory goes up and the proof of Harper and Pfenning
>    needs to be redone. (They exploited the fact that LF doesn't have
>    large eliminations to do a recursion on the size of the type.)
>
>    I would be rather surprised if this couldn't be made to work, though.

Me too.

I was thinking that where you'd really get in trouble is with impredicative quantifiers. From what I understand, hereditary substitutions are a variant of cut elimination, which can't directly handle impredicativity. But so far, HoTT has added impredicativity with an axiom, so maybe it'll work out somehow. Like HoTT's proof-theoretic strength would be impredicative, but its "coherence strength" would still be predicative in some weird sense. That would be a bit unnatural though, in my opinion.

[Michael Shulman]

I prefer my terminology (yes, I think inventing a new word "class" is so bad).
I don't actually reject "term", I use it to mean "derivation of a judgment
\Gamma \vdash A", and I use "type" to mean "derivation of a judgment
\Gamma \vdash type". That matches the extrinsic usage pretty closely
in practice.
I only phrased it as "there are no terms" to contrast with your "there
are no derivations".

But let's not spam everyone else on this list any more with
discussions about terminology.