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

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

[Thorsten Altenkirch]

[-- Attachment #1: Type: text/plain, Size: 2102 bytes --]

Sent from my iPhone

On 16 Oct 2017, at 00:49, Andrej Bauer <andrej...@andrej.com<mailto: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.




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.


[-- Attachment #2: Type: text/html, Size: 4863 bytes --]

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

[Thorsten Altenkirch]

[-- Attachment #1: Type: text/plain, Size: 3514 bytes --]


Sent from my iPhone

On 16 Oct 2017, at 06:31, Andrew Polonsky <andrew....@gmail.com<mailto: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<mailto: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.


[-- Attachment #2: Type: text/html, Size: 6871 bytes --]

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

[Andrew Polonsky]

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


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

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

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

[Thorsten Altenkirch]

[-- Attachment #1: Type: text/plain, Size: 3042 bytes --]

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.

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


[-- Attachment #2: Type: text/html, Size: 7492 bytes --]

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

[Alexander Altman]

[-- Attachment #1: Type: text/plain, Size: 5690 bytes --]

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 <mailto: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 <http://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 <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?
>>> 
>>> 
>>> 
>>> 
>>> 
>>> -- 
>>> 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 <https://groups.google.com/d/optout>.
>> 
>> 
>> -- 
>> 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 <mailto:HomotopyTypeThe...@googlegroups.com>.
>> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.
> 


[-- Attachment #2: Type: text/html, Size: 15420 bytes --]

A small observation on cumulativity and the failure of initiality

[Dimitris Tsementzis]

[-- Attachment #1: Type: text/plain, Size: 2942 bytes --]

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





[-- Attachment #2: Type: text/html, Size: 4449 bytes --]

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

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

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

[Dimitris Tsementzis]

[-- Attachment #1: Type: text/plain, Size: 1815 bytes --]

> 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

> On Oct 12, 2017, at 18:31, Michael Shulman <shu...@sandiego.edu> wrote:
> 
> 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?


[-- Attachment #2: Type: text/html, Size: 3174 bytes --]

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

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

> 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
>
> On Oct 12, 2017, at 18:31, Michael Shulman <shu...@sandiego.edu> wrote:
>
> 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?
>
>

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

[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

> On Oct 13, 2017, at 11:41, Michael Shulman <shu...@sandiego.edu> wrote:
> 
> 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.
> 
>> 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
>> 
>> On Oct 12, 2017, at 18:31, Michael Shulman <shu...@sandiego.edu> wrote:
>> 
>> 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?
>> 
>> 

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

[Steve Awodey]

[-- Attachment #1: Type: text/plain, Size: 3978 bytes --]

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 <mailto: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 <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?
> 
> 
> 
> 
> 
> -- 
> 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 <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.


[-- Attachment #2: Type: text/html, Size: 6178 bytes --]

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

[Alexander Altman]

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

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 <dts...@princeton.edu 
> <javascript:>> 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 <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?
>
>
>
>
>
> -- 
> 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 <javascript:>.
> For more options, visit https://groups.google.com/d/optout.
>
>
>

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

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

[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
>
>
> 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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>
>
> --
> 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.

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

[Steve Awodey]

[-- Attachment #1: Type: text/plain, Size: 7223 bytes --]


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

> 
> 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
>> 
>> 
>> 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 HomotopyTypeThe...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>> 
>> 
>> --
>> 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.
> 
> -- 
> 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 <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.


[-- Attachment #2: Type: text/html, Size: 31641 bytes --]

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

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

On Fri, Oct 13, 2017 at 9:17 AM, Steve Awodey <steve...@gmail.com> wrote:
>
> 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
>
>
> 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
>
>
> 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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>
>
> --
> 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.
>
>
> --
> 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.
>
>
> --
> 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.

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

[Matt Oliveri]

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

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

On Friday, October 13, 2017 at 12:23:37 PM UTC-4, Michael Shulman wrote:
>
> 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. 
>
> On Fri, Oct 13, 2017 at 9:17 AM, Steve Awodey <stev...@gmail.com 
> <javascript:>> wrote: 
> > 
> > On Oct 13, 2017, at 11:50 AM, Michael Shulman <shu...@sandiego.edu 
> <javascript:>> wrote: 
> > 
> > On Thu, Oct 12, 2017 at 5:09 PM, Steve Awodey <stev...@gmail.com 
> <javascript:>> 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.
>

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

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

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

On Fri, Oct 13, 2017 at 6:23 PM, Michael Shulman <shu...@sandiego.edu> wrote:
> 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.
>
> On Fri, Oct 13, 2017 at 9:17 AM, Steve Awodey <steve...@gmail.com> wrote:
>>
>> 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
>>
>>
>> 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
>>
>>
>> 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 HomotopyTypeThe...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>>
>>
>> --
>> 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.
>>
>>
>> --
>> 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.
>>
>>
>> --
>> 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.
>
> --
> 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.

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

[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

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

[Thierry Coquand]

[-- Attachment #1: Type: text/plain, Size: 2020 bytes --]

 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

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













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

[-- Attachment #2: Type: text/html, Size: 3362 bytes --]

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

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

[Andrew Polonsky]

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

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


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 
>

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

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

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

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

[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

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

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

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

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

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

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

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

[Matt Oliveri]

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

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

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

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.

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

[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

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

[Matt Oliveri]

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

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.

On Monday, October 16, 2017 at 8:30:43 AM UTC-4, Neelakantan Krishnaswami 
wrote:
>
> 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 
>
>

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

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

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

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

[Matt Oliveri]

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

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 
> <neelaka...@gmail.com <javascript:>> 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.

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

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

[Matt Oliveri]

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

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

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

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.

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

[Matt Oliveri]

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

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.

On Monday, October 16, 2017 at 11:06:11 AM UTC-4, Michael Shulman wrote:
>
> 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 
> <javascript:>> 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
>

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

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

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

On Mon, Oct 16, 2017 at 9:20 AM, Matt Oliveri <atm...@gmail.com> wrote:
> 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.
>
> On Monday, October 16, 2017 at 11:06:11 AM UTC-4, Michael Shulman wrote:
>>
>> 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.

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

[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

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

[Matt Oliveri]

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

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.

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

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

[Peter LeFanu Lumsdaine]

[-- Attachment #1: Type: text/plain, Size: 4850 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 6709 bytes --]

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

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

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

[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
stre...@mathematik.tu-darmstadt.de> wrote:

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

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

[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

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

[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

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

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

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

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

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

[Dimitris Tsementzis]

[-- Attachment #1: Type: text/plain, Size: 5562 bytes --]

> 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



> On Oct 13, 2017, at 04:03, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> wrote:
> 
> On Thu, Oct 12, 2017 at 8:43 PM, Dimitris Tsementzis <dtse...@princeton.edu <mailto: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?
> 
> 
> 
> 
> 
> -- 
> 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 <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.


[-- Attachment #2: Type: text/html, Size: 10277 bytes --]