From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,HTML_MESSAGE,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE, UNPARSEABLE_RELAY autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 2060 invoked from network); 16 May 2020 08:34:45 -0000 Received: from mail-wm1-x340.google.com (2a00:1450:4864:20::340) by inbox.vuxu.org with ESMTPUTF8; 16 May 2020 08:34:45 -0000 Received: by mail-wm1-x340.google.com with SMTP id q5sf2391921wmc.9 for ; Sat, 16 May 2020 01:34:45 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1589618085; cv=pass; d=google.com; s=arc-20160816; b=hXJv2xPru12oBAKLOwCA+DKmLfxW8uPLtCFteKALKQDEjN+r/Y+DIEVxvVJvCKTncq c49cEEfeRLwYLXEcprGacbdSQlQH57ZOQ4BCfeYjjZBvUUP+/cBIIRUtRB+HXw8qH5P2 LHGC9lzvZuThL0q+LJ+GonRd4ZSs2L6Cl70E7LL065QJN2ln67aLEEl/nl3NzDk21Eaw JXBtnAM7TWQr7hDH3kne06go95RiydeOAPO1uCeWWcJiAKIOYWCbYeael8KaBPIz4rK1 /0t++CESEe58G7+PuRLoy5/qn3pWyjey+CVm9XY+psRPnpDD7ssCv7AwzVIv42FXv6wC 9w/w== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:content-language:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject:sender :dkim-signature; bh=xnO23zQ+7Vcu70sXwCc/PBXdP68RqaHSwX8i7Eot/+4=; b=rZu7Ui9MqA3O3sPjxPf0eoyg9Ujewn1q9pfD5408id8KOsDmM2HSWIq1fOhDh5awRH rrHfp6PX/5fEuiid77OVr/Yv68dQw+DAEs6BLlYsYbge/j0YM/IppXN2X7os43UJAj95 UE0fkoJIg66RWLnBOIT2mTEvXQgQ9b718HsxNUru9G1SgWBpqAqdKO2KOsI1Ia8iTy3V Mu6e4aa8eDf7UmPuOqTK4vafd+lD+3lpZ2gFBvoIUl/t4FtQ+ZDmtgnu6eDpEyAoRcbd kLxQfXZjaW5oRfY04AXrAzC/hd4EUMGbT0il2cuL2BqCeviMc5qK+elhHu5Ep86nDx0I 4Wpg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@ens.fr header.s=default header.b=UCgzfDYE; spf=pass (google.com: domain of rafael.bocquet@ens.fr designates 129.199.96.40 as permitted sender) smtp.mailfrom=rafael.bocquet@ens.fr DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:subject:to:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=xnO23zQ+7Vcu70sXwCc/PBXdP68RqaHSwX8i7Eot/+4=; b=QartdwtmyLZrIu+Y0OHBKl4w4fmP9925sAQ8fWecWvktlG7HwRH2Gz2F6kVgbhYghj Yg4NCfWU0/WNjLf77OijMcp4ddANMzx3ZGsRhVofQTQJTPkCpjjlqXjKE1yhIGvj1Aii rYmXN7esl8t3EUg9uUBFhVxTpj6SACw9bzqw2ztHghTx5F9C3EzsWIA/jT5UiIC6D6AH BwzWKVu6c4VNQFh7hE7VHfpPmRLAxXyTSBsz3UHIeriQhI/Go9/H36pVDmTML97OvaZ7 wP9MrOADkAX1Up90hPs+9qnwZ5HQq7igyr165zAH0mjFziVGM3sTKNfQIsa1oPt8wC0O fRhg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:subject:to:references:from:message-id :date:user-agent:mime-version:in-reply-to:content-language :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=xnO23zQ+7Vcu70sXwCc/PBXdP68RqaHSwX8i7Eot/+4=; b=ONSm7xmbrD13fMgaDru+NCYQkn5tqpbsGFpTk00ekM58EhxdDgU13g5rhv/AiWJg5n djEA0eIk441Q0bU1+sGOYEs85IokHdcgvzST04RtWjy3y48sgCZWUnX/QBwenuc9/VMo vk/0h4c3EILFYpdEoLcRjcdluIx6ZZ4cJSSa+aJIO9mNx9x1n61bRFwc0YclgBQ9yF72 SboKCf+LBvyLe3NS0dZGqnKEVbMguNOXqeALJ/DJy7BRfExTG9GdWLTOLTsezxyD3IAe 4ARjtON597FGeFjJROjOnwtw1/jdAXjS632Ym9q8TCu5bR3pedVKzPRF+PcfUnYY1zUy Vxww== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM5335coaPlZ+/33d1U9KwC3Uh6ewNW94WpEcfIqMSO65n+8BMPpOg 62Hl/frzE9TIQ96j3pyRqq8= X-Google-Smtp-Source: ABdhPJzlvRX2lqHiC2I8ZxvNWyOQ1+w6M7GwhnVhwe5mpbnqMCAzd6jxkb4w5YW20Qnf64CxZXw5gQ== X-Received: by 2002:a1c:2d14:: with SMTP id t20mr8497035wmt.28.1589618084862; Sat, 16 May 2020 01:34:44 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:adf:b441:: with SMTP id v1ls1854193wrd.3.gmail; Sat, 16 May 2020 01:34:44 -0700 (PDT) X-Received: by 2002:a05:6000:146:: with SMTP id r6mr8931041wrx.9.1589618084293; Sat, 16 May 2020 01:34:44 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589618084; cv=none; d=google.com; s=arc-20160816; b=kOKG6q8e9sPAzcWTISAXu5Yoi7Dy2qYkq4SUpYAyJBnNTHNdUK7hyliRqEU7uw3Rku DdZBmHYn9F0J1ax9hYnoLBpGsYmk6QhdJ6tVa67mTWz9SwVbeU+ra78ouMkTdmR6G9hp vbnqcFSYtRRo6yfGjfWrDmC7NcFWRcwoi/NVRSu1+4zBvCTX97uSUVvToUkAP8hRmtab iO0VS9fQMfXwvyuQL/dkwR8QiNZRauHyQ7NWULwWCgSSzd1FfPDBg2QchDDArwLH9vCe TOXflzD978qi+oM2SWnOjFf3JvnmA/aCEx7wUExsa7E0MEkNTGN60zxbj8y2n+rr1x2M e7DA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:in-reply-to:mime-version:user-agent:date :message-id:from:references:to:subject:dkim-signature; bh=P2PEDzviq4jyfzOSM29+Qz3NpsVw7G4P6LdzNNDdFTA=; b=plzMfE3kWRncRN7q2A4c5xsstZDkNaymzahrP++Iv36B65k/eu2WcbxCq7icRIEW1j tX3PiYMcApt0miG+eAkLuszMmzNvL5gTxfnE1VR+u7BYw6Y4/Ya4aaaD6DfObhcRFQ4R /MO6uVaPRUo16tsgjDDVNrKRztJHCGaWQOfBsslFkhqUYkAqaQax8NIm466GoYScYBhm pjmEAW3hEGu3afobLNk2QBotZbdWsi8JGcf589m67rr6NxAeJ/QUyvUypNK2Lt8eW0Z6 9zcdJsa8f+GvliPJxla/luMfr8YPyqLKJ+sNdCFyzxIZ5rvyv8fMPaJxEaFzkdjmNg0L ksgQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@ens.fr header.s=default header.b=UCgzfDYE; spf=pass (google.com: domain of rafael.bocquet@ens.fr designates 129.199.96.40 as permitted sender) smtp.mailfrom=rafael.bocquet@ens.fr Received: from nef.ens.fr (nef2.ens.fr. [129.199.96.40]) by gmr-mx.google.com with ESMTPS id 61si251037wrm.3.2020.05.16.01.34.44 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Sat, 16 May 2020 01:34:44 -0700 (PDT) Received-SPF: pass (google.com: domain of rafael.bocquet@ens.fr designates 129.199.96.40 as permitted sender) client-ip=129.199.96.40; X-ENS-nef-client: 129.199.1.22 Received: from clipper.ens.fr (clipper-gw.ens.fr [129.199.1.22]) by nef.ens.fr (8.14.4/1.01.28121999) with ESMTP id 04G8Yh1x016678 for ; Sat, 16 May 2020 10:34:44 +0200 Received: from localhost.localdomain using smtps by clipper.ens.fr (8.14.4/jb-1.1) id 04G8YhSW132512 for ; Sat, 16 May 2020 10:34:43 +0200 (authenticated user rbocquet) X-ENS-Received: (catv-89-133-37-198.catv.broadband.hu [89.133.37.198]) X-Envelope-To: Subject: =?UTF-8?Q?Re=3A_=5BHoTT=5D_What_is_known_and=2For_written_about_=E2=80=9CFro?= =?UTF-8?Q?benius_eliminators=E2=80=9D=3F?= To: HomotopyTypeTheory@googlegroups.com References: From: =?UTF-8?Q?Rafa=c3=abl_Bocquet?= Message-ID: <17a9e7e7-e03b-cf03-58de-5f1f77d74469@ens.fr> Date: Sat, 16 May 2020 10:34:39 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.7.0 MIME-Version: 1.0 In-Reply-To: Content-Type: multipart/alternative; boundary="------------9910BCDC5EF7AACF8883A20B" Content-Language: en-US X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-4.4.3 (nef.ens.fr [129.199.96.32]); Sat, 16 May 2020 10:34:44 +0200 (CEST) X-Original-Sender: rafael.bocquet@ens.fr X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@ens.fr header.s=default header.b=UCgzfDYE; spf=pass (google.com: domain of rafael.bocquet@ens.fr designates 129.199.96.40 as permitted sender) smtp.mailfrom=rafael.bocquet@ens.fr Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , This is a multi-part message in MIME format. --------------9910BCDC5EF7AACF8883A20B Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable Hi, Here's a simple countermodel that shows that the Martin-L=C3=B6f eliminator= =20 (two-sided eliminator) for identity types is not strong enough to derive=20 transport in the absence of Pi-types. Consider the initial model of a type theory with Id, refl, a closed type=20 A, a type family B over A, and closed terms x,y : A, b : B x and p :=20 Id_A x y. It can be shown that the only terms of that model are the variables, the=20 weakenings of the generators and their iterated refls. Because there is no closed term of type B y, transport does not hold in=20 this model. However, unless I missed some cases, it is still possible to define the=20 Martin-L=C3=B6f eliminator by case distinction on the elimination target. Best, Rafa=C3=ABl On 3/23/20 10:54 AM, Ambrus Kaposi wrote: > 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/Frob= eniusJDeriv.agda > This was observed by Rafael Bocquet and Andr=C3=A1s Kov=C3=A1cs in Octobe= r 2019,=20 > but 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=20 > don't have Pi, Sigma or (usual) universes:=20 > 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=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 they are derivable 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) qu= ite > surprising! > > > I was surprised too. The case of coproducts is especially unexpected. > > I mean a strong version of Id: > > > Side note: this is I think more widely known as the > Paulin-Mohring or one-sided eliminator for Id-types; the HoTT > book calls it based path-induction. > > The fact that the Frobenius version is strictly > stronger is known in folklore, but not written up > anywhere I know of. 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 take the model of given by its (TC,F) wfs; this > will model the simple version of Id-types but not the > Frobenius version. > > Are 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 above shows that the > Frobenius version is also definable. > > > Ah, yes =E2=80=94 there was a mistake in the argument I had in mi= nd.=C2=A0 > In that case, do we really know for sure that the Frobenius > versions are really strictly stronger? > > I don't know how to prove this, but it seems that we can't even > define transport without Frobenius J. Also, if we do have > transport and we know that types of the form \Sigma (x : A) > Id(a,x) are contractible, then the "one-sided J" is definable, so > if we want to prove that 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) Id(a,x) is not > contractible. > > =E2=80=93p. > > > > --=20 > You received this message because you are subscribed to the Google=20 > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send=20 > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com=20 > . > To view this discussion on the web visit=20 > https://groups.google.com/d/msgid/HomotopyTypeTheory/ade5cab1-5df2-41c9-b= 412-ac561fbe77bc%40googlegroups.com=20 > . --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/17a9e7e7-e03b-cf03-58de-5f1f77d74469%40ens.fr. --------------9910BCDC5EF7AACF8883A20B Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

Hi,

Here's a simple countermodel that shows that the Martin-L=C3=B6f eliminator (two-sided eliminator) for identity types is not strong enough to derive transport in the absence of Pi-types.

Consider the initial model of a type theory with Id, refl, a closed type A, a type family B over A, and closed terms x,y : A, b : B x and p : Id_A x y.

It can be shown that the only terms of that model are the variables, the weakenings of the generators and their iterated refls.

Because there is no closed term of type B y, transport does not hold in this model.

However, unless I missed some cases, it is still possible to define the Martin-L=C3=B6f eliminator by case distinction on the elimination target.

Best,
Rafa=C3=ABl

On 3/23/20 10:54 AM, Ambrus Kaposi wrote:
Hi,

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

Cheers,
Ambrus

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

2018-07-13 13:38 GMT+03:00 Peter LeFanu Lumsdaine <p.l.l...@gmail.com>:

I was surprised too. The case of coproducts is especially unexpected.
=C2=A0
=C2=A0
I mean a strong version of Id:
Side note: this is I think more widely known as the Paulin-Mohring or one-sided eliminator for Id-types; the HoTT book calls it based path-induction.

The fact that the Frobenius version is strictly 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 take the model of given by its (TC,F) wfs; this will model the simple version of Id-types but not the Frobenius version.

Are 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 above shows that the Frobenius version is also definable.
Ah, yes =E2=80=94 there was a mistake in the arg= ument I had in mind.=C2=A0 In that case, do we really kno= w for sure that the Frobenius versions are really strictly stronger?

I don't know how to prove this, but it seems that we can't even define transport without Frobenius J. Also, if we do have transport and we know that types of the form \Sigma (x : A) Id(a,x) are contractible, then the "one-sided J" is definable, so if we want to prove that 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) Id(a,x) is not contractible.
=C2=A0
=E2=80=93p.



--
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@googlegroup= s.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/Homotopy= TypeTheory/ade5cab1-5df2-41c9-b412-ac561fbe77bc%40googlegroups.com.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/17a9e7e7-e03b-cf03-58de-5f1f77d74469%40ens.fr.
--------------9910BCDC5EF7AACF8883A20B--