FOMUS slides

FOMUS slides

[Vladimir Voevodsky]

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

Hello,

the slides of my FOMUS talk that have started the discussion about equalities are now available at my website https://www.math.ias.edu/vladimir/lectures <https://www.math.ias.edu/vladimir/lectures> .

Vladimir.


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

[-- Attachment #2: Message signed with OpenPGP using GPGMail --]
[-- Type: application/pgp-signature, Size: 507 bytes --]

Re: [HoTT] FOMUS slides

[Michael Shulman]

Can you explain the idea on the last slide a little more?  Did you
actually mean to say that R and "transportb0 R e" both have type P2,
or should one of them have had type P1?  If the latter, then how can
we tell what type(s) "transportb0 R e" is allowed to have based on
knowing the types of R and e?

On Tue, Jul 19, 2016 at 2:18 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> Hello,
>
> the slides of my FOMUS talk that have started the discussion about
> equalities are now available at my website
> https://www.math.ias.edu/vladimir/lectures .
>
> Vladimir.
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

Re: [HoTT] FOMUS slides

[Vladimir Voevodsky]

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

Thank you for spotting this typo. It is supposed to be P_1. I have corrected the slides.


> On Jul 19, 2016, at 8:16 PM, Michael Shulman <shu...@sandiego.edu> wrote:
> 
> Can you explain the idea on the last slide a little more?  Did you
> actually mean to say that R and "transportb0 R e" both have type P2,
> or should one of them have had type P1?  If the latter, then how can
> we tell what type(s) "transportb0 R e" is allowed to have based on
> knowing the types of R and e?
> 
> On Tue, Jul 19, 2016 at 2:18 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
>> Hello,
>> 
>> the slides of my FOMUS talk that have started the discussion about
>> equalities are now available at my website
>> https://www.math.ias.edu/vladimir/lectures .
>> 
>> Vladimir.
>> 
>> --
>> You received this message because you are subscribed to the Google Groups
>> "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to HomotopyTypeThe...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
> 
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.


[-- Attachment #2: Message signed with OpenPGP using GPGMail --]
[-- Type: application/pgp-signature, Size: 507 bytes --]

Re: [HoTT] FOMUS slides

[Michael Shulman]

Okay, so then suppose I have e:Id0 T A B and R:P2.  What is the type
of transportb0 R e?

On Tue, Jul 19, 2016 at 4:28 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> Thank you for spotting this typo. It is supposed to be P_1. I have corrected the slides.
>
>
>> On Jul 19, 2016, at 8:16 PM, Michael Shulman <shu...@sandiego.edu> wrote:
>>
>> Can you explain the idea on the last slide a little more?  Did you
>> actually mean to say that R and "transportb0 R e" both have type P2,
>> or should one of them have had type P1?  If the latter, then how can
>> we tell what type(s) "transportb0 R e" is allowed to have based on
>> knowing the types of R and e?
>>
>> On Tue, Jul 19, 2016 at 2:18 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
>>> Hello,
>>>
>>> the slides of my FOMUS talk that have started the discussion about
>>> equalities are now available at my website
>>> https://www.math.ias.edu/vladimir/lectures .
>>>
>>> Vladimir.
>>>
>>> --
>>> You received this message because you are subscribed to the Google Groups
>>> "Homotopy Type Theory" group.
>>> To unsubscribe from this group and stop receiving emails from it, send an
>>> email to HomotopyTypeThe...@googlegroups.com.
>>> For more options, visit https://groups.google.com/d/optout.
>>
>> --
>> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

Re: [HoTT] FOMUS slides

[Andrew Polonsky]

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

A couple of years ago, I have experimented with a system based on a similar 
idea.  See page 7 here:

https://dl.dropboxusercontent.com/u/7730626/ett3.pdf

The reduction rules for transporting over a type equality e : A ≈ B can 
indeed be defined purely by induction on e, as on page 9.  (And, if you 
want to add univalence, then equivalence will be a constructor for this 
type, in which case the transport will reduce to the function given in this 
constructor.)

Cheers,
Andrew

On Tuesday, July 19, 2016 at 9:28:14 PM UTC+2, v v wrote:
>
> Thank you for spotting this typo. It is supposed to be P_1. I have 
> corrected the slides. 
>
>
> > On Jul 19, 2016, at 8:16 PM, Michael Shulman <shu...@sandiego.edu 
> <javascript:>> wrote: 
> > 
> > Can you explain the idea on the last slide a little more?  Did you 
> > actually mean to say that R and "transportb0 R e" both have type P2, 
> > or should one of them have had type P1?  If the latter, then how can 
> > we tell what type(s) "transportb0 R e" is allowed to have based on 
> > knowing the types of R and e? 
> > 
> > On Tue, Jul 19, 2016 at 2:18 PM, Vladimir Voevodsky <vla...@ias.edu 
> <javascript:>> wrote: 
> >> Hello, 
> >> 
> >> the slides of my FOMUS talk that have started the discussion about 
> >> equalities are now available at my website 
> >> https://www.math.ias.edu/vladimir/lectures . 
> >> 
> >> Vladimir. 
> >> 
> >> -- 
> >> You received this message because you are subscribed to the Google 
> Groups 
> >> "Homotopy Type Theory" group. 
> >> To unsubscribe from this group and stop receiving emails from it, send 
> an 
> >> email to HomotopyTypeThe...@googlegroups.com <javascript:>. 
>
> >> For more options, visit https://groups.google.com/d/optout. 
> > 
> > -- 
> > You received this message because you are subscribed to the Google 
> Groups "Homotopy Type Theory" group. 
> > To unsubscribe from this group and stop receiving emails from it, send 
> an email to HomotopyTypeThe...@googlegroups.com <javascript:>. 
>
> > For more options, visit https://groups.google.com/d/optout. 
>
>

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

a new transport rule

[Vladimir Voevodsky]

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

What I wrote with words on the last slide is best expressed, I think, by the following rule, where I omit the Gamma in front of each line:

T type
A:T
B:T
X:T |- P top
P[A/X] type
P[B/X] type
R:P[B/X]
e:Id0 T A B
————————
trb0(R,*e,*X.P,*A,*B,*T):P[A/X]

where

"P top” signifies that P is a syntactically correct type expression but need not be well-formed (well typed, derivable) in Gamma,

the “*” in front of an argument as in “ *e “ signifies a non-essential argument, such arguments are ignored when two expressions are compared for alpha-equivalence.

This is semantically acceptable if Id0 is interpreted as exact equality.

Syntactically we have the case when the well-formed sentences form something like an ideal in a ring because one operation has as one of its arguments an element of the ambient structure (raw typing judgements).

This came out stranger than I expected.

Vladimir.


[-- Attachment #2: Message signed with OpenPGP using GPGMail --]
[-- Type: application/pgp-signature, Size: 507 bytes --]

Re: [HoTT] a new transport rule

[Michael Shulman]

Can you give an example of such a P which becomes well-formed when A
and B are substituted for X but is not well-formed with X as a
variable?

On Wed, Jul 20, 2016 at 5:44 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> What I wrote with words on the last slide is best expressed, I think, by the following rule, where I omit the Gamma in front of each line:
>
> T type
> A:T
> B:T
> X:T |- P top
> P[A/X] type
> P[B/X] type
> R:P[B/X]
> e:Id0 T A B
> ————————
> trb0(R,*e,*X.P,*A,*B,*T):P[A/X]
>
> where
>
> "P top” signifies that P is a syntactically correct type expression but need not be well-formed (well typed, derivable) in Gamma,
>
> the “*” in front of an argument as in “ *e “ signifies a non-essential argument, such arguments are ignored when two expressions are compared for alpha-equivalence.
>
> This is semantically acceptable if Id0 is interpreted as exact equality.
>
> Syntactically we have the case when the well-formed sentences form something like an ideal in a ring because one operation has as one of its arguments an element of the ambient structure (raw typing judgements).
>
> This came out stranger than I expected.
>
> Vladimir.
>
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

Re: [HoTT] a new transport rule

[Andrej Bauer]

On Wed, Jul 20, 2016 at 11:10 AM, Michael Shulman <shu...@sandiego.edu> wrote:
> Can you give an example of such a P which becomes well-formed when A
> and B are substituted for X but is not well-formed with X as a
> variable?

Let

 T := Universe

  nat : Universe
  Nat type
  El nat = Nat
  42 : Nat

 P(X) := Id (El X) 42 42

Then P(nat) is well-formed, but P(X) is not. Or, if you dislike universes:

 T := bool

  P(X) := Id (match X with true => Nat | false => (Nat -> Nat) end) 42 42

Now P(true) is well formed, but P(X) is not.

With kind regards,

Andrej

Re: [HoTT] a new transport rule

[Michael Shulman]

Thanks!  I see.

But I must admit I don't immediately see a use for such a transport
rule (or how to give it any semantics).

On Fri, Jul 22, 2016 at 7:00 AM, Andrej Bauer <andrej...@andrej.com> wrote:
> On Wed, Jul 20, 2016 at 11:10 AM, Michael Shulman <shu...@sandiego.edu> wrote:
>> Can you give an example of such a P which becomes well-formed when A
>> and B are substituted for X but is not well-formed with X as a
>> variable?
>
> Let
>
>  T := Universe
>
>   nat : Universe
>   Nat type
>   El nat = Nat
>   42 : Nat
>
>  P(X) := Id (El X) 42 42
>
> Then P(nat) is well-formed, but P(X) is not. Or, if you dislike universes:
>
>  T := bool
>
>   P(X) := Id (match X with true => Nat | false => (Nat -> Nat) end) 42 42
>
> Now P(true) is well formed, but P(X) is not.
>
> With kind regards,
>
> Andrej
>
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

Re: [HoTT] a new transport rule

[andré hirschowitz]

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

I looked for an example without universe/El  and found

P(X) ;= forall p: Id X a, Id p (refl a).

It seems that the formula must involve a "type from term constructor"
(here Id, or there El).

andré

2016-07-22 12:00 GMT+02:00 Andrej Bauer <andrej...@andrej.com>:

> On Wed, Jul 20, 2016 at 11:10 AM, Michael Shulman <shu...@sandiego.edu>
> wrote:
> > Can you give an example of such a P which becomes well-formed when A
> > and B are substituted for X but is not well-formed with X as a
> > variable?
>
> Let
>
>  T := Universe
>
>   nat : Universe
>   Nat type
>   El nat = Nat
>   42 : Nat
>
>  P(X) := Id (El X) 42 42
>
> Then P(nat) is well-formed, but P(X) is not. Or, if you dislike universes:
>
>  T := bool
>
>   P(X) := Id (match X with true => Nat | false => (Nat -> Nat) end) 42 42
>
> Now P(true) is well formed, but P(X) is not.
>
> With kind regards,
>
> Andrej
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>

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

Re: [HoTT] a new transport rule

[Vladimir Voevodsky]

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

The semantics is the strict equality.

> On Jul 22, 2016, at 2:08 PM, Michael Shulman <shu...@sandiego.edu> wrote:
> 
> Thanks!  I see.
> 
> But I must admit I don't immediately see a use for such a transport
> rule (or how to give it any semantics).
> 
> On Fri, Jul 22, 2016 at 7:00 AM, Andrej Bauer <andrej...@andrej.com> wrote:
>> On Wed, Jul 20, 2016 at 11:10 AM, Michael Shulman <shu...@sandiego.edu> wrote:
>>> Can you give an example of such a P which becomes well-formed when A
>>> and B are substituted for X but is not well-formed with X as a
>>> variable?
>> 
>> Let
>> 
>> T := Universe
>> 
>>  nat : Universe
>>  Nat type
>>  El nat = Nat
>>  42 : Nat
>> 
>> P(X) := Id (El X) 42 42
>> 
>> Then P(nat) is well-formed, but P(X) is not. Or, if you dislike universes:
>> 
>> T := bool
>> 
>>  P(X) := Id (match X with true => Nat | false => (Nat -> Nat) end) 42 42
>> 
>> Now P(true) is well formed, but P(X) is not.
>> 
>> With kind regards,
>> 
>> Andrej
>> 
>> --
>> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
> 
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.


[-- Attachment #2: Message signed with OpenPGP using GPGMail --]
[-- Type: application/pgp-signature, Size: 507 bytes --]