From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Mon, 23 Mar 2020 02:54:13 -0700 (PDT) From: Ambrus Kaposi To: Homotopy Type Theory Message-Id: In-Reply-To: References: Subject: =?UTF-8?Q?Re:_[HoTT]_What_is_known_and/or_wri?= =?UTF-8?Q?tten_about_=E2=80=9CFrobenius_eliminators=E2=80=9D=3F?= MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1158_787394512.1584957253591" ------=_Part_1158_787394512.1584957253591 Content-Type: multipart/alternative; boundary="----=_Part_1159_945636576.1584957253591" ------=_Part_1159_945636576.1584957253591 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Hi, Sorry for resurrecting an old thread, I just wanted to document that=20 Frobenius J can be derived from Paulin-Mohring J without Pi, Sigma or=20 universes:=20 https://github.com/akaposi/hiit-signatures/blob/master/formalization/Froben= iusJDeriv.agda This was observed by Rafael Bocquet and Andr=C3=A1s Kov=C3=A1cs in October = 2019, but=20 maybe other people have known about this. We mention this briefly in our paper on HIIT signatures where=20 Paulin-Mohring J can be used on previous equality constructors but we don't= =20 have Pi, Sigma or (usual) universes: https://lmcs.episciences.org/6100 Cheers, Ambrus 2018. j=C3=BAlius 13., p=C3=A9ntek 13:05:47 UTC+2 id=C5=91pontban Valery Is= aev a=20 k=C3=B6vetkez=C5=91t =C3=ADrta: > > > 2018-07-13 13:38 GMT+03:00 Peter LeFanu Lumsdaine >: > >> On Thu, Jul 12, 2018 at 7:07 PM Valery Isaev > > wrote: >> >>> Hi Peter, >>> >>> I've been thinking about such eliminators lately too. It seems that the= y=20 >>> are derivable from ordinary eliminator for most type-theoretic=20 >>> constructions as long as we have identity types and sigma types.=20 >>> >> >> Thankyou =E2=80=94 very nice observation, and (at least to me) quite sur= prising! >> > > I was surprised too. The case of coproducts is especially unexpected. > =20 > >> =20 >> >>> I mean a strong version of Id: >>> >> >> Side note: this is I think more widely known as the Paulin-Mohring or=20 >> one-sided eliminator for Id-types; the HoTT book calls it based=20 >> path-induction. >> >> The fact that the Frobenius version is strictly stronger is known in=20 >>>> folklore, but not written up anywhere I know of. One way to show this= is=20 >>>> to take any non right proper model category (e.g. the model structure = for=20 >>>> quasi-categories on simplicial sets), and take the model of given by i= ts=20 >>>> (TC,F) wfs; this will model the simple version of Id-types but not the= =20 >>>> Frobenius version. >>>> >>>> Are you sure this is true? It seems that we can interpret the strong= =20 >>> version of J even in non right proper model categories. Then the argume= nt I=20 >>> gave above shows that the Frobenius version is also definable. >>> >> >> Ah, yes =E2=80=94 there was a mistake in the argument I had in mind. In= that=20 >> case, do we really know for sure that the Frobenius versions are really= =20 >> strictly stronger? >> >> I don't know how to prove this, but it seems that we can't even define= =20 > transport without Frobenius J. Also, if we do have transport and we know= =20 > that types of the form \Sigma (x : A) Id(a,x) are contractible, then the= =20 > "one-sided J" is definable, so if we want to prove that the Frobenius=20 > version does not follows from the non-Frobenius, we need to find a model= =20 > where either transport is not definable or \Sigma (x : A) Id(a,x) is not= =20 > contractible. > =20 > >> =E2=80=93p. >> >> >> > ------=_Part_1159_945636576.1584957253591 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Hi,

Sorry for resurrecting a= n old thread, I just wanted to document that Frobenius J can be derived fro= m Paulin-Mohring J without Pi, Sigma or universes: https://github.com/akapo= si/hiit-signatures/blob/master/formalization/FrobeniusJDeriv.agda
This was observed by Rafael Bocquet and Andr=C3=A1s Kov=C3=A1cs in October= 2019, but maybe other people have known about this.

We mention this briefly in our paper on HIIT signatures where Paulin= -Mohring J can be used on previous equality constructors but we don't h= ave Pi, Sigma or (usual) universes: https://lmcs.episciences.org/6100
=

Cheers,
Ambrus

2018. j=C3= =BAlius 13., p=C3=A9ntek 13:05:47 UTC+2 id=C5=91pontban Valery Isaev a k=C3= =B6vetkez=C5=91t =C3=ADrta:

2018-07-13 13:38 GMT+03:0= 0 Peter LeFanu Lumsdaine <p...@gmail.com>:
O= n Thu, Jul 12, 2018 at 7:07 PM Valery Isaev <va...@gmail.com> wrote:
Hi Peter,

I've bee= n thinking about such eliminators lately too. It seems that they are deriva= ble from ordinary eliminator for most type-theoretic constructions as long = as we have identity types and sigma types.
Thankyou =E2=80=94 very nice observation, and (at least= to me) quite surprising!

I was surprised too. The case of coproducts is especially unexpected.
=C2=A0
=C2=A0
I mean a strong ve= rsion of Id:

Side note: = this is I think more widely known as the Paulin-Mohring or one-sided elimin= ator for Id-types; the HoTT book calls it based path-induction.
=

The fact that the Frobenius version is str= ictly stronger is known in folklore, but not written up anywhere I know of.= =C2=A0 One way to show this is to take any non right proper model category = (e.g. the model structure for quasi-categories on simplicial sets), and tak= e the model of given by its (TC,F) wfs; this will model the simple version = of Id-types but not the Frobenius version.

A= re you sure this is true? It seems that we can interpret the strong version= of J even in non right proper model categories. Then the argument I gave a= bove shows that the Frobenius version is also definable.
<= /div>

Ah, yes =E2=80=94 there was a = mistake in the argument I had in mind.=C2=A0 In that case, do we really kno= w for sure that the Frobenius versions are really strictly stronger?
<= span>

I don't know how to prove this, but it seems that we can&#= 39;t even define transport without Frobenius J. Also, if we do have transpo= rt and we know that types of the form \Sigma (x : A) Id(a,x) are contractib= le, then the "one-sided J" is definable, so if we want to prove t= hat the Frobenius version does not follows from the non-Frobenius, we need = to find a model where either transport is not definable or \Sigma (x : A) I= d(a,x) is not contractible.
=C2=A0
=
=E2=80=93p.



------=_Part_1159_945636576.1584957253591-- ------=_Part_1158_787394512.1584957253591--