From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDV6Z5UK4EPBBTUVT3NAKGQECUKGFSA@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-pf0-x237.google.com (mail-pf0-x237.google.com [IPv6:2607:f8b0:400e:c00::237]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 05e85195 for ; Thu, 12 Jul 2018 17:07:28 +0000 (UTC) Received: by mail-pf0-x237.google.com with SMTP id b17-v6sf17419193pff.17 for ; Thu, 12 Jul 2018 10:07:28 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1531415247; cv=pass; d=google.com; s=arc-20160816; b=QPD9Qzl6PGO4kpPZRjqX/KsdQ92PmOqoHHTFZRN4GyxvbE5yMjrFSm1PWPQ7zQx9H2 s235KDdt9Dw8WyPZuhAAmlYgS7dCK22/03F96zNC8mWLCSFZAMsK2JB8l3Hb9+S9cZHH 4NiZhlepnjxiQNMJxwBR0WhkL3mY+fGguP07L335f8WQIrf0Nza/Xz23qoYQMjbRotWL RN7+fbp4srWjVeQLYLJYgASogabRhgAvSr8+KgOQcnAm5BYvf1T7xlCfAxScvGkjDHmn k3ptzmrf7+2uGq6+IVyGyQuNnY+SxPX2HuGw6XcCbBr7AbLx6huKubTHCVgvCbzQ5vJT LpHA== 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=GfrDd7OPxrUJ9mX3BdkAJQ5h8QrLhndjNgnr+QEUVNg=; b=0h1Sm8ma67yy5exqZpLxb6DukAHq1QDge9x5TC4wtWAfYGo1kmMf0V4J1+604YhDDs cfSoWBXwAccX3hQCxD4L7kdsej8lRqSntq68fn6L4Dl1NEQWTESaksqu453Nojxx14da fRcxZWIi28NYI3YwptGXyaqD3aFNICoO3kmIYGAO9S9o2kinGAeEyErs15cOaVpPmS+z GTw54TCKeiGfR4rZCbudDLsTx1Frcrvfn4rzgx+2NkqdDuWvqXCH4eO0oEkkVaT5bzBo NSgVJUojVaorbHf1pbj7UZw0vjvpApnxGioqahZX2DnATvoDPtFXiU/2+lajKXA7jjOA 0XBA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=Z4UbsJx1; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4001:c06::22c 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=GfrDd7OPxrUJ9mX3BdkAJQ5h8QrLhndjNgnr+QEUVNg=; b=X0hMmHFappglyYoygOW6Kc/G+0DG509pYwGWjtmeQIzBmw85mETjs0+P/bz7N4HvHT MuA17ihK1LlMZ6lh8p0aBo1Hhi/hFlBQMrb2gUdjByqfMYq4A0kBVF/vIv7yUORWR7GO rAs5TuGPfPCPHpBS1KPBB9+5dtsnhlP+5vTLgLev2xoMssaUBQUhTHSEf3sNJMIXScRo fiwEum+F8BHsGoBRwMYynbViqcduJamA6PDwpJGUpFi+LPmZrjjW/wjxbnkr8GnO4fp5 /G2UO2Il2m+JLN1sK/7woxiJ4z+c7TC5avktvDMcDh2380cgAtf9CR0233/C4Yyt7jBq 1YGQ== 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=GfrDd7OPxrUJ9mX3BdkAJQ5h8QrLhndjNgnr+QEUVNg=; b=agskDVWk/dtKCsUdgGGgwcWR4of7gHrx2d5fj/M5jKuzTHxk7LR5SlQoxmZda5SaVp Ne1ubivBJGabq7f2O2qV0vlXtELt7aQLvj2qDa5GLNexeEgAPodY9zY4yJRjZbWLaGNV X3/lKHsZpejtYV7ZuzIwUqAZ1NCIcy4IxZdw6m3Cn+3mKnDuFn5twq7bRF/83JCrxFKU FbkRNPSd8HriS2NuUMwRKN6uruZZXu7FKXZuslhRlxiHfbk4wOotMER31ShiFcBekmKv EGK2L9vUJY9knX6sO+IFz//3N1ND5H7wmcauJFKg/FXOvVYTXKnCYwqAlcko444mjUkS osgA== 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=GfrDd7OPxrUJ9mX3BdkAJQ5h8QrLhndjNgnr+QEUVNg=; b=r7S2wxt9CrWlVcwEHxonW54hxvYnPWLBSkhwBDAwsOH4Musi74sMma8NC/VPQxgWBe 6DNGA09rDvB4BMEK7k/I7jorw6FnXGXRTV0yrI3g1Oc0lMOaOscJY1v/tM3PB5/2Kq2d u6CXrRG+CUOSx5Wzh4OCh49u8xBbUjCJHFRm/rNpH22sdQW2rfe65NMa5PqM5agQUst1 XExKcKlRzuw6WP0ZkRhr1RyCmHBcn1oyIcSzLJCD3pRTVVv0E5YJYSMJ7R3PKI6Qjp9B 7SRKCu2mp0HX/4knaMTnlnfnXgCnfnMq7vmuB2x8we7UN5WMfd6fPoBI0xwZ+roJ6T4I k56g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlHhUtnvBsIb0TYUIHT6MEAXOC9o15uCGUL0F9FEAuII2AmcNzbD 98EGvC5fz23alkrda6ZZhy0= X-Google-Smtp-Source: AAOMgpdWlvxR7CJiVN7QSu2/T0r4XlEffipt7fhO5mLnQnEjzJfyitFJmtCs3VqEmVXbTZUKINiBtA== X-Received: by 2002:a65:65c3:: with SMTP id y3-v6mr12427pgv.3.1531415247017; Thu, 12 Jul 2018 10:07:27 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:bcc1:: with SMTP id o1-v6ls7114678pls.7.gmail; Thu, 12 Jul 2018 10:07:26 -0700 (PDT) X-Received: by 2002:a17:902:b190:: with SMTP id s16-v6mr702678plr.3.1531415246439; Thu, 12 Jul 2018 10:07:26 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1531415246; cv=none; d=google.com; s=arc-20160816; b=J/KZTETCm1ifF1uKeW5Y+89S5m6XEk7uVGYZhqXEb6phM0u849VDVQVCZUeYxnmjX6 8jvTMYRCGWUD1+7JWFwzkvXDKN7nX0E68ZMNmRyFRLXXIY+vAqo5loyCX9URUD1PwHFe hXBxfMyEzaF2ziwbpe3BsQnh0f+V7hriWQ7NnX4fKIqPl0g0sSSBo5RE9YBV9HI10MpO W2NW+zcRYkftEbycfYpMhNXBh2SQr0AJllqXH0Zh1W3Ep7O+kLDoWsb7qEQETiDeIa46 z2ptV8O6Clwpw0egSrsCk/pYUTc2yJp5bm7c8pYOunPTYvU7e+5Uxto85iIehiME8ZCC 0+KA== 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=ki2i8kNncYs7pOywcaxyrbs6tFFCTuUyAyEsD1Pe6F4=; b=MyMpXmPO8y3UToaArNYPFzDGJBsi/94O/dly0g2idmrUBBZaaA6MJ/AQa7nHc2WdCd TAV5ghKbX0w4CBw1szH16i+pKXTvh5x2w4zY9Ua0aBjbtcB+/ES/ZgYByd+d3DxxBBAA 9vxFhbgclAaL3dXhqpkzeT1FjlXejgD3Fkl/LKJCggYgTvqWAkedct3hXaVQcc5e8o6m hzm2QKeLF8IkSIupTLNcHvwo8NNGNrxBRhq7C9w0PNEkTiYZoP/WWzAcVNQ6Vwenurto ZNE4vur5CDsiFYl54WDx+yzM3edi7HYymG4cbrBj6+CyOaHgTpr7kzOTnJQ9BlYxQQn4 KkGg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=Z4UbsJx1; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4001:c06::22c as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-io0-x22c.google.com (mail-io0-x22c.google.com. [2607:f8b0:4001:c06::22c]) by gmr-mx.google.com with ESMTPS id a16-v6si612791pfi.1.2018.07.12.10.07.26 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 12 Jul 2018 10:07:26 -0700 (PDT) Received-SPF: pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4001:c06::22c as permitted sender) client-ip=2607:f8b0:4001:c06::22c; Received: by mail-io0-x22c.google.com with SMTP id z19-v6so28867133ioh.4 for ; Thu, 12 Jul 2018 10:07:26 -0700 (PDT) X-Received: by 2002:a5e:9209:: with SMTP id y9-v6mr16215810iop.92.1531415246069; Thu, 12 Jul 2018 10:07:26 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a6b:da18:0:0:0:0:0 with HTTP; Thu, 12 Jul 2018 10:06:45 -0700 (PDT) In-Reply-To: References: From: Valery Isaev Date: Thu, 12 Jul 2018 20:06:45 +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="000000000000bee74a0570d06587" 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=Z4UbsJx1; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4001:c06::22c 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: , --000000000000bee74a0570d06587 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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. I did not write down proofs in full detail, but I sketched them for identity types, sigma types, and coproducts and I think this also should be true for pushouts. Now, when I say that we have identity types I mean a strong version of Id: =CE=93 |=E2=80=93 a : A =CE=93, y:A, u:Id(a,y) |=E2=80=93 C(y,u) type =CE=93 |=E2=80=93 d : C(a,a,r(a)) type =CE=93 |=E2=80=94 b : A =CE=93 |=E2=80=94 p : Id(a,b) =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2= =80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 =CE=93 |=E2=80=94 J(a, (y,u)C, d, b, p) : C(b,p) We can prove all the usual constructions for identity types using this version of J including transport and extensionality for sigma types. To define the "Frobenius version" of this J, we construct a term t : (b,p) =3D (a,r(a)) using extensionality for sigma. Then we transport c along t from =CE=94(b,p) to =CE=94(a,r(a)), and substitute this in d. At this point= , we have a term d' of type C(a,r(a),t_*(c)). Then we use the fact that the type of triples \Sigma (q : \Sigma (b : A) Id(a,b)) Id((b,p),q) is contractible (this type is of the form \Sigma (x : A) Id(a,x) and we can prove that such types are contractible using the strong version of J). Thus, we have a path from ((a,r(a),t) to ((b,p),r((b,p))) and transporting d' along this path gives us a term of type C(b,p,c). Similar argument shows that the "Frobenius version" of sigma eliminator is definable. We just prove that p =3D (\pi_1(p),\pi_2(p)) and then transport terms back and forth along this path. The proof for coproducts is slightly more difficult, but the idea is similar. I constructed Frobenius versions of various eliminators in my recent preprint https://arxiv.org/abs/1806.08038 (I call Frobenius eliminators "local" and the usual ones "global"). I used there a non-standard version of HoTT, but as I mentioned before I believe that it should be possible to construct them in the ordinary HoTT (with sigma and Id types only). I also want to mention that Frobenius eliminators are definable only when our constructions are stable under substitution. If we do not assume that the type former, the constructors, and the non-Frobenius eliminator of some construction are stable under substitution, then we can interpret them in any category in which the corresponding categorical constructions are not necessarily stable under pullbacks, but this is not true for Frobenius eliminators. 2018-07-12 18:15 GMT+03:00 Peter LeFanu Lumsdaine = : > Briefly: I=E2=80=99m looking for background on the =E2=80=9CFrobenius ver= sion=E2=80=9D of > elimination rules for inductive types. I=E2=80=99m aware of a few pieces= of work > mentioning this for identity types, and nothing at all for other inductiv= e > types. I=E2=80=99d be grateful to hear if anyone else can point me to an= ything > I=E2=80=99ve missed in the literature =E2=80=94 even just to a reference = that lays out the > Frobenius versions of the rules for anything beyond Id-types. The > proximate motivation is just that I want to use these versions in a paper= , > and it=E2=80=99d be very nice to have a reference rather than cluttering = up the > paper by writing them all out in full=E2=80=A6 > > In more detail: Here are two versions of the eliminator for identity type= s: > > =CE=93, x,y:A, u:Id(x,y) |=E2=80=93 C(x,y,u) type > =CE=93, x:A |=E2=80=93 d(x) : C(x,x,r(x)) type > =CE=93 |=E2=80=94 a, b : A > =CE=93 |=E2=80=94 p : Id(a,b) > =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94= =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 > =CE=93 |=E2=80=94 J(A, (x,y,u)C, (x)d, a, b, p) : C(a,b,p) > > =CE=93, x,y:A, u:Id(x,y), w:=CE=94(x,y,u) |=E2=80=93 C(x,y,u,w) type > =CE=93, x:A, w:=CE=94(x,x,r(x)) |=E2=80=93 d(x,w) : C(x,x,r(x),w) type > =CE=93 |=E2=80=94 a, b : A > =CE=93 |=E2=80=94 p : Id(a,b) > =CE=93 |=E2=80=94 c : =CE=94(a,b,p) > =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94= =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 > =CE=93 |=E2=80=94 J(A, (x,y,u)=CE=94, (x,y,u,w)C, (x,w)d, a, b, p, c) : C= (a,b,p,c) > > (where =CE=94(x,y,u) represents a =E2=80=9Ccontext extension=E2=80=9D, i.= e. some finite > sequence of variables and types w_1 : B_1(x,y,u), w_2 : B_2(x,y,u,w_1), = =E2=80=A6) > > I=E2=80=99ll call these the =E2=80=9Csimple version=E2=80=9D and the =E2= =80=9CFrobenius version=E2=80=9D of the > Id-elim rule; I=E2=80=99ll call =CE=94 the =E2=80=9CFrobenius context=E2= =80=9D. The simple version is a > special case of the Frobenius one; conversely, in the presence of Pi-type= s, > the Frobenius version is derivable from the simple one. > > Most presentations just give the simple version. The first mention of th= e > Frobenius version I know of is in [Gambino, Garner 2008]; the connection > with categorical Frobenius conditions is made in [van den Berg, Garner > 2008], and some further helpful explanatory pointers are given in [Gambin= o, > Sattler 2015]. It=E2=80=99s based on this that I use =E2=80=9CFrobenius= =E2=80=9D to refer to these > versions; I=E2=80=99m open to suggestions of better terminology. (All re= ferences > are linked below.) > > 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. > Overall, I think the consensus among everyone who=E2=80=99s thought about= this > (starting from [Gambino, Garner 2008], as far as I know) is that if one= =E2=80=99s > studying Id-types in the absence of Pi-types, then one needs to use the > Frobenius version. > > One can also of course write Frobenius versions of the eliminators for > other inductive types =E2=80=94 eg Sigma-types, W-types, =E2=80=A6 Howev= er, I don=E2=80=99t know > anywhere that even mentions these versions! > > I remember believing at some point that at least for Sigma-types, the > Frobenius version is in fact derivable from the simple version (without > assuming Pi-types or any other type formers), which would explain why > no-one=E2=80=99s bothered considering it=E2=80=A6 but if that=E2=80=99s t= he case, it=E2=80=99s eluding me > now. On the other hand, I also can=E2=80=99t think of a countermodel sho= wing the > Frobenius version is strictly stronger =E2=80=94 wfs models won=E2=80=99t= do for this, > since they have strong Sigma-types given by composition of fibrations. > > So as far as I can see, if one=E2=80=99s studying Sigma-types in the abse= nce of > Pi-types, one again might want the Frobenius version; and it seems likely > that the situation for other inductive types would be similar. > > But I=E2=80=99m not sure, and I feel I may be overlooking or forgetting s= omething > obvious. What have others on the list thought about this? Does anyone > have a reference discussing the Frobenius versions of inductive types oth= er > than identity types, or at least giving the rules for them? > > Best, > =E2=80=93Peter. > > References: > > - Gambino, Garner, 2008, =E2=80=9CThe Identity Type Weak Factorisation Sy= stem=E2=80=9D, > https://arxiv.org/abs/0803.4349 > - van den Berg, Garner, 2008, =E2=80=9CTypes are weak =CF=89-groupoids= =E2=80=9D, > https://arxiv.org/pdf/0812.0298.pdf > - Gambino, Sattler, 2015, =E2=80=9CThe Frobenius condition, right propern= ess, and > uniform fibrations=E2=80=9D, https://arxiv.org/pdf/1510.00669.pdf > > -- > 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@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > --=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. --000000000000bee74a0570d06587 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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 identi= ty types and sigma types. I did not write down proofs in full detail, but I= sketched them for identity types, sigma types, and coproducts and I think = this also should be true for pushouts. Now, when I say that we have identit= y types I mean a strong version of Id:
=CE=93=C2=A0|=E2=80= =93 a : A
=CE=93, y:A, u:Id(a,y) =C2=A0|=E2=80=93 C(y,u) type=
=CE=93 |=E2=80=93 d : C(a,a,r(a)) type
=CE=93 |=E2=80= =94 b : A
=CE=93 |=E2=80=94 p : Id(a,b)
=E2=80=94=E2=80= =94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94= =E2=80=94=E2=80=94=E2=80=94=E2=80=94
=CE=93 |=E2=80=94 J(a, (y,u)= C, d, b, p) : C(b,p)

We can prove all the us= ual constructions for identity types using this version of J including tran= sport and extensionality for sigma types. To define the "Frobenius ver= sion" of this J, we construct a term t : (b,p) =3D (a,r(a)) using exte= nsionality for sigma. Then we transport c along t from=C2=A0=CE=94(b,p) to= =C2=A0=CE=94(a,r(a)), and substitute this in d. At this point, we have a te= rm d' of type C(a,r(a),t_*(c)). Then we use the fact that the type of t= riples \Sigma (q : \Sigma (b : A) Id(a,b)) Id((b,p),q) is contractible (thi= s type is of the form \Sigma (x : A) Id(a,x) and we can prove that such typ= es are contractible using the strong version of J). Thus, we have a path fr= om ((a,r(a),t) to ((b,p),r((b,p))) and transporting d' along this path = gives us a term of type C(b,p,c).

Similar argument= shows that the "Frobenius version" of sigma eliminator is defina= ble. We just prove that p =3D (\pi_1(p),\pi_2(p)) and then transport terms = back and forth along this path. The proof for coproducts is slightly more d= ifficult, but the idea is similar.

I constructed F= robenius versions of various eliminators in my recent preprint=C2=A0https://arxiv.org/a= bs/1806.08038=C2=A0(I call Frobenius eliminators "local"= and the usual ones "global"). I used there a non-standard versio= n of HoTT, but as I mentioned before I believe that it should be possible t= o construct them in the ordinary HoTT (with sigma and Id types only).
=

I also want to mention that Frobenius eliminators are d= efinable only when our constructions are stable under substitution. If we d= o not assume that the type former, the constructors, and the non-Frobenius = eliminator of some construction are stable under substitution, then we can = interpret them in any category in which the corresponding categorical const= ructions are not necessarily stable under pullbacks, but this is not true f= or Frobenius eliminators.

2018-07-12 18:15 GMT+03:00 Peter LeFanu Lumsdaine <p= .l.lumsdaine@gmail.com>:
Briefly: I=E2=80=99m looking for background on the =E2=80=9C= Frobenius version=E2=80=9D of elimination rules for inductive types.=C2=A0 = I=E2=80=99m aware of a few pieces of work mentioning this for identity type= s, and nothing at all for other inductive types.=C2=A0 I=E2=80=99d be grate= ful to hear if anyone else can point me to anything I=E2=80=99ve missed in = the literature =E2=80=94 even just to a reference that lays out the Frobeni= us versions of the rules for anything beyond Id-types.=C2=A0 The proximate = motivation is just that I want to use these versions in a paper, and it=E2= =80=99d be very nice to have a reference rather than cluttering up the pape= r by writing them all out in full=E2=80=A6

In more detail: Here are = two versions of the eliminator for identity types:

=CE=93, x,y:A, u:= Id(x,y) =C2=A0|=E2=80=93 C(x,y,u) type
=CE=93, x:A |=E2=80=93 d(x) : C(x= ,x,r(x)) type
=CE=93 |=E2=80=94 a, b : A
=CE=93 |=E2=80=94 p : Id(a,b= )
=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80= =94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94
=CE=93 |=E2=80= =94 J(A, (x,y,u)C, (x)d, a, b, p) : C(a,b,p)

=CE=93, x,y:A, u:Id(x,y= ), w:=CE=94(x,y,u) |=E2=80=93 C(x,y,u,w) type
=CE=93, x:A, w:=CE=94(x,x,= r(x)) |=E2=80=93 d(x,w) : C(x,x,r(x),w) type
=CE=93 |=E2=80=94 a, b : A<= br>=CE=93 |=E2=80=94 p : Id(a,b)
=CE=93 |=E2=80=94 c : =CE=94(a,b,p)
= =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2= =80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94
=CE=93 |=E2=80=94 J(= A, (x,y,u)=CE=94, (x,y,u,w)C, (x,w)d, a, b, p, c) : C(a,b,p,c)

(wher= e =CE=94(x,y,u) represents a =E2=80=9Ccontext extension=E2=80=9D, i.e. some= finite sequence of variables and types w_1 : B_1(x,y,u), w_2 : B_2(x,y,u,w= _1), =E2=80=A6)

I=E2=80=99ll call these the =E2=80=9Csimple version= =E2=80=9D and the =E2=80=9CFrobenius version=E2=80=9D of the Id-elim rule; = I=E2=80=99ll call =CE=94 the =E2=80=9CFrobenius context=E2=80=9D.=C2=A0 The= simple version is a special case of the Frobenius one; conversely, in the = presence of Pi-types, the Frobenius version is derivable from the simple on= e.

Most presentations just give the simple version.=C2=A0 The first = mention of the Frobenius version I know of is in [Gambino, Garner 2008]; th= e connection with categorical Frobenius conditions is made in [van den Berg= , Garner 2008], and some further helpful explanatory pointers are given in = [Gambino, Sattler 2015].=C2=A0 It=E2=80=99s based on this that I use =E2=80= =9CFrobenius=E2=80=9D to refer to these versions; I=E2=80=99m open to sugge= stions of better terminology. =C2=A0(All references are linked below.)
<= br>The fact that the Frobenius version is strictly stronger is known in fol= klore, 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 (T= C,F) wfs; this will model the simple version of Id-types but not the Froben= ius version.

Are you sure this is true? It s= eems 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.
=C2=A0
Overall, I think the consensus among everyone who=E2= =80=99s thought about this (starting from [Gambino, Garner 2008], as far as= I know) is that if one=E2=80=99s studying Id-types in the absence of Pi-ty= pes, then one needs to use the Frobenius version.

One can also of c= ourse write Frobenius versions of the eliminators for other inductive types= =E2=80=94 eg Sigma-types, W-types, =E2=80=A6 =C2=A0However, I don=E2=80=99= t know anywhere that even mentions these versions!

I remember believ= ing at some point that at least for Sigma-types, the Frobenius version is i= n fact derivable from the simple version (without assuming Pi-types or any = other type formers), which would explain why no-one=E2=80=99s bothered cons= idering it=E2=80=A6 but if that=E2=80=99s the case, it=E2=80=99s eluding me= now.=C2=A0 On the other hand, I also can=E2=80=99t think of a countermodel= showing the Frobenius version is strictly stronger =E2=80=94 wfs models wo= n=E2=80=99t do for this, since they have strong Sigma-types given by compos= ition of fibrations.

So as far as I can see, if one=E2=80=99s studyi= ng Sigma-types in the absence of Pi-types, one again might want the Frobeni= us version; and it seems likely that the situation for other inductive type= s would be similar.

But I=E2=80=99m not sure, and I feel= I may be overlooking or forgetting something obvious.=C2=A0 What have othe= rs on the list thought about this?=C2=A0 Does anyone have a reference discu= ssing the Frobenius versions of inductive types other than identity types, = or at least giving the rules for them?

Best,
=
=E2=80=93Peter.

References:

- Gambino, Garner, 20= 08, =E2=80=9CThe Identity Type Weak Factorisation System=E2=80=9D, https://arxiv.org/ab= s/0803.4349
- van den Berg, Garner, 2008, =E2=80=9CTypes are we= ak =C2=A0=CF=89-groupoids=E2=80=9D, https://arxiv.org/pdf/0812.0298.pdf
= - Gambino, Sattler, 2015, =E2=80=9CThe Frobenius condition, right propernes= s, and uniform fibrations=E2=80=9D, https://arxiv.org/pdf/1510.00669.pdf
=

--
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 https://groups.google.com/d/optout.

--
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.
--000000000000bee74a0570d06587--