From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDV6Z5UK4EPBBSNZT3NAKGQE2WE6LKA@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-yb0-x238.google.com (mail-yb0-x238.google.com [IPv6:2607:f8b0:4002:c09::238]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id f9ad2cf5 for ; Thu, 12 Jul 2018 18:24:10 +0000 (UTC) Received: by mail-yb0-x238.google.com with SMTP id g6-v6sf28498226ybc.5 for ; Thu, 12 Jul 2018 11:24:10 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1531419849; cv=pass; d=google.com; s=arc-20160816; b=H7RvrZ+5mqPe3/uf4veoM7O3Pj9bZkPvVwUIkgbzHEQTQ489Fhb/JXmrPtjsvbaJUa GV3YK2i+jsSps6ahhuxKq56yTWD9XrH4WUDQPzWeIyv6TZrAc1P+3s3dZ+ikMis/rje1 PZfHxPlFoQs9hGKJnkmdL1hq9MdUVTXs12E1hmneKozpLTnwYjGa4Om1yljTPzaFEV2y CquS30CCRQ/Px8bmG4tyOU/PCqSUqmoZWQhYxEah3B7hktxjjbvRgoRzL3ssI33jUgQs CYslJDjMoxV2OOPZ3/bXyMrnniIw8ZW0axmnivpP3kq4vyv3Ald4bUh5M+Zt09D4NWkN rjsQ== 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=54SnrSLf9gFwbApc5C0/jhJAJ2UUjJJIz3or90x4dcw=; b=Tec593iBrTd7hk1n5IcQSyxzjnEtpWpqf50p+ibboCEFXZ0MN1/ERhc9XYY9lnAAiE UG/OCG0hAPFzSNSLy+yMD2gafegpKOsl/HOIsbnLotOLK8eBkyw4OdAKCD+axIBLduUN nTgUweL0up9VGS6xTGCdO9jF6y5CmVKQasxXOK9znC4Y0J81uQ2NqQxMYpfSlHcaRh0K iAMemR0d9RVX6YexJprshZ3KiIGDYH3lPPYza7iQAj6zfRlY56A452HwkCGx+b+e/VN7 gtgiZjM1YLL9sBQSmMVwb3hSxsTIogtE9ZP4R+YAv7Pq5EfJjTO5hkkQrui2TZwUDW9n wmsA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=XyfYey0a; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4001:c06::236 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=54SnrSLf9gFwbApc5C0/jhJAJ2UUjJJIz3or90x4dcw=; b=CxjpAigl3LaYAjaJIMFoG9TH6AoJzXhNpUqYwCdgNXA/42CJgABQxfqhuqOPC62Fbu nI7EAhUWBc8ILUuPRLhw8ETawHW88K1bz6/hcN5woxFD15jsbL6WWKqLL9PmKuHMtzf5 ZsmKXzA6zV9xE4IHvRsnSf3h0uAm4A6C6KTc3aFHrpJUd5UQvmVwmBkoiu5DftZXXBmH 5P8ppschftDCP1ID9Hp7UJ0fwmCi2g3gYk1V2/LhlIPE2Xn9BiIJ+DuvM40kRlkxKwt3 96CwT2Plep73Zmx1SeE/BP/HtEUosN8JDNWgnGG67s/hhXJ7cu7Eypvm9tEM4DLWb3JG GvkA== 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=54SnrSLf9gFwbApc5C0/jhJAJ2UUjJJIz3or90x4dcw=; b=YVvoP2VO+fPS5KT/KyuBH7gW1LMib13htEcCqwElVRH5+FRIq1hwK2SudX2NPkMUeb g02vGc2BQw5yWWs6E0X9G2xnTtWLebBc8weizcFFz1bHPaa8tT4po4PiDAVriY+iVpt9 2byzhbT/rGKsDep+BaNHi/09OCygtmz53PkBjn86LIKWn6J8gK8wGdjWgrWwTOAEX54Z 1H5GkZjwOjdQfdA458GbcGYSDYCMm19x/ZfR8JaRQbsyd2z4z2zLcWJYT2f94eUsRqfy p+ur0m8/aZ5h//PicYeQwWLbME3bNeFSelu6xD6XoAZUqOCdisAQtodL1+PK+l6s7hjP 9WLw== 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=54SnrSLf9gFwbApc5C0/jhJAJ2UUjJJIz3or90x4dcw=; b=uZivQBwclljtYsClxIPvYbkypYEeQ7eF4VWyCTpnSkJqr49Ofx3BwY+0fPtQgZVQHv a48eKnXoWOygdPq+4muJBCL4ATEOKcvixkakvcR1eE37mkpJcVQsItrbiI0TWLhecdUr k6p4MNeJj9Yq1DMgqHku5g2qGHDKfDXrud4DU2zYE20+5Y1Bg/cIUubXP5DlNESf0E49 dd480eRLU/eDnK7/VOoyx0vlVLzIjOhmgxih22kUtTQZTMa/EoN4E+PEoTIWzUhkq5Cv +6HXNR0eKZRkfojoAzFUckeBuK5wmefXSQIcM3hhiCvLZEHO+55YNAACXKXFfQ/vo9rA IuYQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlHRPp6oA9bJb34DNO3oe/NQnGSUFCYgRj6tUp1/fQ8rxzcqg2qZ t7LAitCxc1LS+5Wt35f00sU= X-Google-Smtp-Source: AAOMgpfRACy1O0+FYUoCqOzafzN6dK9H3ozoGMOKEwjQ5PDvXNYONtdWLyjuPZcFEwZTp15t2cV26w== X-Received: by 2002:a81:330a:: with SMTP id z10-v6mr326774ywz.5.1531419849616; Thu, 12 Jul 2018 11:24:09 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:10d5:: with SMTP id 204-v6ls3395597ywq.37.gmail; Thu, 12 Jul 2018 11:24:09 -0700 (PDT) X-Received: by 2002:a0d:f483:: with SMTP id d125-v6mr970669ywf.159.1531419849307; Thu, 12 Jul 2018 11:24:09 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1531419849; cv=none; d=google.com; s=arc-20160816; b=NAyYxMxf2EumPn1QxoCB4eOuXKVfPPnZQkETR0cp5smGAgWuQa3Z+8GQCNUqvg74Tt 4PHEvBZ6rqR400Adic0Z7mpUjSCJGbLpf64QlPVehyCB0rro1+LzwF/yvg+gHbc+Zz6m XK2qXNksgwmmPXrxlNjwE+uePbpf1S7/zvW4z3bDBIbUgHXScq3mYH7M5xvqPboENKHR o4VjLZl2faVUTALpqCjVwzSf6Jg+5A86ggoaXzE+Hc9WieenUNz2ViV3ZiLqwgh1MLFC T0wPP5pHipGsbM8993wYos+SeI9nGKP5Eey5j8xfItFtzVRRUQzutdk/gHFJ7F2Z7kkk OnfA== 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=KTKkG2UQ6UUwRbea2YiSsIJmJ0+5fByxoM2XbUd4jxs=; b=p1sKvVhiILKfZpMQFcCQC0VLMdd7fZREkaRk6s5wRAMQIPnLWJW6pdnD6/m52E2pBb Za6I70AEQDpta4bIfBBZjIdWAc9p3wAM4BK/cKIeYE5mOjaPDX6uVfmZf0BBX43t6kX4 3B0JJXF71uKUomeGi2HOhuc9rYMSzwySq+iSMJQ29U+qO3DhPn7ird5RRzuIoTMJh/W7 7sfYkDTpo4MBqAs3LVyORohHptUiCnBnV6he2eVDVjCT9zmycsROIA+LGGC40oMpqYDz zYBEdYkVydnXWSR4nepPv30ZWltzfDBioOjJQZptTjKshhVDsOE0iPxgYaAki+j/4BnJ wf/g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=XyfYey0a; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4001:c06::236 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-x236.google.com (mail-io0-x236.google.com. [2607:f8b0:4001:c06::236]) by gmr-mx.google.com with ESMTPS id v79-v6si1456922ywc.2.2018.07.12.11.24.09 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 12 Jul 2018 11:24:09 -0700 (PDT) Received-SPF: pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4001:c06::236 as permitted sender) client-ip=2607:f8b0:4001:c06::236; Received: by mail-io0-x236.google.com with SMTP id v26-v6so29066856iog.5 for ; Thu, 12 Jul 2018 11:24:09 -0700 (PDT) X-Received: by 2002:a6b:b342:: with SMTP id c63-v6mr27837963iof.204.1531419848911; Thu, 12 Jul 2018 11:24:08 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a6b:da18:0:0:0:0:0 with HTTP; Thu, 12 Jul 2018 11:23:28 -0700 (PDT) In-Reply-To: References: From: Valery Isaev Date: Thu, 12 Jul 2018 21:23:28 +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: Thorsten Altenkirch Cc: "homotopytypetheory@googlegroups.com" Content-Type: multipart/alternative; boundary="00000000000018b4450570d178dc" 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=XyfYey0a; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4001:c06::236 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: , --00000000000018b4450570d178dc Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Such version corresponds simply to the fact that the eliminator is defined in every context (=CE=93 in Peter's original post). Without this context eliminators are undeniably too weak. The point of Frobenius eliminators is that Y in your notation can depend on the eliminated parameter. I don't think that it is possible to define Frobenius for recursive datatypes. Regards, Valery Isaev 2018-07-12 21:06 GMT+03:00 Thorsten Altenkirch < Thorsten.Altenkirch@nottingham.ac.uk>: > Isn't this what is usually called recursion with parameters. E.g. in the > simple typed case for natural numbers: the usual recursor can be written > using only 1st order functions: > > z : X > s : Nat -> X -> X > ----------------------- > R_X(z,s) : N -> X > > R(z,s) 0 =3D=3D z > R(z,s) (suc m) =3D=3D s m (R(z,s) m) > > while recursion with a parameter is: > > z : Y -> X > s : Nat -> Y -> X -> X > ---------------------------- > R'_X,Y(z,s) : Nat -> Y -> X > > R'(z,s) 0 y =3D=3D z y > R'(z,s) (suc m) y =3D=3D s m y (R'(z,s) m y) > > Using functions we can reduce R' to R > > R'_X,Y(z,s) =3D R_(Y -> X)(z,\n f y.s n y (f y)) > > but without functions R' is stronger and it is what you need to have > recursion in every slice. A simple example is addition over the 1st > argument, which with functions we can write as > > R_Nat->Nat (\n . n) (\ n fn m . suc (fn m)) > > but you can use R' without function types > > R'_Nat,Nat (\ n . n) (\ n m x . suc m) > > Hence in the absence of Pi-types you need to use the "localized" version > of the recursor. I think in the special case of + this gives you > distributivity over x even without cartesian closure. > If we don't assume products we need to replace Y by a context. > > I think I have seen the case for Id in Thomas Streicher's habilitation bu= t > I am not sure. > > Thorsten > > > From: on behalf of Peter LeFanu > Lumsdaine > Date: Thursday, 12 July 2018 at 16:15 > To: "homotopytypetheory@googlegroups.com" googlegroups.com> > Subject: [HoTT] What is known and/or written about =E2=80=9CFrobenius > eliminators=E2=80=9D? > > 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. > > 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. > > > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > attachment. > > Any views or opinions expressed by the author of this email do not > necessarily reflect the views of the University of Nottingham. Email > communications with the University of Nottingham may be monitored > where permitted by law. > > > > > -- > 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. --00000000000018b4450570d178dc Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Such version corresponds simply to the fact that the elimi= nator is defined in every context (=CE=93 in Peter's original post). Wi= thout this context eliminators are undeniably too weak. The point of Froben= ius eliminators is that Y in your notation can depend on the eliminated par= ameter. I don't think that it is possible to define Frobenius for recur= sive datatypes.

Regards,
Valery Isaev

2018-07-12 21:06 GMT+03:00 Thorsten Altenkir= ch <Thorsten.Altenkirch@nottingham.ac.uk>= :
Isn't this what is usually called recursion with parameters. E.g. = in the simple typed case for natural numbers: the usual recursor can be wri= tten using only 1st order functions:

z : X=C2=A0
s : Nat -> X -> X
-----------------------
R_X(z,s) : N -> X

R(z,s) 0 =3D=3D z
R(z,s) (suc m) =3D=3D s m (R(z,s) m)

while recursion with a parameter is:

z : Y -> X
s : Nat -> Y -> X -> X
----------------------------
R'_X,Y(z,s) : Nat -> Y -> X

R'(z,s) 0 y =3D=3D z y
R'(z,s) (suc m) y =3D=3D s m y (R'(z,s) m y)

Using functions we can reduce R' to R

R'_X,Y(z,s) =3D R_(Y -> X)(z,\n f y.s n y (f y))

but without functions R' is stronger and it is what you need to ha= ve recursion in every slice.=C2=A0 A simple example is addition over the 1s= t argument, which with functions we can write as

R_Nat->Nat (\n . n) (\ n fn m . suc (fn m))

but you can use R' without function types

R'_Nat,Nat (\ n . n) (\ n m x . suc m)=C2=A0

Hence in the absence of Pi-types you need to use the "localized&q= uot; version of the recursor. I think in the special case of + this gives y= ou distributivity over x even without cartesian closure.
If we don't assume products we need to replace Y by a context.=C2= =A0

I think I have seen the case for Id in Thomas Streicher's habilita= tion but I am not sure.

Thorsten


From: <homotopytypetheory@goo= glegroups.com> on behalf of Peter LeFanu Lumsdaine <p.l.lumsdaine@gmail.com= >
Date: Thursday, 12 July 2018 at 16:= 15
To: "homotopytypetheory@goo= glegroups.com" <homotopytypetheory@googlegroups.com><= br> Subject: [HoTT] What is known and/o= r written about =E2=80=9CFrobenius eliminators=E2=80=9D?

Briefly: 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 g= rateful to hear if anyone else can point me to anything I=E2=80=99ve missed in the li= terature =E2=80=94 even just to a reference that lays out the Frobenius ver= sions of the rules for anything beyond Id-types.=C2=A0 The proximate motiva= tion 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 u= p the paper 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
=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.=C2=A0 The simple version is a spe= cial case of the Frobenius one; conversely, in the presence of Pi-types, th= e Frobenius version is derivable from the simple one.

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 connecti= on with categorical Frobenius conditions is made in [van den Berg, Garner 2= 008], 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 suggestions of better terminology. =C2=A0(All references= are linked below.)

The fact that the Frobenius version is strictly stronger is known in folklo= re, 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 qua= si-categories on simplicial sets), and take the model of given by its (TC,F) wfs; this will model the simple vers= ion of Id-types but not the Frobenius version.

Overall, I think the consensus among everyone who=E2=80=99s thought about t= his (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 othe= r inductive types =E2=80=94 eg Sigma-types, W-types, =E2=80=A6 =C2=A0Howeve= r, 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 Frobe= nius 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 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 strictl= y 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 absenc= e of Pi-types, one again might want the Frobenius version; and it seems lik= ely 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 forgettin= g something obvious.=C2=A0 What have others on the list thought about this?= =C2=A0 Does anyone have a reference discussing the Frobenius versions of in= ductive types other 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 Syst= em=E2=80=9D, https://arxiv.org/abs/0803.4349
- van den Berg, Garner, 2008, =E2=80=9CTypes are weak =C2=A0=CF=89-groupoid= s=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.
 
This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.=20

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored=20
where permitted by law.

--
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.
--00000000000018b4450570d178dc--