[HoTT] Question about the formal rules of cohesive homotopy type theory

[HoTT] Question about the formal rules of cohesive homotopy type theory

[Madeleine Birchfield]

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

In Mike Shulman's presentation of cohesive homotopy type theory in his 2018 
article Brouwer’s fixed-point theorem in real-cohesive homotopy type 
theory, he states in section 2 that "All the ordinary rules of type theory (
∏-types, ∑-types, =-types, W -types, HITs) are imported into our theory only 
in the world of cohesive variables." Does this also include the structural 
rules of type theory such as the substitution and weakening rules?

Madeleine Birchfield

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/96f15467-49c9-43cc-8868-40b1bdf2162dn%40googlegroups.com.

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

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Michael Shulman]

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

Substitution and weakening hold for all types with the restriction that
only crisp terms (i.e. those involving only crisp variables) can be
substituted for crisp variables.  This restriction is mentioned in the
beginning of section 2.

On Fri, Nov 11, 2022 at 3:14 PM Madeleine Birchfield <
madeleinebirchfield@gmail.com> wrote:

> In Mike Shulman's presentation of cohesive homotopy type theory in his
> 2018 article Brouwer’s fixed-point theorem in real-cohesive homotopy type
> theory, he states in section 2 that "All the ordinary rules of type
> theory (∏-types, ∑-types, =-types, W -types, HITs) are imported into our
> theory only in the world of cohesive variables." Does this also include
> the structural rules of type theory such as the substitution and weakening
> rules?
>
> Madeleine Birchfield
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/HomotopyTypeTheory/96f15467-49c9-43cc-8868-40b1bdf2162dn%40googlegroups.com
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/96f15467-49c9-43cc-8868-40b1bdf2162dn%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpymP9gVGU8oy-m-NKtS_8f7fgR5WRBoMaY3NUSRfPejFQ%40mail.gmail.com.

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

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[andrej.bauer]

>  Does this also include the structural rules of type theory such as the substitution and weakening rules?

I would just like to point out that substutition and weakening typically are not part of the rules. They are shown to be admissible. In this spirit, the question should have been: what is the precise version of substitution and weakening (which is a special case of substitution) that is admissible in cohesive type theory?

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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/D66F4584-A005-4F69-8E75-E976E0FF9957%40andrej.com.

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

['Thorsten Altenkirch' via Homotopy Type Theory]

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

That depends on what presentation of Type Theory you are using. Your remarks apply to the extrinsic approach from the last millennium. More recent presentation of Type Theory built in substitution and weakening and use an intrinsic approach which avoids talking about preterms you don’t really care about.

https://dl.acm.org/doi/10.1145/2837614.2837638

Cheers,
Thorsten

From: homotopytypetheory@googlegroups.com <homotopytypetheory@googlegroups.com> on behalf of andrej.bauer@andrej.com <andrej.bauer@andrej.com>
Date: Tuesday, 15 November 2022 at 22:39
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>
Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory
>  Does this also include the structural rules of type theory such as the substitution and weakening rules?

I would just like to point out that substutition and weakening typically are not part of the rules. They are shown to be admissible. In this spirit, the question should have been: what is the precise version of substitution and weakening (which is a special case of substitution) that is admissible in cohesive type theory?

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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/D66F4584-A005-4F69-8E75-E976E0FF9957%40andrej.com.



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 contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.




-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB786979CA94519BCC98EDD32FCD079%40PAXPR06MB7869.eurprd06.prod.outlook.com.

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

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Jon Sterling]

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

Indeed, I echo Thorsten's comment — to put it another way, even being 
able to tell whether these rules are derivable or only admissible is 
like knowing what an angel's favorite TV show is (in other words, a form 
of knowledge that cannot be applied toward anything by human beings). At 
least for structural type theory, there is nothing worth saying that 
cannot be phrased in a way that does not depend on whether structural 
rules are admissible or derivable. It may be that admissiblity of 
structural rules starts to play a role in substructural type theory, 
however, but this is not my area of expertise.

It is revealing that nobody has proposed a notion of **model** of type 
theory in which the admissible structural rules do not hold; this would 
be the necessary form taken by any evidence for the thesis that it is 
important for structural rules to not be derivable. Absent such a notion 
of model and evidence that it is at all compelling/useful, we would have 
to conclude that worrying about admissibility vs. derivability of 
structural rules in the official presentation of type theory is 
fundementally misguided.


On 16 Nov 2022, at 4:52, 'Thorsten Altenkirch' via Homotopy Type Theory 
wrote:

> That depends on what presentation of Type Theory you are using. Your 
> remarks apply to the extrinsic approach from the last millennium. More 
> recent presentation of Type Theory built in substitution and weakening 
> and use an intrinsic approach which avoids talking about preterms you 
> don’t really care about.
>
> https://dl.acm.org/doi/10.1145/2837614.2837638
>
> Cheers,
> Thorsten
>
> From: homotopytypetheory@googlegroups.com 
> <homotopytypetheory@googlegroups.com> on behalf of 
> andrej.bauer@andrej.com <andrej.bauer@andrej.com>
> Date: Tuesday, 15 November 2022 at 22:39
> To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>
> Subject: Re: [HoTT] Question about the formal rules of cohesive 
> homotopy type theory
>>  Does this also include the structural rules of type theory such as 
>> the substitution and weakening rules?
>
> I would just like to point out that substutition and weakening 
> typically are not part of the rules. They are shown to be admissible. 
> In this spirit, the question should have been: what is the precise 
> version of substitution and weakening (which is a special case of 
> substitution) that is admissible in cohesive type theory?
>
> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/HomotopyTypeTheory/D66F4584-A005-4F69-8E75-E976E0FF9957%40andrej.com.
>
>
>
> 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 contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
> -- 
> You received this message because you are subscribed to the Google 
> Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send 
> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB786979CA94519BCC98EDD32FCD079%40PAXPR06MB7869.eurprd06.prod.outlook.com.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF%40jonmsterling.com.

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

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Michael Shulman]

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

As far as the mathematical study of type theories and their models goes,
that may be true.  But I believe that when talking about the way type
theories are used in practice, either on paper or in a proof assistant,
there is still a difference.

Suppose I am teaching a calculus class, and I define f(x) = x^2 + 1 and I
want to evaluate f(3).  I don't write

f(3) = (x^2+1)[3/x] = (x^2)[3/x] + 1[3/x] = 3^2 + 1 = 9 + 1 = 10.

Instead, I jump right to f(3) = 3^2+1, because substitution is an operation
that happens immediately in my head, not a computational step analogous to
3^2 = 9.  Similarly, the user of a proof assistant never types or sees
substitution as part of the syntax; it is an operation *on* syntax that
happens behind the scenes.

Yes, this is a property of a particular *presentation* of a free structure
rather than a property of the structure itself, but that doesn't
intrinsically make it unimportant.  Groups and group presentations are both
important.  Maybe you want to say that "a type theory" refers to the free
structure rather than its presentation, but choosing to use words in that
way doesn't by itself make "presentations of type theories" (or whatever
you call them) less important.  Maybe you want to define an "admissible
rule" to be a property that holds in the syntax but fails in some actual
models; but that doesn't make "rules that hold in all models and can be
made to hold in a particular presentation of the free model without being
given explicitly as generating operations/equalities" (or whatever you call
them) less important.

I do agree that Andrej's formulation sounds backwards.  In practice (in my
experience) one doesn't write the rules down first and then try to figure
out what kind of substitution is admissible.  Instead one decides what the
substitution rule should be, and *then* (hopefully) works out a way of
presenting the syntax to make that substitution rule admissible.  This is
particularly tricky for modal type theories, where the categorically
"obvious" rules do not admit substitution, and leads to the introduction of
split contexts as used in the BFP paper.  I have trouble imagining how I
could have written that paper if I had been forced to write explicit
substitutions everywhere.  Thorsten and Jon, do you maintain that all the
work that's gone into figuring out ways to present modal type theories with
"admissible substitution" is meaningless?

On Thu, Nov 17, 2022 at 5:37 AM Jon Sterling <jon@jonmsterling.com> wrote:

> Indeed, I echo Thorsten's comment — to put it another way, even being able
> to tell whether these rules are derivable or only admissible is like
> knowing what an angel's favorite TV show is (in other words, a form of
> knowledge that cannot be applied toward anything by human beings). At least
> for structural type theory, there is nothing worth saying that cannot be
> phrased in a way that does not depend on whether structural rules are
> admissible or derivable. It may be that admissiblity of structural rules
> starts to play a role in substructural type theory, however, but this is
> not my area of expertise.
>
> It is revealing that nobody has proposed a notion of **model** of type
> theory in which the admissible structural rules do not hold; this would be
> the necessary form taken by any evidence for the thesis that it is
> important for structural rules to not be derivable. Absent such a notion of
> model and evidence that it is at all compelling/useful, we would have to
> conclude that worrying about admissibility vs. derivability of structural
> rules in the official presentation of type theory is fundementally
> misguided.
>
> On 16 Nov 2022, at 4:52, 'Thorsten Altenkirch' via Homotopy Type Theory
> wrote:
>
> That depends on what presentation of Type Theory you are using. Your
> remarks apply to the extrinsic approach from the last millennium. More
> recent presentation of Type Theory built in substitution and weakening and
> use an intrinsic approach which avoids talking about preterms you don’t
> really care about.
>
>
>
> https://dl.acm.org/doi/10.1145/2837614.2837638
>
>
>
> Cheers,
>
> Thorsten
>
>
>
> *From:* homotopytypetheory@googlegroups.com <
> homotopytypetheory@googlegroups.com> on behalf of andrej.bauer@andrej.com
> <andrej.bauer@andrej.com>
> *Date:* Tuesday, 15 November 2022 at 22:39
> *To:* Homotopy Type Theory <homotopytypetheory@googlegroups.com>
> *Subject:* Re: [HoTT] Question about the formal rules of cohesive
> homotopy type theory
>
> >  Does this also include the structural rules of type theory such as the
> substitution and weakening rules?
>
> I would just like to point out that substutition and weakening typically
> are not part of the rules. They are shown to be admissible. In this spirit,
> the question should have been: what is the precise version of substitution
> and weakening (which is a special case of substitution) that is admissible
> in cohesive type theory?
>
> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/HomotopyTypeTheory/D66F4584-A005-4F69-8E75-E976E0FF9957%40andrej.com
> .
>
> 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 contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB786979CA94519BCC98EDD32FCD079%40PAXPR06MB7869.eurprd06.prod.outlook.com
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB786979CA94519BCC98EDD32FCD079%40PAXPR06MB7869.eurprd06.prod.outlook.com?utm_medium=email&utm_source=footer>
> .
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/HomotopyTypeTheory/41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF%40jonmsterling.com
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF%40jonmsterling.com?utm_medium=email&utm_source=footer>
> .
>

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpxcTpvy6%2BBS%2B-5yjOjVFkdXFHdmCX0U3Qre2J6t8Lfh_g%40mail.gmail.com.

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

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Tom Hirschowitz]

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

Only valid for simply-typed languages, so not (yet) contradicting Jon's
claim: admissibility of substitution is important in the development of
Howe's method for proving that applicative bisimilarity is a congruence.
Essentially, the reason is that it provides a simpler induction principle.
This is implicit in my recent work with Peio Borthelle and Ambroise Lafont
on a categorical framework for Howe's method (e.g., [1]), used as
motivation for "A unified treatment of structural definitions on syntax..."
[2], and explicitly used (and extended to operations other than
substitution) in ongoing work on a generalisation of [1].

More generally, I suspect that it is useful in programming language theory,
where people tend to work with extrinsic presentations.

[1] https://hal.archives-ouvertes.fr/hal-02966439v6
[2] https://hal.archives-ouvertes.fr/hal-03633933

Le ven. 18 nov. 2022 à 03:35, Michael Shulman <shulman@sandiego.edu> a
écrit :

> As far as the mathematical study of type theories and their models goes,
> that may be true.  But I believe that when talking about the way type
> theories are used in practice, either on paper or in a proof assistant,
> there is still a difference.
>
> Suppose I am teaching a calculus class, and I define f(x) = x^2 + 1 and I
> want to evaluate f(3).  I don't write
>
> f(3) = (x^2+1)[3/x] = (x^2)[3/x] + 1[3/x] = 3^2 + 1 = 9 + 1 = 10.
>
> Instead, I jump right to f(3) = 3^2+1, because substitution is an
> operation that happens immediately in my head, not a computational step
> analogous to 3^2 = 9.  Similarly, the user of a proof assistant never types
> or sees substitution as part of the syntax; it is an operation *on* syntax
> that happens behind the scenes.
>
> Yes, this is a property of a particular *presentation* of a free structure
> rather than a property of the structure itself, but that doesn't
> intrinsically make it unimportant.  Groups and group presentations are both
> important.  Maybe you want to say that "a type theory" refers to the free
> structure rather than its presentation, but choosing to use words in that
> way doesn't by itself make "presentations of type theories" (or whatever
> you call them) less important.  Maybe you want to define an "admissible
> rule" to be a property that holds in the syntax but fails in some actual
> models; but that doesn't make "rules that hold in all models and can be
> made to hold in a particular presentation of the free model without being
> given explicitly as generating operations/equalities" (or whatever you call
> them) less important.
>
> I do agree that Andrej's formulation sounds backwards.  In practice (in my
> experience) one doesn't write the rules down first and then try to figure
> out what kind of substitution is admissible.  Instead one decides what the
> substitution rule should be, and *then* (hopefully) works out a way of
> presenting the syntax to make that substitution rule admissible.  This is
> particularly tricky for modal type theories, where the categorically
> "obvious" rules do not admit substitution, and leads to the introduction of
> split contexts as used in the BFP paper.  I have trouble imagining how I
> could have written that paper if I had been forced to write explicit
> substitutions everywhere.  Thorsten and Jon, do you maintain that all the
> work that's gone into figuring out ways to present modal type theories with
> "admissible substitution" is meaningless?
>
> On Thu, Nov 17, 2022 at 5:37 AM Jon Sterling <jon@jonmsterling.com> wrote:
>
>> Indeed, I echo Thorsten's comment — to put it another way, even being
>> able to tell whether these rules are derivable or only admissible is like
>> knowing what an angel's favorite TV show is (in other words, a form of
>> knowledge that cannot be applied toward anything by human beings). At least
>> for structural type theory, there is nothing worth saying that cannot be
>> phrased in a way that does not depend on whether structural rules are
>> admissible or derivable. It may be that admissiblity of structural rules
>> starts to play a role in substructural type theory, however, but this is
>> not my area of expertise.
>>
>> It is revealing that nobody has proposed a notion of **model** of type
>> theory in which the admissible structural rules do not hold; this would be
>> the necessary form taken by any evidence for the thesis that it is
>> important for structural rules to not be derivable. Absent such a notion of
>> model and evidence that it is at all compelling/useful, we would have to
>> conclude that worrying about admissibility vs. derivability of structural
>> rules in the official presentation of type theory is fundementally
>> misguided.
>>
>> On 16 Nov 2022, at 4:52, 'Thorsten Altenkirch' via Homotopy Type Theory
>> wrote:
>>
>> That depends on what presentation of Type Theory you are using. Your
>> remarks apply to the extrinsic approach from the last millennium. More
>> recent presentation of Type Theory built in substitution and weakening and
>> use an intrinsic approach which avoids talking about preterms you don’t
>> really care about.
>>
>>
>>
>> https://dl.acm.org/doi/10.1145/2837614.2837638
>>
>>
>>
>> Cheers,
>>
>> Thorsten
>>
>>
>>
>> *From:* homotopytypetheory@googlegroups.com <
>> homotopytypetheory@googlegroups.com> on behalf of andrej.bauer@andrej.com
>> <andrej.bauer@andrej.com>
>> *Date:* Tuesday, 15 November 2022 at 22:39
>> *To:* Homotopy Type Theory <homotopytypetheory@googlegroups.com>
>> *Subject:* Re: [HoTT] Question about the formal rules of cohesive
>> homotopy type theory
>>
>> >  Does this also include the structural rules of type theory such as the
>> substitution and weakening rules?
>>
>> I would just like to point out that substutition and weakening typically
>> are not part of the rules. They are shown to be admissible. In this spirit,
>> the question should have been: what is the precise version of substitution
>> and weakening (which is a special case of substitution) that is admissible
>> in cohesive type theory?
>>
>> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
>> To view this discussion on the web visit
>> https://groups.google.com/d/msgid/HomotopyTypeTheory/D66F4584-A005-4F69-8E75-E976E0FF9957%40andrej.com
>> .
>>
>> 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 contact the sender and delete the email and
>> attachment.
>>
>> Any views or opinions expressed by the author of this email do not
>> necessarily reflect the views of the University of Nottingham. Email
>> communications with the University of Nottingham may be monitored
>> where permitted by law.
>>
>>
>>
>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
>> To view this discussion on the web visit
>> https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB786979CA94519BCC98EDD32FCD079%40PAXPR06MB7869.eurprd06.prod.outlook.com
>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB786979CA94519BCC98EDD32FCD079%40PAXPR06MB7869.eurprd06.prod.outlook.com?utm_medium=email&utm_source=footer>
>> .
>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
>> To view this discussion on the web visit
>> https://groups.google.com/d/msgid/HomotopyTypeTheory/41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF%40jonmsterling.com
>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF%40jonmsterling.com?utm_medium=email&utm_source=footer>
>> .
>>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpxcTpvy6%2BBS%2B-5yjOjVFkdXFHdmCX0U3Qre2J6t8Lfh_g%40mail.gmail.com
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpxcTpvy6%2BBS%2B-5yjOjVFkdXFHdmCX0U3Qre2J6t8Lfh_g%40mail.gmail.com?utm_medium=email&utm_source=footer>
> .
>

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAHE5TSNXhvH4QH08fW1mOk8Qn7sGPCfTzRN37rfhMxeQEqyVqA%40mail.gmail.com.

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

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Jon Sterling]

[-- Attachment #1: Type: text/html, Size: 11547 bytes --]

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Michael Shulman]

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

On Fri, Nov 18, 2022 at 2:59 AM Jon Sterling <jon@jonmsterling.com> wrote:

> Hi Mike, thanks for your comments — regarding modal type theory, please
> note that there are state of the art general modal type theories that do
> not employ admissible substitution! MTT is one of them.
>

Split-context modal type theories can also be presented without admissible
substitutions.  Making substitutions explicit is easy; it's making them
admissible that's hard.  And as far as I understand it, MTT does satisfy
the primary desideratum when making substitutions admissible, namely that
all rules have a fully general context in their conclusion.

MTT is also not equivalent to split-context theories, and IMHO is less
pleasant to work with in practice.  I believe there should be some way to
combine the ideas of the two theories.

By the way, in the followup paper "Modalities and parametric adjoints" by
Gratzer, Cavallo, Kavvos, Guatto, and Birkedal (three of whom are also
authors of the MTT paper) we read "The admissibility of substitution is a
central property of type theory, and indeed of all logic" (section IB).

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpwz_Y61ST5eauZiH1b9E79BF--oroXinvzd2odHsycyjg%40mail.gmail.com.

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

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Jon Sterling]

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

On 18 Nov 2022, at 11:16, Michael Shulman wrote:

> On Fri, Nov 18, 2022 at 2:59 AM Jon Sterling <jon@jonmsterling.com> 
> wrote:
>
>> Hi Mike, thanks for your comments — regarding modal type theory, 
>> please
>> note that there are state of the art general modal type theories that 
>> do
>> not employ admissible substitution! MTT is one of them.
>>
>
> Split-context modal type theories can also be presented without 
> admissible
> substitutions.  Making substitutions explicit is easy; it's making 
> them
> admissible that's hard.  And as far as I understand it, MTT does 
> satisfy
> the primary desideratum when making substitutions admissible, namely 
> that
> all rules have a fully general context in their conclusion.
>
> MTT is also not equivalent to split-context theories, and IMHO is less
> pleasant to work with in practice.  I believe there should be some way 
> to
> combine the ideas of the two theories.
>
> By the way, in the followup paper "Modalities and parametric adjoints" 
> by
> Gratzer, Cavallo, Kavvos, Guatto, and Birkedal (three of whom are also
> authors of the MTT paper) we read "The admissibility of substitution 
> is a
> central property of type theory, and indeed of all logic" (section 
> IB).


The real reason it is central is that making substitution admissible 
forces you to figure out the equational theory of substitutions (as I 
said), not the other way around. You are free to consult the other 
authors of that paper, and I guarantee to you that they will confirm my 
analysis. Admissibility seems to have been cargo-culted, as people 
forgot the reason why it was important in the first place.

It is important to recall that the first admissible rule was *cut* in 
Gentzen's analysis of sequent calculus, but Gentzen's cut-free sequent 
calculus is eliminating not only substitution but also all computational 
redexes simultaneously (this is due to the way that sequent calculus is 
arranged). This kind of admissibility is much more useful than mere 
admissibility of substitution, because it gives a normal-forms 
presentation, which (unlike mere admissible substitution) actually has a 
ton of practical applications (not just deciding equivalence, but also 
proof search, etc.).  So I would characterize my viewpoint as an 
essentially orthodox one, though the language we use to say these things 
in 2022 is very different from what was available in the 1930s.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/4D4B5058-E159-4139-8713-979EC5E1D3BA%40jonmsterling.com.

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

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

['Thorsten Altenkirch' via Homotopy Type Theory]

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

Hi Mike,

Certainly I would never claim that anybody’s work is meaningless, but I think that understanding and presentation can often by improved by using an appropriate level of abstraction. Often the obvious and naïve choice isn’t the best option. I experience this a lot with students who often use strings to represent syntactic objects like expressions. One of my mantras is “use trees not strings” – I even made a youtube video<https://youtu.be/7tCNu4CnjVc> about it.

Now most people accept that we should use trees to represent syntax but many still believe that typing should be extrinsic: ie we first define untyped syntax (using trees) and then a typing relation. In my view they make a similar mistake as my students using strings but on a different level. When I think about type theory I only want to talk about typed objects. Properties like subject reduction, admissibility of substitution etc are just noise caused by using an inappropriate level of abstraction. The essence of what we want to say becomes clear once we overcome these misleading traditions. This becomes even more essential once we deal with dependent types where the overhead often becomes unbearable.

Now people we say that we do need to implement and verify programs like type checkers. That is true and it is similar to the need for parsers to translate from strings to trees. My understanding of a parser is that it is the partial inverse of the printing function which translates trees into strings. Similarly a type checker is the partial inverse of a function from intrinsically typed terms to untyped terms. Hence yes we do need to implement the whole toolchain of parsers, typecheckers and when we implement a type system but its specification should happen on the top.

I haven’t worked on modal type theories but I suspect that they can and should be presented intrinsically. I refer to Jon’s comments on this topic.

Cheers,
Thorsten

From: Michael Shulman <shulman@sandiego.edu>
Date: Friday, 18 November 2022 at 02:36
To: Jon Sterling <jon@jonmsterling.com>
Cc: Thorsten Altenkirch (staff) <psztxa@exmail.nottingham.ac.uk>, andrej.bauer <andrej.bauer@andrej.com>, Homotopy Type Theory <homotopytypetheory@googlegroups.com>
Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory
As far as the mathematical study of type theories and their models goes, that may be true.  But I believe that when talking about the way type theories are used in practice, either on paper or in a proof assistant, there is still a difference.

Suppose I am teaching a calculus class, and I define f(x) = x^2 + 1 and I want to evaluate f(3).  I don't write

f(3) = (x^2+1)[3/x] = (x^2)[3/x] + 1[3/x] = 3^2 + 1 = 9 + 1 = 10.

Instead, I jump right to f(3) = 3^2+1, because substitution is an operation that happens immediately in my head, not a computational step analogous to 3^2 = 9.  Similarly, the user of a proof assistant never types or sees substitution as part of the syntax; it is an operation *on* syntax that happens behind the scenes.

Yes, this is a property of a particular *presentation* of a free structure rather than a property of the structure itself, but that doesn't intrinsically make it unimportant.  Groups and group presentations are both important.  Maybe you want to say that "a type theory" refers to the free structure rather than its presentation, but choosing to use words in that way doesn't by itself make "presentations of type theories" (or whatever you call them) less important.  Maybe you want to define an "admissible rule" to be a property that holds in the syntax but fails in some actual models; but that doesn't make "rules that hold in all models and can be made to hold in a particular presentation of the free model without being given explicitly as generating operations/equalities" (or whatever you call them) less important.

I do agree that Andrej's formulation sounds backwards.  In practice (in my experience) one doesn't write the rules down first and then try to figure out what kind of substitution is admissible.  Instead one decides what the substitution rule should be, and *then* (hopefully) works out a way of presenting the syntax to make that substitution rule admissible.  This is particularly tricky for modal type theories, where the categorically "obvious" rules do not admit substitution, and leads to the introduction of split contexts as used in the BFP paper.  I have trouble imagining how I could have written that paper if I had been forced to write explicit substitutions everywhere.  Thorsten and Jon, do you maintain that all the work that's gone into figuring out ways to present modal type theories with "admissible substitution" is meaningless?

On Thu, Nov 17, 2022 at 5:37 AM Jon Sterling <jon@jonmsterling.com<mailto:jon@jonmsterling.com>> wrote:

Indeed, I echo Thorsten's comment — to put it another way, even being able to tell whether these rules are derivable or only admissible is like knowing what an angel's favorite TV show is (in other words, a form of knowledge that cannot be applied toward anything by human beings). At least for structural type theory, there is nothing worth saying that cannot be phrased in a way that does not depend on whether structural rules are admissible or derivable. It may be that admissiblity of structural rules starts to play a role in substructural type theory, however, but this is not my area of expertise.

It is revealing that nobody has proposed a notion of **model** of type theory in which the admissible structural rules do not hold; this would be the necessary form taken by any evidence for the thesis that it is important for structural rules to not be derivable. Absent such a notion of model and evidence that it is at all compelling/useful, we would have to conclude that worrying about admissibility vs. derivability of structural rules in the official presentation of type theory is fundementally misguided.


On 16 Nov 2022, at 4:52, 'Thorsten Altenkirch' via Homotopy Type Theory wrote:
That depends on what presentation of Type Theory you are using. Your remarks apply to the extrinsic approach from the last millennium. More recent presentation of Type Theory built in substitution and weakening and use an intrinsic approach which avoids talking about preterms you don’t really care about.

https://dl.acm.org/doi/10.1145/2837614.2837638

Cheers,
Thorsten

From: homotopytypetheory@googlegroups.com<mailto:homotopytypetheory@googlegroups.com> <homotopytypetheory@googlegroups.com<mailto:homotopytypetheory@googlegroups.com>> on behalf of andrej.bauer@andrej.com<mailto:andrej.bauer@andrej.com> <andrej.bauer@andrej.com<mailto:andrej.bauer@andrej.com>>
Date: Tuesday, 15 November 2022 at 22:39
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com<mailto:homotopytypetheory@googlegroups.com>>
Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory
>  Does this also include the structural rules of type theory such as the substitution and weakening rules?

I would just like to point out that substutition and weakening typically are not part of the rules. They are shown to be admissible. In this spirit, the question should have been: what is the precise version of substitution and weakening (which is a special case of substitution) that is admissible in cohesive type theory?

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 HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory%2Bunsubscribe@googlegroups.com>.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/D66F4584-A005-4F69-8E75-E976E0FF9957%40andrej.com.

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 contact the sender and delete the email and

attachment.



Any views or opinions expressed by the author of this email do not

necessarily reflect the views of the University of Nottingham. Email

communications with the University of Nottingham may be monitored

where permitted by law.






--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB786979CA94519BCC98EDD32FCD079%40PAXPR06MB7869.eurprd06.prod.outlook.com<https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB786979CA94519BCC98EDD32FCD079%40PAXPR06MB7869.eurprd06.prod.outlook.com?utm_medium=email&utm_source=footer>.
--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF%40jonmsterling.com<https://groups.google.com/d/msgid/HomotopyTypeTheory/41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF%40jonmsterling.com?utm_medium=email&utm_source=footer>.



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 contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.




-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB7869899326D6A5C41CC20CB9CD099%40PAXPR06MB7869.eurprd06.prod.outlook.com.

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

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Jon Sterling]

On 17 Nov 2022, at 21:35, Michael Shulman wrote:

> As far as the mathematical study of type theories and their models goes,
> that may be true.  But I believe that when talking about the way type
> theories are used in practice, either on paper or in a proof assistant,
> there is still a difference.
>
> Suppose I am teaching a calculus class, and I define f(x) = x^2 + 1 and I
> want to evaluate f(3).  I don't write
>
> f(3) = (x^2+1)[3/x] = (x^2)[3/x] + 1[3/x] = 3^2 + 1 = 9 + 1 = 10.
>
> Instead, I jump right to f(3) = 3^2+1, because substitution is an operation
> that happens immediately in my head, not a computational step analogous to
> 3^2 = 9.  Similarly, the user of a proof assistant never types or sees
> substitution as part of the syntax; it is an operation *on* syntax that
> happens behind the scenes.

By the way, I find this calculus example to be supremely uncompelling --- not because I am hung up on the fact that it pertains to a presentation, but because mathematics is full of equations that we basically agree not to mention at various times.

It is also not particularly helpful to your point to bring up implementation, where it is extremely common to eschew implicit substitution for explicit substitutions --- or to use a mix of the two... In neither case are the details of this presented to the user, however, because the gender of an angel is not useful information to mere humans who use proof assistants.

Best,
Jon

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/9B3B568C-452A-4919-A149-CF7C1E91CDAE%40jonmsterling.com.

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Jon Sterling]

Maybe just to put a finer point on it, re: the calculus example (and then I'll try to shut up, I have alreadyspoken too much):

I subscribe to the viewpoint of the HoTT book regarding the practice of informal mathematics (or at least, I subscribe to a version of the viewpoint of the HoTT book which I think at least some of its authors held, including Steve Awodey with whom I have discussed this topic at length in the past). Things like terms, variables, and substitution do not actually arise in informal mathematics: instead, we work *directly* with things that are functions of other things. Thus when doing informal mathematics, if we say "term" we usually mean something that someone might more precisely refer to as an "element". (But let me not open that can of worms!)

In that sense, it would be completely incorrect to say that when doing mathematics and we have a function `f(x) = x^2 + 1`, to evaluate f at 3 we must apply a syntactical operation that recursively walks a syntax tree and replaces a placeholder with 3. The function `f` has the same ontological status as a tree or as a friend or as a piece of stone: it is not a piece of code that tracks a function, rather it is *actually* a function --- in the same way that a stone is not a representation of an object, but an actual object. Thus to evaluate `f(3)`, we use what we know about `f`: namely that it is the function associated to the law that relates any number to the successor of its square.

So in ordinary math, "substitution" tends to be a façon de parler for an operation that is not really syntactical at all but is instead intrinsically constitutive of the informal notion of a "mapping", which exists long before any logicians could attempt to intervene with their syntactical gesticulations... (By the way: truly syntactic substitution also arises *separately* in mathematics, by the way, when thinking about free extensions of algebraic objects (like rings of the form R[x]). But this is a very specialized usage, and if we are being precise we will always distinguish between an element of R[x] and the function it encodes.)

It is true that it is possible to put aside this ontology, and think of mathematical objects in terms of their encodings and then make sure to only speak of syntactical operations that track mathematical operations (e.g. well-typed substitutions, but not ill-typed substitutions). But this is the way of logicians, and it is not really pertinent to the practice of everyday mathematics. Mathematics abstracts over these things, and we try to work "directly" with the objects we are concerned with, regardless of where we fall on the ancient debate of the "real-ness" of these objects.

I fear we have veered off topic from the original question! But I think it would be great if we could put this debate to rest once and for all --- I am constantly amazed to be the syntactician in the room, but having semanticists insist to me that the study of syntax needs raw terms and variables and admissible substitution, etc. If it were needed, then I would certainly have noticed it by now! The world of syntax is far richer than can be described with mere trees or strings, and many of us who study syntax for a living have moved on from that viewpoint. ;-)

Best,
Jon


On 18 Nov 2022, at 7:47, Jon Sterling wrote:

> On 17 Nov 2022, at 21:35, Michael Shulman wrote:
>
>> As far as the mathematical study of type theories and their models goes,
>> that may be true.  But I believe that when talking about the way type
>> theories are used in practice, either on paper or in a proof assistant,
>> there is still a difference.
>>
>> Suppose I am teaching a calculus class, and I define f(x) = x^2 + 1 and I
>> want to evaluate f(3).  I don't write
>>
>> f(3) = (x^2+1)[3/x] = (x^2)[3/x] + 1[3/x] = 3^2 + 1 = 9 + 1 = 10.
>>
>> Instead, I jump right to f(3) = 3^2+1, because substitution is an operation
>> that happens immediately in my head, not a computational step analogous to
>> 3^2 = 9.  Similarly, the user of a proof assistant never types or sees
>> substitution as part of the syntax; it is an operation *on* syntax that
>> happens behind the scenes.
>
> By the way, I find this calculus example to be supremely uncompelling --- not because I am hung up on the fact that it pertains to a presentation, but because mathematics is full of equations that we basically agree not to mention at various times.
>
> It is also not particularly helpful to your point to bring up implementation, where it is extremely common to eschew implicit substitution for explicit substitutions --- or to use a mix of the two... In neither case are the details of this presented to the user, however, because the gender of an angel is not useful information to mere humans who use proof assistants.
>
> Best,
> Jon

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/21B50B02-4107-4854-8015-99EA4B14EBA5%40jonmsterling.com.

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Michael Shulman]

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

In general, I feel like we are still talking past each other.  Maybe the
problem is that I still haven't found the words that will communicate my
point to you.  I was trying to say that it isn't the word "admissible" that
matters, but there are real mathematical questions going on whatever words
you use to talk about them.

Last summer when I was explaining something about HOTT to a group that I
think included you, I used the phrase "admissible" for a certain equality,
and we got into a bit of this discussion.  But I felt like we agreed in the
end that what I meant was "a rule that doesn't have to get used explicitly
by the conversion-checker", and that it was useful to distinguish such
things whatever we call them.  That's what I was trying to get at with
"rules that hold in all models and can be made to hold in a particular
presentation of the free model without being given explicitly as generating
operations/equalities".

Similarly, I don't think the implicitness or explicitness of substitutions
in the syntax is what's crucial.  If you formulate substitutions
implicitly, then the statement you want is that substitution can be defined
as an "admissible" operation on the syntax.  If you formulate substitutions
explicitly, then the statement you want is that substitutions can be
eliminated by a computation.  Isn't this what you mean by "The equational
theory of substitution in this situation (particularly, how to commute
substitutions past the modal forms) is the hard part"?  You don't just want
an equational theory for substitution -- the equations in an equational
theory are undirected -- but some kind of rewriting system that tells you
how to push a substitution inside the modal forms.  Whether the
substitutions are part of the syntax or not isn't the point.



On Fri, Nov 18, 2022 at 5:06 AM Jon Sterling <jon@jonmsterling.com> wrote:

> Maybe just to put a finer point on it, re: the calculus example (and then
> I'll try to shut up, I have alreadyspoken too much):
>
> I subscribe to the viewpoint of the HoTT book regarding the practice of
> informal mathematics (or at least, I subscribe to a version of the
> viewpoint of the HoTT book which I think at least some of its authors held,
> including Steve Awodey with whom I have discussed this topic at length in
> the past). Things like terms, variables, and substitution do not actually
> arise in informal mathematics: instead, we work *directly* with things that
> are functions of other things. Thus when doing informal mathematics, if we
> say "term" we usually mean something that someone might more precisely
> refer to as an "element". (But let me not open that can of worms!)
>
> In that sense, it would be completely incorrect to say that when doing
> mathematics and we have a function `f(x) = x^2 + 1`, to evaluate f at 3 we
> must apply a syntactical operation that recursively walks a syntax tree and
> replaces a placeholder with 3. The function `f` has the same ontological
> status as a tree or as a friend or as a piece of stone: it is not a piece
> of code that tracks a function, rather it is *actually* a function --- in
> the same way that a stone is not a representation of an object, but an
> actual object. Thus to evaluate `f(3)`, we use what we know about `f`:
> namely that it is the function associated to the law that relates any
> number to the successor of its square.
>
> So in ordinary math, "substitution" tends to be a façon de parler for an
> operation that is not really syntactical at all but is instead
> intrinsically constitutive of the informal notion of a "mapping", which
> exists long before any logicians could attempt to intervene with their
> syntactical gesticulations... (By the way: truly syntactic substitution
> also arises *separately* in mathematics, by the way, when thinking about
> free extensions of algebraic objects (like rings of the form R[x]). But
> this is a very specialized usage, and if we are being precise we will
> always distinguish between an element of R[x] and the function it encodes.)
>
> It is true that it is possible to put aside this ontology, and think of
> mathematical objects in terms of their encodings and then make sure to only
> speak of syntactical operations that track mathematical operations (e.g.
> well-typed substitutions, but not ill-typed substitutions). But this is the
> way of logicians, and it is not really pertinent to the practice of
> everyday mathematics. Mathematics abstracts over these things, and we try
> to work "directly" with the objects we are concerned with, regardless of
> where we fall on the ancient debate of the "real-ness" of these objects.
>
> I fear we have veered off topic from the original question! But I think it
> would be great if we could put this debate to rest once and for all --- I
> am constantly amazed to be the syntactician in the room, but having
> semanticists insist to me that the study of syntax needs raw terms and
> variables and admissible substitution, etc. If it were needed, then I would
> certainly have noticed it by now! The world of syntax is far richer than
> can be described with mere trees or strings, and many of us who study
> syntax for a living have moved on from that viewpoint. ;-)
>
> Best,
> Jon
>
>
> On 18 Nov 2022, at 7:47, Jon Sterling wrote:
>
> > On 17 Nov 2022, at 21:35, Michael Shulman wrote:
> >
> >> As far as the mathematical study of type theories and their models goes,
> >> that may be true.  But I believe that when talking about the way type
> >> theories are used in practice, either on paper or in a proof assistant,
> >> there is still a difference.
> >>
> >> Suppose I am teaching a calculus class, and I define f(x) = x^2 + 1 and
> I
> >> want to evaluate f(3).  I don't write
> >>
> >> f(3) = (x^2+1)[3/x] = (x^2)[3/x] + 1[3/x] = 3^2 + 1 = 9 + 1 = 10.
> >>
> >> Instead, I jump right to f(3) = 3^2+1, because substitution is an
> operation
> >> that happens immediately in my head, not a computational step analogous
> to
> >> 3^2 = 9.  Similarly, the user of a proof assistant never types or sees
> >> substitution as part of the syntax; it is an operation *on* syntax that
> >> happens behind the scenes.
> >
> > By the way, I find this calculus example to be supremely uncompelling
> --- not because I am hung up on the fact that it pertains to a
> presentation, but because mathematics is full of equations that we
> basically agree not to mention at various times.
> >
> > It is also not particularly helpful to your point to bring up
> implementation, where it is extremely common to eschew implicit
> substitution for explicit substitutions --- or to use a mix of the two...
> In neither case are the details of this presented to the user, however,
> because the gender of an angel is not useful information to mere humans who
> use proof assistants.
> >
> > Best,
> > Jon
>

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpxMB%3D1kSPQM-OmSV_a9EauGmz7Gr-U3L%3DqfLCqsgzOnZQ%40mail.gmail.com.

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

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Jon Sterling]

Hi Mike,

Thanks for this! I think we are getting a lot closer.

On 18 Nov 2022, at 11:25, Michael Shulman wrote:

> In general, I feel like we are still talking past each other.  Maybe the
> problem is that I still haven't found the words that will communicate my
> point to you.  I was trying to say that it isn't the word "admissible" that
> matters, but there are real mathematical questions going on whatever words
> you use to talk about them.
>
> Last summer when I was explaining something about HOTT to a group that I
> think included you, I used the phrase "admissible" for a certain equality,
> and we got into a bit of this discussion.  But I felt like we agreed in the
> end that what I meant was "a rule that doesn't have to get used explicitly
> by the conversion-checker", and that it was useful to distinguish such
> things whatever we call them.  That's what I was trying to get at with
> "rules that hold in all models and can be made to hold in a particular
> presentation of the free model without being given explicitly as generating
> operations/equalities".
>
> Similarly, I don't think the implicitness or explicitness of substitutions
> in the syntax is what's crucial.  If you formulate substitutions
> implicitly, then the statement you want is that substitution can be defined
> as an "admissible" operation on the syntax.  If you formulate substitutions
> explicitly, then the statement you want is that substitutions can be
> eliminated by a computation.  Isn't this what you mean by "The equational
> theory of substitution in this situation (particularly, how to commute
> substitutions past the modal forms) is the hard part"?  You don't just want
> an equational theory for substitution -- the equations in an equational
> theory are undirected -- but some kind of rewriting system that tells you
> how to push a substitution inside the modal forms.  Whether the
> substitutions are part of the syntax or not isn't the point.
>

I agree with a lot of what you have written here, but maybe not all of it. Let me put it my own way, which is probably similar to what you are getting at --- I see deciding the equational theory of substitution as a special case of deciding the rest of the equational theory. To me, it is basically useless to have a decision procedure for "reducing substitutions but not any other computations (like beta laws, etc.)". To put it another way, if I don't have an algorithm for full normalization (or at least deciding def.eq.), I really couldn't care less if I have an algorithm for reducing substitutions.

Regarding things that exist in the syntax but not necessarily in all models, this is indeed the point of admissibility and it's really really important! It just so happens, however, that substitutions are the main example of something that is both admissible **and** exists in all reasonable models. Even in weak models, we have substitution up to isomorphism --- and no existing solution to the Seely substitution coherence problem works by saying "Well, substitution is admissible, so we don't need it in the model anyway". So the one place to look for an example of substitution-admissibility being important in type theory is actually a non-example.

Not all admissible rules are as useless as this! To the contrary, there ARE very important examples of different admissible rules that must not be derivable unless we wish to degenerate the theory; the main examples that have practical import are injectivity laws, which allow you to deterministically reduce complex equality problems to simpler ones; without these, elaboration and type checking would be essentially impossible (whereas elaboration and typechecking are completely insensitive to the question of whether substitution is admissible). Injectivity of type constructors is the main example of an important admissible rule, but there are many more examples (and I expect, based on our conversations about HOTT over the summer) that there will be a lot more interesting and important ones to discover in the coming years.

So in case it clarifies me, I think admissibility is extremely important and it is, in some sense, the main topic that people like me study. My experience has led me, however, to make a distinction between admissibilities that matter (like injectivity laws) and ones that do not matter at all (like substitution). Nonetheless, there are many roads to the same idea, and the study of type theory and logic in terms of admissible substitutions has been (and remains) an extremely reliable and effective way to obtain well-behaved theories. All I am doing is trying to tease out which parts of this process were essential, and which parts were incidental.

Best,
Jon

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/19FCB983-3890-4113-9DD6-A76C2AFD8268%40jonmsterling.com.

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Michael Shulman]

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

Thanks.  It does sound like we mostly agree.  I would probably argue that
even for type theories in development, where we don't yet know that full
definitional equality is decidable -- or intrinsically ill-behaved type
theories like Lean, or Agda with non-confluent rewrite rules, where
definitional equality *isn't* decidable -- there is still value in being
able to reduce just substitutions.  But I think that's a relatively minor
point.

Maybe we can work out some way to use words so that this underlying
agreement is evident.  For instance, can we find a third word to use
alongside "admissible" and "derivable" to refer to operations/equalities
like substitution and its theory, which hold in all reasonable models, and
can be made admissible in some presentations, but more importantly can be
eliminated in an equality-checking algorithm?


On Fri, Nov 18, 2022 at 8:38 AM Jon Sterling <jon@jonmsterling.com> wrote:

> Hi Mike,
>
> Thanks for this! I think we are getting a lot closer.
>
> On 18 Nov 2022, at 11:25, Michael Shulman wrote:
>
> > In general, I feel like we are still talking past each other.  Maybe the
> > problem is that I still haven't found the words that will communicate my
> > point to you.  I was trying to say that it isn't the word "admissible"
> that
> > matters, but there are real mathematical questions going on whatever
> words
> > you use to talk about them.
> >
> > Last summer when I was explaining something about HOTT to a group that I
> > think included you, I used the phrase "admissible" for a certain
> equality,
> > and we got into a bit of this discussion.  But I felt like we agreed in
> the
> > end that what I meant was "a rule that doesn't have to get used
> explicitly
> > by the conversion-checker", and that it was useful to distinguish such
> > things whatever we call them.  That's what I was trying to get at with
> > "rules that hold in all models and can be made to hold in a particular
> > presentation of the free model without being given explicitly as
> generating
> > operations/equalities".
> >
> > Similarly, I don't think the implicitness or explicitness of
> substitutions
> > in the syntax is what's crucial.  If you formulate substitutions
> > implicitly, then the statement you want is that substitution can be
> defined
> > as an "admissible" operation on the syntax.  If you formulate
> substitutions
> > explicitly, then the statement you want is that substitutions can be
> > eliminated by a computation.  Isn't this what you mean by "The equational
> > theory of substitution in this situation (particularly, how to commute
> > substitutions past the modal forms) is the hard part"?  You don't just
> want
> > an equational theory for substitution -- the equations in an equational
> > theory are undirected -- but some kind of rewriting system that tells you
> > how to push a substitution inside the modal forms.  Whether the
> > substitutions are part of the syntax or not isn't the point.
> >
>
> I agree with a lot of what you have written here, but maybe not all of it.
> Let me put it my own way, which is probably similar to what you are getting
> at --- I see deciding the equational theory of substitution as a special
> case of deciding the rest of the equational theory. To me, it is basically
> useless to have a decision procedure for "reducing substitutions but not
> any other computations (like beta laws, etc.)". To put it another way, if I
> don't have an algorithm for full normalization (or at least deciding
> def.eq.), I really couldn't care less if I have an algorithm for reducing
> substitutions.
>
> Regarding things that exist in the syntax but not necessarily in all
> models, this is indeed the point of admissibility and it's really really
> important! It just so happens, however, that substitutions are the main
> example of something that is both admissible **and** exists in all
> reasonable models. Even in weak models, we have substitution up to
> isomorphism --- and no existing solution to the Seely substitution
> coherence problem works by saying "Well, substitution is admissible, so we
> don't need it in the model anyway". So the one place to look for an example
> of substitution-admissibility being important in type theory is actually a
> non-example.
>
> Not all admissible rules are as useless as this! To the contrary, there
> ARE very important examples of different admissible rules that must not be
> derivable unless we wish to degenerate the theory; the main examples that
> have practical import are injectivity laws, which allow you to
> deterministically reduce complex equality problems to simpler ones; without
> these, elaboration and type checking would be essentially impossible
> (whereas elaboration and typechecking are completely insensitive to the
> question of whether substitution is admissible). Injectivity of type
> constructors is the main example of an important admissible rule, but there
> are many more examples (and I expect, based on our conversations about HOTT
> over the summer) that there will be a lot more interesting and important
> ones to discover in the coming years.
>
> So in case it clarifies me, I think admissibility is extremely important
> and it is, in some sense, the main topic that people like me study. My
> experience has led me, however, to make a distinction between
> admissibilities that matter (like injectivity laws) and ones that do not
> matter at all (like substitution). Nonetheless, there are many roads to the
> same idea, and the study of type theory and logic in terms of admissible
> substitutions has been (and remains) an extremely reliable and effective
> way to obtain well-behaved theories. All I am doing is trying to tease out
> which parts of this process were essential, and which parts were incidental.
>
> Best,
> Jon
>

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpxB3-n6Udm86ZDZQTKUTYfgzjHWM6g85_-ANpo6pVsOqQ%40mail.gmail.com.

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

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Jon Sterling]

On 18 Nov 2022, at 11:56, Michael Shulman wrote:

> Thanks.  It does sound like we mostly agree.  I would probably argue that
> even for type theories in development, where we don't yet know that full
> definitional equality is decidable -- or intrinsically ill-behaved type
> theories like Lean, or Agda with non-confluent rewrite rules, where
> definitional equality *isn't* decidable -- there is still value in being
> able to reduce just substitutions.  But I think that's a relatively minor
> point.
>
> Maybe we can work out some way to use words so that this underlying
> agreement is evident.  For instance, can we find a third word to use
> alongside "admissible" and "derivable" to refer to operations/equalities
> like substitution and its theory, which hold in all reasonable models, and
> can be made admissible in some presentations, but more importantly can be
> eliminated in an equality-checking algorithm?
>

Cool, it's a relief to start getting this cleared up! I really agree with you that there is a need for terminology to describe the situation you mention, and maybe even more, there is a need to define this phenomenon...

I wonder if we can think of more concrete examples of this. For instance, in many versions of syntax (like bidirectional ones) we can choose to drop certain annotations because they will be available as part of the flow of information in the elaboration algorithm. Would these be an example of the phenomenon you are describing, or is it something different?

Best,
Jon

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/92CA5128-A764-47EA-8ECD-B6931F7EA7AF%40jonmsterling.com.

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Michael Shulman]

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

That's an interesting question.  I was thinking of operations and
equalities, and annotations are neither of those, but I can see that
they're somewhat similar in spirit.  But I find it even more difficult to
imagine how to define this phenomenon precisely in a way that would include
them...

On Fri, Nov 18, 2022 at 8:59 AM Jon Sterling <jon@jonmsterling.com> wrote:

> On 18 Nov 2022, at 11:56, Michael Shulman wrote:
>
> > Thanks.  It does sound like we mostly agree.  I would probably argue that
> > even for type theories in development, where we don't yet know that full
> > definitional equality is decidable -- or intrinsically ill-behaved type
> > theories like Lean, or Agda with non-confluent rewrite rules, where
> > definitional equality *isn't* decidable -- there is still value in being
> > able to reduce just substitutions.  But I think that's a relatively minor
> > point.
> >
> > Maybe we can work out some way to use words so that this underlying
> > agreement is evident.  For instance, can we find a third word to use
> > alongside "admissible" and "derivable" to refer to operations/equalities
> > like substitution and its theory, which hold in all reasonable models,
> and
> > can be made admissible in some presentations, but more importantly can be
> > eliminated in an equality-checking algorithm?
> >
>
> Cool, it's a relief to start getting this cleared up! I really agree with
> you that there is a need for terminology to describe the situation you
> mention, and maybe even more, there is a need to define this phenomenon...
>
> I wonder if we can think of more concrete examples of this. For instance,
> in many versions of syntax (like bidirectional ones) we can choose to drop
> certain annotations because they will be available as part of the flow of
> information in the elaboration algorithm. Would these be an example of the
> phenomenon you are describing, or is it something different?
>
> Best,
> Jon
>

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpyohZmqoArApd2vdE%2BGp%2BsVczpw95TDy9xvDnMStMj%3DZQ%40mail.gmail.com.

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

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Andreas Nuyts]

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

Hi everyone,

I finally found time to read up on this lengthy conversation.

Jon wrote:

    It is revealing that nobody has proposed a notion of **model** of
    type theory in which the admissible structural rules do not hold;
    this would be the necessary form taken by any evidence for the
    thesis that it is important for structural rules to not be derivable.


I think, on the contrary, that such models are not acknowledged as being 
models, because the language without substitution is in general not 
really the language of interest. An example of a model disrespecting 
substitution is the prettyprinter by Allais, Atkey, Chapman, McBride & 
McKinna (2021):
https://doi.org/10.1017/S0956796820000076
Indeed, substitution is no longer possible after prettyprinting, but all 
other language constructs are supported. Note that if a substitution 
operation is unavailable in a model, then the β-rule for functions 
cannot even be stated in that model, let alone asked to hold. So a model 
that fails to have a substitution operation necessarily also disrespects 
the equational theory of a language with such a β-rule. Prettyprinting 
indeed disrespects βη-equality.

Mike wrote:

    MTT is also not equivalent to split-context theories, and IMHO is
    less pleasant to work with in practice.


I'm reluctant to postulate here that any split-context theory is 
equivalent to some instance of MTT, but I would be quite surprised if 
you ever face any practical problems when abandoning a split-context 
system in favour of MTT. If you're thinking in particular about a system 
with crisp and non-crisp variables: such a system is implemented by 
Andrea in agda-flat. At the last Agda meeting, we have been 
investigating how mature the current modality system in Agda is and how 
feasible it is to support full MTT. One thing we observed is that - of 
all the parallel modality systems implemented in Agda - the cohesive one 
(of which only the flat and non-flat modalities are exposed to the user) 
is actually the one that adheres to the discipline of MTT (by having a 
third "squash" modality that effectively removes variables from the 
context).
Both regarding usability and equivalence, do not be misled by the 
invasive-looking locks. These locks have two confluent histories:
- there is a history of fitch-style logics,
- there is a history of modal logics with left-division. When 
implementing Menkar, which was intended as a proof assistant for general 
multimode systems with left division, I observed at some point that the 
left division of all modalities in the context actually never needs to 
be computed and can thus be regarded as a context /constructor/, rather 
than as an operation (i.e. admissibility of left division was not 
required, in none of the senses of the word mentioned so far). Modal 
Agda does use an eagerly computed left division. These systems with left 
division are very closely related to dual context systems.

I think usability is hard to judge because there isn't yet good tool 
support to experiment with. But I believe that it can grow on the user. 
A lock simply means "we've moved into a modal subterm". The position of 
the lock in the context is important in order to keep track of which 
variables were introduced before/after moving into that modal subterm. 
When using a variable, you just need to make sure that the variable's 
modal annotation is ≤ the composition of the locks, i.e. the modality of 
the position where we currently are and where we want to use the variable.

I am happy to discuss this matter further if you have any questions or 
doubts.

Best regards,
Andreas Nuyts

On 18.11.22 18:14, Michael Shulman wrote:
> That's an interesting question.  I was thinking of operations and 
> equalities, and annotations are neither of those, but I can see that 
> they're somewhat similar in spirit.  But I find it even more difficult 
> to imagine how to define this phenomenon precisely in a way that would 
> include them...
>
> On Fri, Nov 18, 2022 at 8:59 AM Jon Sterling <jon@jonmsterling.com> wrote:
>
>     On 18 Nov 2022, at 11:56, Michael Shulman wrote:
>
>     > Thanks.  It does sound like we mostly agree.  I would probably
>     argue that
>     > even for type theories in development, where we don't yet know
>     that full
>     > definitional equality is decidable -- or intrinsically
>     ill-behaved type
>     > theories like Lean, or Agda with non-confluent rewrite rules, where
>     > definitional equality *isn't* decidable -- there is still value
>     in being
>     > able to reduce just substitutions.  But I think that's a
>     relatively minor
>     > point.
>     >
>     > Maybe we can work out some way to use words so that this underlying
>     > agreement is evident.  For instance, can we find a third word to use
>     > alongside "admissible" and "derivable" to refer to
>     operations/equalities
>     > like substitution and its theory, which hold in all reasonable
>     models, and
>     > can be made admissible in some presentations, but more
>     importantly can be
>     > eliminated in an equality-checking algorithm?
>     >
>
>     Cool, it's a relief to start getting this cleared up! I really
>     agree with you that there is a need for terminology to describe
>     the situation you mention, and maybe even more, there is a need to
>     define this phenomenon...
>
>     I wonder if we can think of more concrete examples of this. For
>     instance, in many versions of syntax (like bidirectional ones) we
>     can choose to drop certain annotations because they will be
>     available as part of the flow of information in the elaboration
>     algorithm. Would these be an example of the phenomenon you are
>     describing, or is it something different?
>
>     Best,
>     Jon
>
> -- 
> You received this message because you are subscribed to the Google 
> Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send 
> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpyohZmqoArApd2vdE%2BGp%2BsVczpw95TDy9xvDnMStMj%3DZQ%40mail.gmail.com 
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpyohZmqoArApd2vdE%2BGp%2BsVczpw95TDy9xvDnMStMj%3DZQ%40mail.gmail.com?utm_medium=email&utm_source=footer>.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/4d352fc9-c4d3-2304-1510-17cd653513a8%40gmail.com.

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

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Jon Sterling]

[-- Attachment #1: Type: text/html, Size: 9948 bytes --]

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Andreas Nuyts]

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

Right, but when looking for a model that misses a substitution operation 
and is not contrived, you're not going to find it among the models that 
try to respect equality, because that isn't even statable in the model. 
When you drop both the requirement of supporting substitution, and of 
respecting equality, then your search space has grown enough that 
prettyprinters can be found in it.

On 01.12.22 16:54, Jon Sterling wrote:
> The issue regarding the beta law is kind of spurious: one of course 
> states the beta law using the ADMISSIBLE substitution action. The 
> problem with pretty printing is that it is indeed not satisfying the 
> beta law but this has absolutely nothing to do with substitution — you 
> can still check in the admissible-subst scenario whether the 
> interpretation function respects the beta law on all terms, and in 
> this case it just happens that it doesn’t.
>
>> On Dec 1, 2022, at 3:40 PM, Andreas Nuyts <andreasnuyts@gmail.com> wrote:
>>
>>  Hi everyone,
>>
>> I finally found time to read up on this lengthy conversation.
>>
>> Jon wrote:
>>
>>     It is revealing that nobody has proposed a notion of **model** of
>>     type theory in which the admissible structural rules do not hold;
>>     this would be the necessary form taken by any evidence for the
>>     thesis that it is important for structural rules to not be derivable.
>>
>>
>> I think, on the contrary, that such models are not acknowledged as 
>> being models, because the language without substitution is in general 
>> not really the language of interest. An example of a model 
>> disrespecting substitution is the prettyprinter by Allais, Atkey, 
>> Chapman, McBride & McKinna (2021):
>> https://doi.org/10.1017/S0956796820000076
>> Indeed, substitution is no longer possible after prettyprinting, but 
>> all other language constructs are supported. Note that if a 
>> substitution operation is unavailable in a model, then the β-rule for 
>> functions cannot even be stated in that model, let alone asked to 
>> hold. So a model that fails to have a substitution operation 
>> necessarily also disrespects the equational theory of a language with 
>> such a β-rule. Prettyprinting indeed disrespects βη-equality.
>>
>> Mike wrote:
>>
>>     MTT is also not equivalent to split-context theories, and IMHO is
>>     less pleasant to work with in practice.
>>
>>
>> I'm reluctant to postulate here that any split-context theory is 
>> equivalent to some instance of MTT, but I would be quite surprised if 
>> you ever face any practical problems when abandoning a split-context 
>> system in favour of MTT. If you're thinking in particular about a 
>> system with crisp and non-crisp variables: such a system is 
>> implemented by Andrea in agda-flat. At the last Agda meeting, we have 
>> been investigating how mature the current modality system in Agda is 
>> and how feasible it is to support full MTT. One thing we observed is 
>> that - of all the parallel modality systems implemented in Agda - the 
>> cohesive one (of which only the flat and non-flat modalities are 
>> exposed to the user) is actually the one that adheres to the 
>> discipline of MTT (by having a third "squash" modality that 
>> effectively removes variables from the context).
>> Both regarding usability and equivalence, do not be misled by the 
>> invasive-looking locks. These locks have two confluent histories:
>> - there is a history of fitch-style logics,
>> - there is a history of modal logics with left-division. When 
>> implementing Menkar, which was intended as a proof assistant for 
>> general multimode systems with left division, I observed at some 
>> point that the left division of all modalities in the context 
>> actually never needs to be computed and can thus be regarded as a 
>> context /constructor/, rather than as an operation (i.e. 
>> admissibility of left division was not required, in none of the 
>> senses of the word mentioned so far). Modal Agda does use an eagerly 
>> computed left division. These systems with left division are very 
>> closely related to dual context systems.
>>
>> I think usability is hard to judge because there isn't yet good tool 
>> support to experiment with. But I believe that it can grow on the 
>> user. A lock simply means "we've moved into a modal subterm". The 
>> position of the lock in the context is important in order to keep 
>> track of which variables were introduced before/after moving into 
>> that modal subterm. When using a variable, you just need to make sure 
>> that the variable's modal annotation is ≤ the composition of the 
>> locks, i.e. the modality of the position where we currently are and 
>> where we want to use the variable.
>>
>> I am happy to discuss this matter further if you have any questions 
>> or doubts.
>>
>> Best regards,
>> Andreas Nuyts
>>
>> On 18.11.22 18:14, Michael Shulman wrote:
>>> That's an interesting question.  I was thinking of operations and 
>>> equalities, and annotations are neither of those, but I can see that 
>>> they're somewhat similar in spirit.  But I find it even more 
>>> difficult to imagine how to define this phenomenon precisely in a 
>>> way that would include them...
>>>
>>> On Fri, Nov 18, 2022 at 8:59 AM Jon Sterling <jon@jonmsterling.com> 
>>> wrote:
>>>
>>>     On 18 Nov 2022, at 11:56, Michael Shulman wrote:
>>>
>>>     > Thanks.  It does sound like we mostly agree.  I would probably
>>>     argue that
>>>     > even for type theories in development, where we don't yet know
>>>     that full
>>>     > definitional equality is decidable -- or intrinsically
>>>     ill-behaved type
>>>     > theories like Lean, or Agda with non-confluent rewrite rules,
>>>     where
>>>     > definitional equality *isn't* decidable -- there is still
>>>     value in being
>>>     > able to reduce just substitutions.  But I think that's a
>>>     relatively minor
>>>     > point.
>>>     >
>>>     > Maybe we can work out some way to use words so that this
>>>     underlying
>>>     > agreement is evident.  For instance, can we find a third word
>>>     to use
>>>     > alongside "admissible" and "derivable" to refer to
>>>     operations/equalities
>>>     > like substitution and its theory, which hold in all reasonable
>>>     models, and
>>>     > can be made admissible in some presentations, but more
>>>     importantly can be
>>>     > eliminated in an equality-checking algorithm?
>>>     >
>>>
>>>     Cool, it's a relief to start getting this cleared up! I really
>>>     agree with you that there is a need for terminology to describe
>>>     the situation you mention, and maybe even more, there is a need
>>>     to define this phenomenon...
>>>
>>>     I wonder if we can think of more concrete examples of this. For
>>>     instance, in many versions of syntax (like bidirectional ones)
>>>     we can choose to drop certain annotations because they will be
>>>     available as part of the flow of information in the elaboration
>>>     algorithm. Would these be an example of the phenomenon you are
>>>     describing, or is it something different?
>>>
>>>     Best,
>>>     Jon
>>>
>>> -- 
>>> You received this message because you are subscribed to the Google 
>>> Groups "Homotopy Type Theory" group.
>>> To unsubscribe from this group and stop receiving emails from it, 
>>> send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
>>> To view this discussion on the web visit 
>>> https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpyohZmqoArApd2vdE%2BGp%2BsVczpw95TDy9xvDnMStMj%3DZQ%40mail.gmail.com 
>>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpyohZmqoArApd2vdE%2BGp%2BsVczpw95TDy9xvDnMStMj%3DZQ%40mail.gmail.com?utm_medium=email&utm_source=footer>.
>>

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/a60dce1b-8ad7-3d07-8232-92a811b3bb62%40gmail.com.

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

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Andreas Nuyts]

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

Actually, I think I disagree on a deeper level:
To say that a model (in the sense of algebraic theories) respects the 
equational theory of a language, does not *only* mean that the 
evaluation of syntactic programs in that model respects equality. It 
also means that the evaluation of programs containing subterms that are 
actually quoted elements from the model, respects equality. 
(Algebraically speaking, the model should be an Eilenberg-Moore-algebra 
for the quotiented version of the term monad.) But since *admissible* 
substitution is undefined for such quoted elements, this cannot be 
stated (the term monad cannot be quotiented satisfactorily).
So while it's true that "you can still check in the admissible-subst 
scenario whether the interpretation function respects the beta law on 
all terms", this is a much weaker property than respecting the 
equational theory of the language.

But I agree that my statement "Prettyprinting indeed disrespects 
βη-equality." made it sound as evidence of something, whereas I was 
merely arguing that it's a drawback that you cannot reasonably complain 
about if you were looking for a model without substitution in the first 
place.

On 01.12.22 16:57, Andreas Nuyts wrote:
> Right, but when looking for a model that misses a substitution 
> operation and is not contrived, you're not going to find it among the 
> models that try to respect equality, because that isn't even statable 
> in the model. When you drop both the requirement of supporting 
> substitution, and of respecting equality, then your search space has 
> grown enough that prettyprinters can be found in it.
>
> On 01.12.22 16:54, Jon Sterling wrote:
>> The issue regarding the beta law is kind of spurious: one of course 
>> states the beta law using the ADMISSIBLE substitution action. The 
>> problem with pretty printing is that it is indeed not satisfying the 
>> beta law but this has absolutely nothing to do with substitution — 
>> you can still check in the admissible-subst scenario whether the 
>> interpretation function respects the beta law on all terms, and in 
>> this case it just happens that it doesn’t.
>>
>>> On Dec 1, 2022, at 3:40 PM, Andreas Nuyts <andreasnuyts@gmail.com> 
>>> wrote:
>>>
>>>  Hi everyone,
>>>
>>> I finally found time to read up on this lengthy conversation.
>>>
>>> Jon wrote:
>>>
>>>     It is revealing that nobody has proposed a notion of **model**
>>>     of type theory in which the admissible structural rules do not
>>>     hold; this would be the necessary form taken by any evidence for
>>>     the thesis that it is important for structural rules to not be
>>>     derivable.
>>>
>>>
>>> I think, on the contrary, that such models are not acknowledged as 
>>> being models, because the language without substitution is in 
>>> general not really the language of interest. An example of a model 
>>> disrespecting substitution is the prettyprinter by Allais, Atkey, 
>>> Chapman, McBride & McKinna (2021):
>>> https://doi.org/10.1017/S0956796820000076
>>> Indeed, substitution is no longer possible after prettyprinting, but 
>>> all other language constructs are supported. Note that if a 
>>> substitution operation is unavailable in a model, then the β-rule 
>>> for functions cannot even be stated in that model, let alone asked 
>>> to hold. So a model that fails to have a substitution operation 
>>> necessarily also disrespects the equational theory of a language 
>>> with such a β-rule. Prettyprinting indeed disrespects βη-equality.
>>>
>>> Mike wrote:
>>>
>>>     MTT is also not equivalent to split-context theories, and IMHO
>>>     is less pleasant to work with in practice.
>>>
>>>
>>> I'm reluctant to postulate here that any split-context theory is 
>>> equivalent to some instance of MTT, but I would be quite surprised 
>>> if you ever face any practical problems when abandoning a 
>>> split-context system in favour of MTT. If you're thinking in 
>>> particular about a system with crisp and non-crisp variables: such a 
>>> system is implemented by Andrea in agda-flat. At the last Agda 
>>> meeting, we have been investigating how mature the current modality 
>>> system in Agda is and how feasible it is to support full MTT. One 
>>> thing we observed is that - of all the parallel modality systems 
>>> implemented in Agda - the cohesive one (of which only the flat and 
>>> non-flat modalities are exposed to the user) is actually the one 
>>> that adheres to the discipline of MTT (by having a third "squash" 
>>> modality that effectively removes variables from the context).
>>> Both regarding usability and equivalence, do not be misled by the 
>>> invasive-looking locks. These locks have two confluent histories:
>>> - there is a history of fitch-style logics,
>>> - there is a history of modal logics with left-division. When 
>>> implementing Menkar, which was intended as a proof assistant for 
>>> general multimode systems with left division, I observed at some 
>>> point that the left division of all modalities in the context 
>>> actually never needs to be computed and can thus be regarded as a 
>>> context /constructor/, rather than as an operation (i.e. 
>>> admissibility of left division was not required, in none of the 
>>> senses of the word mentioned so far). Modal Agda does use an eagerly 
>>> computed left division. These systems with left division are very 
>>> closely related to dual context systems.
>>>
>>> I think usability is hard to judge because there isn't yet good tool 
>>> support to experiment with. But I believe that it can grow on the 
>>> user. A lock simply means "we've moved into a modal subterm". The 
>>> position of the lock in the context is important in order to keep 
>>> track of which variables were introduced before/after moving into 
>>> that modal subterm. When using a variable, you just need to make 
>>> sure that the variable's modal annotation is ≤ the composition of 
>>> the locks, i.e. the modality of the position where we currently are 
>>> and where we want to use the variable.
>>>
>>> I am happy to discuss this matter further if you have any questions 
>>> or doubts.
>>>
>>> Best regards,
>>> Andreas Nuyts
>>>
>>> On 18.11.22 18:14, Michael Shulman wrote:
>>>> That's an interesting question.  I was thinking of operations and 
>>>> equalities, and annotations are neither of those, but I can see 
>>>> that they're somewhat similar in spirit.  But I find it even more 
>>>> difficult to imagine how to define this phenomenon precisely in a 
>>>> way that would include them...
>>>>
>>>> On Fri, Nov 18, 2022 at 8:59 AM Jon Sterling <jon@jonmsterling.com> 
>>>> wrote:
>>>>
>>>>     On 18 Nov 2022, at 11:56, Michael Shulman wrote:
>>>>
>>>>     > Thanks.  It does sound like we mostly agree.  I would
>>>>     probably argue that
>>>>     > even for type theories in development, where we don't yet
>>>>     know that full
>>>>     > definitional equality is decidable -- or intrinsically
>>>>     ill-behaved type
>>>>     > theories like Lean, or Agda with non-confluent rewrite rules,
>>>>     where
>>>>     > definitional equality *isn't* decidable -- there is still
>>>>     value in being
>>>>     > able to reduce just substitutions.  But I think that's a
>>>>     relatively minor
>>>>     > point.
>>>>     >
>>>>     > Maybe we can work out some way to use words so that this
>>>>     underlying
>>>>     > agreement is evident.  For instance, can we find a third word
>>>>     to use
>>>>     > alongside "admissible" and "derivable" to refer to
>>>>     operations/equalities
>>>>     > like substitution and its theory, which hold in all
>>>>     reasonable models, and
>>>>     > can be made admissible in some presentations, but more
>>>>     importantly can be
>>>>     > eliminated in an equality-checking algorithm?
>>>>     >
>>>>
>>>>     Cool, it's a relief to start getting this cleared up! I really
>>>>     agree with you that there is a need for terminology to describe
>>>>     the situation you mention, and maybe even more, there is a need
>>>>     to define this phenomenon...
>>>>
>>>>     I wonder if we can think of more concrete examples of this. For
>>>>     instance, in many versions of syntax (like bidirectional ones)
>>>>     we can choose to drop certain annotations because they will be
>>>>     available as part of the flow of information in the elaboration
>>>>     algorithm. Would these be an example of the phenomenon you are
>>>>     describing, or is it something different?
>>>>
>>>>     Best,
>>>>     Jon
>>>>
>>>> -- 
>>>> You received this message because you are subscribed to the Google 
>>>> Groups "Homotopy Type Theory" group.
>>>> To unsubscribe from this group and stop receiving emails from it, 
>>>> send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
>>>> To view this discussion on the web visit 
>>>> https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpyohZmqoArApd2vdE%2BGp%2BsVczpw95TDy9xvDnMStMj%3DZQ%40mail.gmail.com 
>>>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpyohZmqoArApd2vdE%2BGp%2BsVczpw95TDy9xvDnMStMj%3DZQ%40mail.gmail.com?utm_medium=email&utm_source=footer>.
>>>
>

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/74bff49b-91b0-8b55-5cb1-10ce815ce470%40gmail.com.

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

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[Michael Shulman]

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

On Thu, Dec 1, 2022 at 6:40 AM Andreas Nuyts <andreasnuyts@gmail.com> wrote:

> I think usability is hard to judge because there isn't yet good tool
> support to experiment with. But I believe that it can grow on the user. A
> lock simply means "we've moved into a modal subterm". The position of the
> lock in the context is important in order to keep track of which variables
> were introduced before/after moving into that modal subterm. When using a
> variable, you just need to make sure that the variable's modal annotation
> is ≤ the composition of the locks, i.e. the modality of the position where
> we currently are and where we want to use the variable.
>

This is a reasonable point.

I do think, however, that tool support is not necessary to evaluate
usability.  A really usable theory should also be usable informally, as in
the HoTT Book and my BFP paper.  This is what I have trouble with for
locking modal type theories; but it's certainly possible that I could train
myself to do it.  It certainly takes some mental training to use
split-context modal type theories informally too.

A more serious and mathematical issue is that MTT requires all modalities
to be right adjoints, semantically, because you have to have some operation
to interpret the locking functors on contexts.  (And FitchTT even requires
those left adjoints to themselves be (parametric) right adjoints.)  This
seems a serious restriction on the kinds of situations we can model.

One can argue that the process of interpreting a split-context theory
involves building a new category of contexts (some generalized kind of
comma category, perhaps) that *does* interpret such context operations, and
therefore could also interpret MTT.  But we don't have a general theory of
this yet.

To be precise, given an arbitrary 2-category M of modes, I would like there
to be a corresponding instance of a general modal type theory that can be
interpreted in any M-shaped diagram of suitable categories, with all the
morphisms of M corresponding to syntactic modalities, and not requiring the
existence of any additional adjoints in the semantics.  The LSR fibrational
framework achieves this for simple type theories, but I don't think there
is any published framework that achieves it for dependent type theories.

Best,
Mike

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpzCJLHMmB4ZPCX8Cn0_agLcD5_UZ1KsAkZZ8m0bLqHGKA%40mail.gmail.com.

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

Re: [HoTT] Question about the formal rules of cohesive homotopy type theory

[andrej.bauer]

I am sorry I started such a long conversation about so little.

Of course one needs to distinguish structures from presentations of structures, which can be done without promoting one's personal preferences as value judgements about the 20th century type theories.

Mike already explained why presentations are important. Thank you.

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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/13907424-5B03-4804-AC89-33DC5466F497%40andrej.com.