From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Fri, 18 May 2018 14:03:30 -0700 (PDT) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <55fca524-24be-4f98-b9a4-fa4846d9c51c@googlegroups.com> In-Reply-To: References: <4f23688f-af7c-43cb-946c-988f9d476848@googlegroups.com> Subject: Re: [HoTT] Univalence <-> equivalence induction MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_8770_1029928689.1526677410169" ------=_Part_8770_1029928689.1526677410169 Content-Type: multipart/alternative; boundary="----=_Part_8771_1317322196.1526677410169" ------=_Part_8771_1317322196.1526677410169 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On Friday, 18 May 2018 17:41:00 UTC+2, Michael Shulman wrote: > > I certainly knew that univalence is equivalent to=20 > equivalence-induction *with* computation rule, which I think is what=20 > is in Egbert's notes. But I don't think I knew that you can do=20 > without the computation rule. =20 Yes, this is the difference - or are you doing the same, Egbert? Also, I should have said that I needed to adapt Peter's argument slightly -= =20 unfortunately, I couldn't use his result off-the-shelf. The main difference= =20 is that Peter works with a global identity system on all types (of a=20 universe), whereas I work with an identity system on a single type, namely= =20 a universe. As a result, I can't define the type of left-cancellable maps= =20 using the notion of equality given by the identity system. Instead, I=20 define it using the native (Martin-Loef) identity type, and with this=20 little modification, Peter's argument goes through for the situation=20 considered here. Can you give a link to the "some years=20 > ago" discussion claiming it strictly weaker?=20 > I will try to dig it up tomorrow. Martin =20 > > On Fri, May 18, 2018 at 6:04 AM, Egbert Rijke > wrote:=20 > > Hi Martin,=20 > >=20 > > I think it was known. I taught this in my intro to HoTT class this=20 > semester:=20 > >=20 > > http://www.andrew.cmu.edu/user/erijke/hott/univalence.pdf=20 > >=20 > > Best wishes,=20 > > Egbert=20 > >=20 > > On Fri, May 18, 2018 at 2:36 AM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3= =20 > > > wrote:=20 > >>=20 > >> Equivalence induction says that in order to prove something for all=20 > >> equivalences, it is enough to prove it for all identity equivalences= =20 > for all=20 > >> types.=20 > >>=20 > >> This follows from univalence. But also, conversely, univalence follows= =20 > >> from it:=20 > >>=20 > >> http://www.cs.bham.ac.uk/~mhe/agda-new/UF-Univalence.html#JEq=20 > >>=20 > >> Is this known? Some years ago it was claimed in this list that=20 > equivalence=20 > >> induction would be strictly weaker than univalence.=20 > >>=20 > >> To prove the above, I apply a technique I learned from Peter Lumsdaine= ,=20 > >> that given an abstract identity system (Id, refl , J) with no given=20 > >> "computation rule" for J, produces another identity system (Id, refl ,= =20 > J' ,=20 > >> J'-comp) with=20 > >> a "propositional computation rule" J'-comp for J'.=20 > >>=20 > >> http://www.cs.bham.ac.uk/~mhe/agda-new/Lumsdaine.html=20 > >>=20 > >> Martin=20 > >>=20 > >> --=20 > >> You received this message because you are subscribed to the Google=20 > Groups=20 > >> "Homotopy Type Theory" group.=20 > >> To unsubscribe from this group and stop receiving emails from it, send= =20 > an=20 > >> email to HomotopyTypeThe...@googlegroups.com .=20 > > >> For more options, visit https://groups.google.com/d/optout.=20 > >=20 > >=20 > >=20 > >=20 > > --=20 > > egbertrijke.com=20 > >=20 > > --=20 > > You received this message because you are subscribed to the Google=20 > Groups=20 > > "Homotopy Type Theory" group.=20 > > To unsubscribe from this group and stop receiving emails from it, send= =20 > an=20 > > email to HomotopyTypeThe...@googlegroups.com .=20 > > For more options, visit https://groups.google.com/d/optout.=20 > ------=_Part_8771_1317322196.1526677410169 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
On Friday, 18 May 2018 17:41:00 UTC+2, Michael Shulman wr= ote:
I certainly knew that univ= alence is equivalent to
equivalence-induction *with* computation rule, which I think is what
is in Egbert's notes. =C2=A0But I don't think I knew that you c= an do
without the computation rule. =C2=A0

Ye= s, this is the difference - or are you doing the same, Egbert?
Also, I should have said that I needed to adapt Peter's ar= gument slightly - unfortunately, I couldn't use his result off-the-shel= f. The main difference is that Peter works with a global identity system on= all types (of a universe), whereas I work with an identity system on a sin= gle type, namely a universe. As a result, I can't define the type of le= ft-cancellable maps using the notion of equality given by the identity syst= em. Instead, I define it using the native (Martin-Loef) identity type, and = with this little modification, Peter's argument goes through for the si= tuation considered here.

Can you give a link to the "some years
ago" discussion claiming it strictly weaker?

I will try to dig it up tomorrow.

Martin
=C2=A0

On Fri, May 18, 2018 at 6:04 AM, Egbert Rijke <e.m...@gmail.com> w= rote:
> Hi Martin,
>
> I think it was known. I taught this in my intro to HoTT class this= semester:
>
> http://www.andrew.cmu.edu/user/erijke/h= ott/univalence.pdf
>
> Best wishes,
> Egbert
>
> On Fri, May 18, 2018 at 2:36 AM, Mart=C3=ADn H=C3=B6tzel Escard=C3= =B3
> <escar...@gmail.com> wrote:
>>
>> Equivalence induction says that in order to prove something fo= r all
>> equivalences, it is enough to prove it for all identity equiva= lences for all
>> types.
>>
>> This follows from univalence. But also, conversely, univalence= follows
>> from it:
>>
>> =C2=A0 =C2=A0http://www.cs.b= ham.ac.uk/~mhe/agda-new/UF-Univalence.html#JEq
>>
>> Is this known? Some years ago it was claimed in this list that= equivalence
>> induction would be strictly weaker than univalence.
>>
>> To prove the above, I apply a technique I learned from Peter L= umsdaine,
>> that given an abstract identity system (Id, refl , J) with no = given
>> "computation rule" for J, produces another identity = system (Id, refl , J' ,
>> J'-comp) with
>> a "propositional computation rule" J'-comp for J= '.
>>
>> =C2=A0 =C2=A0http://www.cs.bham.ac.uk/~mhe/agda-new= /Lumsdaine.html
>>
>> Martin
>>
>> --
>> You received this message because you are subscribed to the Go= ogle Groups
>> "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from = it, send an
>> email to HomotopyTypeTheory+unsub...@googlegroups.com.
>> For more options, visit https://group= s.google.com/d/optout.
>
>
>
>
> --
> egbertrijke.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+unsub...@googlegroups.com.
> For more options, visit https://groups.go= ogle.com/d/optout.
------=_Part_8771_1317322196.1526677410169-- ------=_Part_8770_1029928689.1526677410169--