From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBC7KF3MJXIPBBE5GT3NAKGQE4V7AXOI@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-oi0-x23e.google.com (mail-oi0-x23e.google.com [IPv6:2607:f8b0:4003:c06::23e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b60e4dc9 for ; Thu, 12 Jul 2018 17:42:45 +0000 (UTC) Received: by mail-oi0-x23e.google.com with SMTP id 13-v6sf40844133oiq.1 for ; Thu, 12 Jul 2018 10:42:44 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=9y3bHeCIt41xcKFhX9/sVrfn0+sT3y4Gx9rPgRw8dZk=; b=bXRhtR8EDgNRsr4I67kCeJsfwA2Eq2LTkpTUoObpYWydwH/HZT6bSx044+LTxMftde aQ1+4htMl1rpmEl4vuby223Wj8NYesLfmVcuMRBZF6WGi3AUUbm/2B+669auwQWCp2Uu dTcrxl2BaLEcfU4pohoZF55xPXlv7m22sEu8ogHWHc8K1k9RQOy9Hn+eJSP35wKGNLBB hMQk/HlNTEqaBP651ClClH+LO3j/5erk8Wsj2/2mm4JfhcNzlEI6HS5UEHcTdJ1LAVt7 m8bVkalBosNFgeGwdFpGl7rDv8AwfsRRlr3RDB+tYUOA8i3a7ngF4qwNAKC5DsVnrgYc M5iQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=9y3bHeCIt41xcKFhX9/sVrfn0+sT3y4Gx9rPgRw8dZk=; b=nGltxyexVKi9IEoo7bOD2fcFI+TUOEgNBQKPAQQRjDoKF6H4H2OH7w4oVQ3XYdXB7g cwRNZNulp2nIa9clqHw7MWIas10UNejAhV05XV6WBGwPG+qxTzNzYTNpSCFyVr+IjwZ6 JY7yg8HFsXbelgkOVTlNsR0/+D09odUwvKEL7pB+m3oCfMP62gSTqnJynL+rvouJ9BwZ i7d80agNmU1RTrT7iG2suNM69QqiwSOPHStoA6GQYS8n+pwjZFneWWeBi5PdK1/1TGr7 2Fu8JHqvuNVaMuneiXY5nr/EFM25gwYIDUYcAIfVcn91dr6kAN8IVdQyGeVA2hBN6Qof gHdQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=9y3bHeCIt41xcKFhX9/sVrfn0+sT3y4Gx9rPgRw8dZk=; b=HPLs/atLAjPqseL3fGNbHkhFLy5z07NmRe8TOrbpOemt8tnmevMsoFnrrHYf7hYPas ED2wymJ3F87HmoBzPDLPabJTKFqMy4XZJOqql3OWMqjHvra0eaRSPtv7rb1toBGDq2DV Fg/CgouqDzBl6FzxIb8R8ug+A31/XLLxkCw6YY+4V+Ew4Oit++FKNinySOrNKY4VPn0C o/laWS931ujZa+i2RaH0w+bI0rjauhIipH9SYY3/m1JYdvHt26icxFp75FeU6gXN4QjJ TH7EjbmaCKYEQMUJAwIwdeVX/G8ie2XRP6CeiouDqOKX50thVfbw0KmZWwUrUG5vD3iy 7G+w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlEyCFTEYHQik+1EQ5jYEMgAVk1/l/zdP96GRVS/S4GOKUAQipG6 JdDQDxYeZGSdilXbzv1z3io= X-Google-Smtp-Source: AAOMgpfFor0KXk+sJjkpWDuUT893C9gWVyAwcXhnHPxKfvzLSdfIlFmzzS9dkWlZ9yRzNjk8jm0FVw== X-Received: by 2002:aca:c6ca:: with SMTP id w193-v6mr677592oif.1.1531417364083; Thu, 12 Jul 2018 10:42:44 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:e610:: with SMTP id d16-v6ls15059524oih.2.gmail; Thu, 12 Jul 2018 10:42:43 -0700 (PDT) X-Received: by 2002:aca:f495:: with SMTP id s143-v6mr669345oih.7.1531417363535; Thu, 12 Jul 2018 10:42:43 -0700 (PDT) Date: Thu, 12 Jul 2018 10:42:42 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <7a64bd9e-42ae-4d7b-a08e-df1c60437dc0@googlegroups.com> In-Reply-To: References: Subject: =?UTF-8?Q?=5BHoTT=5D_Re=3A_What_is_known_and=2For_written_about_=E2=80=9CFro?= =?UTF-8?Q?benius_eliminators=E2=80=9D=3F?= MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_46552_43979954.1531417362957" X-Original-Sender: atmacen@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: , ------=_Part_46552_43979954.1531417362957 Content-Type: multipart/alternative; boundary="----=_Part_46553_1969475314.1531417362957" ------=_Part_46553_1969475314.1531417362957 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable This looks similar to the "left rule" version of inductive elimination,=20 where you eliminate a variable (not an arbitrary term), and the context=20 extension depending on it gets updated. Except the "Frobenious version"=20 allows an arbitrary term, so you say in what way part of the context=20 depends on it. (Your "c : =CE=94(a,b,p)".) Coq's "destruct" tactic sort of= =20 implements this; it picks =CE=94 and c for you by searching subexpressions = in=20 the context. In general, "dependent pattern matching" seems to use the left= =20 rules, and variants, rather than the "simple versions", where the context= =20 never changes. Have you tried looking at the literature on dependent=20 pattern matching? I know this isn't a real answer. I don't know any papers= =20 that I know have Frobenious versions. Also, it looks like your =CE=94 is no= t=20 literally a context extension, but the corresponding dependent record type. On Thursday, July 12, 2018 at 11:15:38 AM UTC-4, Peter LeFanu Lumsdaine=20 wrote: > > Briefly: I=E2=80=99m looking for background on the =E2=80=9CFrobenius ver= sion=E2=80=9D of=20 > elimination rules for inductive types. I=E2=80=99m aware of a few pieces= of work=20 > mentioning this for identity types, and nothing at all for other inductiv= e=20 > types. I=E2=80=99d be grateful to hear if anyone else can point me to an= ything=20 > I=E2=80=99ve missed in the literature =E2=80=94 even just to a reference = that lays out the=20 > Frobenius versions of the rules for anything beyond Id-types. The=20 > proximate motivation is just that I want to use these versions in a paper= ,=20 > and it=E2=80=99d be very nice to have a reference rather than cluttering = up the=20 > 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=20 > 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=20 > Id-elim rule; I=E2=80=99ll call =CE=94 the =E2=80=9CFrobenius context=E2= =80=9D. The simple version is a=20 > special case of the Frobenius one; conversely, in the presence of Pi-type= s,=20 > the Frobenius version is derivable from the simple one. > > Most presentations just give the simple version. The first mention of th= e=20 > Frobenius version I know of is in [Gambino, Garner 2008]; the connection= =20 > with categorical Frobenius conditions is made in [van den Berg, Garner=20 > 2008], and some further helpful explanatory pointers are given in [Gambin= o,=20 > Sattler 2015]. It=E2=80=99s based on this that I use =E2=80=9CFrobenius= =E2=80=9D to refer to these=20 > versions; I=E2=80=99m open to suggestions of better terminology. (All re= ferences=20 > are linked below.) > > 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 its= =20 > (TC,F) wfs; this will model the simple version of Id-types but not the=20 > Frobenius version. > > Overall, I think the consensus among everyone who=E2=80=99s thought about= this=20 > (starting from [Gambino, Garner 2008], as far as I know) is that if one= =E2=80=99s=20 > studying Id-types in the absence of Pi-types, then one needs to use the= =20 > Frobenius version.=20 > > One can also of course write Frobenius versions of the eliminators for=20 > other inductive types =E2=80=94 eg Sigma-types, W-types, =E2=80=A6 Howev= er, I don=E2=80=99t know=20 > anywhere that even mentions these versions! > > I remember believing at some point that at least for Sigma-types, the=20 > Frobenius version is in fact derivable from the simple version (without= =20 > assuming Pi-types or any other type formers), which would explain why=20 > 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=20 > now. On the other hand, I also can=E2=80=99t think of a countermodel sho= wing the=20 > Frobenius version is strictly stronger =E2=80=94 wfs models won=E2=80=99t= do for this,=20 > 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=20 > Pi-types, one again might want the Frobenius version; and it seems likely= =20 > 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=20 > obvious. What have others on the list thought about this? Does anyone= =20 > have a reference discussing the Frobenius versions of inductive types oth= er=20 > 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,=20 > https://arxiv.org/abs/0803.4349 > - van den Berg, Garner, 2008, =E2=80=9CTypes are weak =CF=89-groupoids= =E2=80=9D,=20 > https://arxiv.org/pdf/0812.0298.pdf > - Gambino, Sattler, 2015, =E2=80=9CThe Frobenius condition, right propern= ess, and=20 > uniform fibrations=E2=80=9D, https://arxiv.org/pdf/1510.00669.pdf > --=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. ------=_Part_46553_1969475314.1531417362957 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
This looks similar to the "left rule" version of= inductive elimination, where you eliminate a variable (not an arbitrary te= rm), and the context extension depending on it gets updated. Except the &qu= ot;Frobenious version" allows an arbitrary term, so you say in what wa= y part of the context depends on it. (Your "c : =CE=94(a,b,p)".) = Coq's "destruct" tactic sort of implements this; it picks =CE= =94 and c for you by searching subexpressions in the context. In general, &= quot;dependent pattern matching" seems to use the left rules, and vari= ants, rather than the "simple versions", where the context never = changes. Have you tried looking at the literature on dependent pattern matc= hing? I know this isn't a real answer. I don't know any papers that= I know have Frobenious versions. Also, it looks like your =CE=94 is not li= terally a context extension, but the corresponding dependent record type.
On Thursday, July 12, 2018 at 11:15:38 AM UTC-4, Peter LeFanu Lumsdai= ne wrote:
Brie= fly: I=E2=80=99m looking for background on the =E2=80=9CFrobenius 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 types, and nothing at= all for other inductive types.=C2=A0 I=E2=80=99d be grateful to hear if an= yone 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 Frobenius versions of = the rules for anything beyond Id-types.=C2=A0 The proximate motivation is j= ust 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 the= m 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
=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 s= equence 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 presenc= e of Pi-types, the Frobenius version is derivable from the simple one.
<= br>Most presentations just give the simple version.=C2=A0 The first mention= of the Frobenius version I know of is in [Gambino, Garner 2008]; the conne= ction with categorical Frobenius conditions is made in [van den Berg, Garne= r 2008], and some further helpful explanatory pointers are given in [Gambin= o, Sattler 2015].=C2=A0 It=E2=80=99s based on this that I use =E2=80=9CFrob= enius=E2=80=9D to refer to these versions; I=E2=80=99m open to suggestions = of better terminology. =C2=A0(All references are linked below.)

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 tak= e any non right proper model category (e.g. the model structure for quasi-c= ategories on simplicial sets), and take the model of given by its (TC,F) wf= s; this will model the simple version of Id-types but not the Frobenius ver= sion.

Overall, I think the consensus among everyone who=E2=80=99s th= ought about this (starting from [Gambino, Garner 2008], as far as I know) i= s 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 writ= e 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=99t know any= where that even mentions these versions!

I remember believing at som= e point that at least for Sigma-types, the Frobenius version is in fact der= ivable 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 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 won=E2=80= =99t do for this, since they have strong Sigma-types given by composition o= f fibrations.

So as far as I can see, if one=E2=80=99s studying Sigm= a-types in the absence of Pi-types, one again might want the Frobenius vers= ion; 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 something obvious.=C2=A0 What have others on t= he list thought about this?=C2=A0 Does anyone have a reference discussing t= he Frobenius versions of inductive types other than identity types, or at l= east giving the rules for them?

Best,
= =E2=80=93Peter.

References:

- Gambino, Garner, 2008, = =E2=80=9CThe Identity Type Weak Factorisation System=E2=80=9D, https://arxiv.org/abs/0803.4349
- van den Berg, Garner, 2008, = =E2=80=9CTypes are weak =C2=A0=CF=89-groupoids=E2=80=9D, https://arxiv.org/pdf/0812.0298.pdf
- Gambino, Sattler, = 2015, =E2=80=9CThe Frobenius condition, right properness, and uniform fibra= tions=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 http= s://groups.google.com/d/optout.
------=_Part_46553_1969475314.1531417362957-- ------=_Part_46552_43979954.1531417362957--