From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDV6Z5UK4EPBBC4PULNAKGQETPJF4KQ@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.6 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-vk0-x240.google.com (mail-vk0-x240.google.com [IPv6:2607:f8b0:400c:c05::240]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id e500f88b for ; Fri, 13 Jul 2018 11:05:48 +0000 (UTC) Received: by mail-vk0-x240.google.com with SMTP id x125-v6sf10092141vke.2 for ; Fri, 13 Jul 2018 04:05:48 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1531479947; cv=pass; d=google.com; s=arc-20160816; b=xm3N+bzw2EBIRyBW5sTBywVOd12RXE1iLBKH4HYHClVmTV26stwvaqPDL3rrVX0wYh 6sic7J3o4b7XVHifSDBrDJfegt5m1yzY6m+bbWMMfKfDub34zJUR7ImxwE2sWRHJ/k8v aMNOdrZjXL1NXhvZj1qIFCAOMtyVMfCqjwddOmv7B1NUI0Q/ZNYKfLlxywCozlEjSbzw IGtmPbYBJq4iqoaJ45TBbGV0vZqi+00efriLpk2ROpajhx8kDUPx0DtPHekhYpjgPMKg OTC5NG6D75RzIUSSwAACd6nLXRYLxH3ewKOXEwEX8HXBQ/TgLF2uSSv/SzWpV4s3Q2c+ WOlw== 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:cc:to:subject:message-id:date:from :references:in-reply-to:mime-version:arc-authentication-results :arc-message-signature:sender:dkim-signature:dkim-signature :arc-authentication-results; bh=yQUSiHDM06Mph4pk6WmEzeGs4JEhr7Fb+972yH5Pbls=; b=aEgvunoTOnDT0N5wkRdf8xlGv5ONQPP0SOT6a53iwgT37az/e89E2jSBZ9ZDaR1PP0 DzvI36ZKjrwouKBXV/njMKALBoNng3vH69+mZ6is0Wykm4NaZ/rYqOEv+cmBh9rc/Yif PxelpKtn8UyrQ+gL8liO20eMVjMPFrD4FT54qLIDy28DHIsR+96MuClLQcey0Gi1TMuM UI51b8QjpEcFBR4rP8vn1MFSVs5p7stqFdFrZOhcl8S16nkvNTjsIa5S3lHdVBIrmQq+ PGGP2u4KB3R6nYGNJ6VAlyLZN3HmUZAlA65QOFHuDtRsduW3gRcesfUg4jdu2YncgXlm MNSg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=bLD4EVau; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4001:c0b::244 as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:in-reply-to:references:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=yQUSiHDM06Mph4pk6WmEzeGs4JEhr7Fb+972yH5Pbls=; b=n+ja2uJlT+DoLNJ9Vn8wxMJF312PxNlIMWYhcCmknxki6lvOYZLK0rBclGoZyx24sf yYltT5UC+fvWNWqMgsvSPWJaLlmCuhomB7Qqo9+13rvvOw3oucGZSACIdtZumYkDxQm9 JRgdTdxD4BeTbMRQZnP7h4oXDDDBvcBXRyNy8Gz7UdX3dELOVhvvSf+X5wSyRx2WMHH+ Gp7DZLGMeNVKPwkR6HkgGs8GJ2qZv5h8ML4Asywvpu7tvIWLCn+0mIBZ49Wf9z5aNd7/ UADJA8uIYEtV4oLBeOfgnt4QAkFN7rGWl8lvdfcG57kSKMm/5omL6g5YibXAbMD3u4cU D1eg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=yQUSiHDM06Mph4pk6WmEzeGs4JEhr7Fb+972yH5Pbls=; b=D7m+t3bWLv2T8DD3kBGxh6LdvZoNhZen/ctLKQoYjHTSv4mPsMgyZ0l2xiDI0kpZL2 n1ouCCMRvIHHPoYk/RWb0u7lBjUXlekyAm3feJvQDzo6CXtUkh0N50QwyGLiFEtsIYOU isddS5ySCckwFijZeChFY1otqXF/taANSGGO2Yo8dK1BVM0pGCVU2dle8OJ+g4sAqmUW DHAorWCwvUQ5Egr0K8xLERoIsDLsi12fdruU5otakD11qf+LgLAPv6k2IykzxzJyiAs4 5jYwa3a2P2VEntpM445E7N1CXm49EPuT+vyVmpGZExSHhXiSKgTVfldkWssGLY5EvqL/ 0UCA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:in-reply-to:references:from :date:message-id:subject:to:cc: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=yQUSiHDM06Mph4pk6WmEzeGs4JEhr7Fb+972yH5Pbls=; b=T0OCRkp3X/Ui1Aj0WN8yoTsD60MX+fI2xSC7huIiM1VWNJ1cu/4QWf6CNDKYF/Lkdu b6DrGYd/BLsdc0ddC6I3f9SIOv5MvWaWK31S68/O41o+4rB45nWf5nSgt+KMgJ7hMExR OIs4JDwZ0PQ3i1Fiq4wBrDCIZEGKObyPj0brLvdU909XGYXCIxJas7mDdtuSCNvYSOgs hXXaba4GyeKgzUdMLQyed4alxQSl8JAqR24xVhZ4Ip/RKJQeGcE5cqk8mPzz42V7Wj0Y pu4bORWyLt9tHJ8+4qKnZ3OCAwgwaKtAj9udmt4dOqpItaYjU3eYDcEq9BldJbL7PbJB C32w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlEK70dlnScKP/dcN70o112ddDlhUwGIhZdMR8kFBsDb/T/+EaZY cUXUt6Lfmfkx/0OtjCnHP18= X-Google-Smtp-Source: AAOMgpdWJBJLXnCI50qvrO5U7ZL1otQyQpS6nhvpCGp5/7wcBUnSEUEkofKDUrfQ87d513mRWaj+YQ== X-Received: by 2002:a1f:9746:: with SMTP id z67-v6mr33175vkd.2.1531479947310; Fri, 13 Jul 2018 04:05:47 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1f:c093:: with SMTP id q141-v6ls269669vkf.20.gmail; Fri, 13 Jul 2018 04:05:47 -0700 (PDT) X-Received: by 2002:a1f:820e:: with SMTP id e14-v6mr2854794vkd.42.1531479946975; Fri, 13 Jul 2018 04:05:46 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1531479946; cv=none; d=google.com; s=arc-20160816; b=ysHiEJiSPZAPuGMTWuU6/xxTc61Cf+KTg4e6xQNGrhYuKSaEhlDZmTkE9IzCo3l936 rAApnlTpzkkCB3KI7Btet2loDhQQor0VkN36lb0Wljff6GD1ZlT8WGZDXLNRUagwZrQM 9D0gODaHMpEWlanksMrn5G9aheXaGhiBFrxH0keCgsP2eoFS5luToZ8JDm39XVsvuEsF SmNurRA7C6urFANWFA1I7PBwVmzgcCsAAzoq+84NqrPWo7qH9FGq5AY1jH61DqshUTzB pvtMzmxBsEdy5lUQ7yoquTBfK9BbDWaZkprGUZVJa+Nr/O7vIR2bNFF9m3ceMF3dGHUi Pcfw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=mfHbRw39VrR/Q5nS4ZSzlslp8vZRtyAP2aegOunctfU=; b=Pa+pFJDB9hEXppGr70k70KMADvJ9e0H5aYUArsPmkgj5S1pZxwwVOE4++i6GfwtlTy Udp5cUIvLMEM0MqllzdxzXvPxTNWfqfK/B7STvI987OupFK1MazmP3rJRAO+UwrSIMqD vVsFOoKmHNLGRc9jFDINCO9Gfxq7/C30yIsur71qTAxqhR9ldoU1Aw6m2pSEE1MwcsUl QiavgICnyyITRkxnMomo6vOQHadiyo/IBvNJr2vKLL0FIF9y4FD1T5RiQB3omlPGDXAE LPUVfowDXZGxFgIvRDxJEvcHYUXDjeyIbIDkL5wqAQaHVQqRiOzPkMdsnG5/RuZYE/ZB ME6Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=bLD4EVau; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4001:c0b::244 as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-it0-x244.google.com (mail-it0-x244.google.com. [2607:f8b0:4001:c0b::244]) by gmr-mx.google.com with ESMTPS id w85-v6si1376456vkw.4.2018.07.13.04.05.46 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 13 Jul 2018 04:05:46 -0700 (PDT) Received-SPF: pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4001:c0b::244 as permitted sender) client-ip=2607:f8b0:4001:c0b::244; Received: by mail-it0-x244.google.com with SMTP id p17-v6so10973431itc.2 for ; Fri, 13 Jul 2018 04:05:46 -0700 (PDT) X-Received: by 2002:a02:5658:: with SMTP id o85-v6mr4893317jab.135.1531479946657; Fri, 13 Jul 2018 04:05:46 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a6b:da18:0:0:0:0:0 with HTTP; Fri, 13 Jul 2018 04:05:06 -0700 (PDT) In-Reply-To: References: From: Valery Isaev Date: Fri, 13 Jul 2018 14:05:06 +0300 Message-ID: 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: Peter LeFanu Lumsdaine Cc: "HomotopyTypeTheory@googlegroups.com" Content-Type: multipart/alternative; boundary="0000000000003384880570df76f4" X-Original-Sender: valery.isaev@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=bLD4EVau; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4001:c0b::244 as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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: , --0000000000003384880570df76f4 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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) quite surp= rising! > 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 f= or >>> quasi-categories on simplicial sets), and take the model of given by it= s >>> (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 argumen= t 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 mind. 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 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. For more options, visit https://groups.google.com/d/optout. --0000000000003384880570df76f4 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

= 2018-07-13 13:38 GMT+03:00 Peter LeFanu Lumsdaine <p.l.lumsdaine@gma= il.com>:
On Thu, Jul 12, 2018 at 7:07 PM Valery Isaev <valery.isaev@gmai= l.com> wrote:
Hi Peter,

<= /div>
I've been thinking about such eliminators lately too. It seem= s 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 obse= rvation, and (at least to me) quite surprising!

I was surprised too. The case of coproducts is espec= ially unexpected.
=C2=A0
=C2= =A0
I mean a strong version of Id:

Side note: this is I think more widely known as the Paulin-Moh= ring or one-sided eliminator for Id-types; the HoTT book calls it based pat= h-induction.

The fact that the Frobenius version is strictly stronger is known in folk= lore, 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 q= uasi-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 Frobeni= us version.

Are you sure this is true? It se= ems 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 v= ersion is also definable.

Ah, yes =E2=80=94 there was a mistake in the argument I had i= n mind.=C2=A0 In that case, do we really know for sure that the Frobenius v= ersions are really strictly stronger?

I don't know h= ow to prove this, but it seems that we can't even define transport with= out Frobenius J. Also, if we do have transport and we know that types of th= e form \Sigma (x : A) Id(a,x) are contractible, then the "one-sided J&= quot; 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 tr= ansport 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 &= 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.
For more options, visit http= s://groups.google.com/d/optout.
--0000000000003384880570df76f4--