From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCIPFMNR2IEBBPFRT3NAKGQEYILOPBA@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.8 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_DKIMWL_WL_MED autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-ed1-x539.google.com (mail-ed1-x539.google.com [IPv6:2a00:1450:4864:20::539]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 44e08b26 for ; Thu, 12 Jul 2018 18:06:53 +0000 (UTC) Received: by mail-ed1-x539.google.com with SMTP id c2-v6sf11615070edi.20 for ; Thu, 12 Jul 2018 11:06:53 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1531418812; cv=pass; d=google.com; s=arc-20160816; b=cAdJelhEc9op3t6SCXkGjisnFx87cHR8l4vdL1x0mh1VUjtNHc8pktLbfdBd4RoBV2 vY8r6cTvtv/WFpRyIQ4IqiLDGiFMJ9P6iZwu3kfZ2CNWSVD/3QeTcuAQTOj5u4bDZ+V0 /zV+3LHliuZ+1roNrhKb+P5Rd+4GGXaPV2SE7/HNN12PqGlmqE7XD38Vr9N3YxxoOtCj R4NFXYfmPXsqNAE08UiijjE6q/O3QIHpv09rhw8VbMIUZfRHv/3tdYWCryktQ/lVCYSp VIgphmHNmP+QsxnqcnKPm8ifHpA0whWgu8xPX3EQ8gmU45Adymv2ZzIhrHb6XWyT3M5M joCQ== 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:mime-version:spamdiagnosticmetadata :spamdiagnosticoutput:user-agent:content-language:accept-language :in-reply-to:references:message-id:date:thread-index:thread-topic :subject:to:from:arc-authentication-results:arc-message-signature :sender:dkim-signature:arc-authentication-results; bh=Dsp/vEL3N09b5PhtqMTzXcMlCaqKe8Qn/fMbxDuViIY=; b=SMKeCyj9ehcGl7A/Ru6mSKmOeCsMvQ0p+kqlEmhogxlgt77Xc7R/zMtEBPaisYeVF3 pSNvQUboFD5vyUCUcqOm2WepkYhSu2jlN0M9sHCWnx08lr+IUJbRolJQxhI2CFjLSpPV usMHNDM6ejSVPZKjNecyAZo70tPykx7X/TZNNWJmh5lJ9XAckqxgmiOSx16z3ip7L5g1 /sjtH2mDjhMpdx8oVjbLfIN0P4kXzcMfnyd5ZaaYT0WOMKgXPlpXPa6XoG6FxiJvC6as CvbZ0bF0RgMfwb/80MSq7/Qvvpu3RtEq0ioZEgTU6UVo9kPhiYpXde0wn6rhylF/EEll wO9Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.125 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language:user-agent :spamdiagnosticoutput:spamdiagnosticmetadata:mime-version :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=Dsp/vEL3N09b5PhtqMTzXcMlCaqKe8Qn/fMbxDuViIY=; b=Rw3HPCME4bWYZPcnwrVDJ23FQSVnSV0kqd5qdsClbwQc8aAbCc8vxWBfiAJR+sflF5 u3lrWZPCSEmsDidDAe/PXeTmq/DayanHSYpw+exds3VGDY6aYW1WR+8Vu80ZeGJOxuAw /ev9KLha9ux+Wpd07hITIuAXaY175sxthhMINxwZ8MYX9/wsfW8HjDtTtsYG4eK+nuyX hiz7S9Lv0m5G+IPEGydVHqwT3K4gHP1UdUjQVPNRCeuq8JzrWzAqwQGnMKOIFwtcgvE1 pH9Dyb6V08Js3ep2pIHW8JkoSMSC12Is70zYvR8XEkhvUaAW5oDWIXIvXu0u47bGATQJ 50lw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:subject:thread-topic:thread-index :date:message-id:references:in-reply-to:accept-language :content-language:user-agent:spamdiagnosticoutput :spamdiagnosticmetadata:mime-version: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=Dsp/vEL3N09b5PhtqMTzXcMlCaqKe8Qn/fMbxDuViIY=; b=pt/tJp/0O2EivokiDaeNNK5Ef2SiL3VGbw6E85NWnEy7Y5LLmc+8x2T250l6nj0z9K lZO44MoYLTDs7rNht0/KPLW2egupwFiU6QMSabiL9YdrP3q4hYW5EXu5BgUy1E2aK8y1 M3qfpI4MBBl8YvQYgsBCEnwIR+fEkJdXJ4uwdq91XJQRizyOqntYZQDQRYuxvuUqSymj 0xH+9DiI/NKDJ/wVfXcpWROUwNpBZsUVpPYJWnIWUHZdY97pjua0p55Zf/N6ovIFdVq+ zLgB6k89f/Qfn8T1sYQgBnPKxmDIlFHyYXiiOIXyzCyufgDBOOE2YvAMoB8TfgWNQhY0 FezA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlExT3vZAaMH6OanMF5f1OfRXQXB8YiFkcOHwH1MRZ5ufyCMY5wk tzKXdVdsegiRm3AzS/cmsuQ= X-Google-Smtp-Source: AAOMgpdBuPaleyPv2kzs1qmobU2N8FF1gI8vgT/t7PGGqbsT/zqV7dZNHoqFHDPsvj56dJTxOfnqrw== X-Received: by 2002:a50:c941:: with SMTP id p1-v6mr16745edh.4.1531418812794; Thu, 12 Jul 2018 11:06:52 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aa7:d7c9:: with SMTP id e9-v6ls387178eds.7.gmail; Thu, 12 Jul 2018 11:06:52 -0700 (PDT) X-Received: by 2002:aa7:d492:: with SMTP id b18-v6mr1124870edr.11.1531418812227; Thu, 12 Jul 2018 11:06:52 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1531418812; cv=none; d=google.com; s=arc-20160816; b=d7YkYQeeihMld2JUSi47DRWK+UKxoGUVAEeqknTfcOpwBhZnNK/HfkXUZf75VlkejE OQ7orV926vT6OZyHQFhf9gY5+jEQ7HEGK5pvx4DM9BWuO1a/6Dgdd5IjvSo8r6QMtKfC FfSMUBLzXqhvtr1j/b788KKhEJ8f5q3olP0pR01j45K2JFgbMlrDCVNE4ROv/XewrC1H 0YPe5X+22OV+Zw7VZvf4ZqYROcQ1ubRpYF3I8VZ12M5j60aVOALI8kqV5wg2RV639hA6 qPVIfKNRwhFOHe16StjKEgIgv9UmM4lLjl5pGzPkEixgztfWfQ63lJxZi8F5FB9r+lb1 RQDQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:spamdiagnosticmetadata:spamdiagnosticoutput:user-agent :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:to:from :arc-authentication-results; bh=qF6VPEriLgqF6QETFt0njojkxVmOXr0TBOAOPFyWqtI=; b=V8AMPpEnTNClnk9I8KoI3b098FNl2JG1CqvBKnIGXxUQt6D+LV3x69v0oHuf5xXjHM 6l3wOc0Ps/YMyEOqSjT/Te+dxDnHIJNdNFJkcnDjgPP/CGWoeWUB+otGueaXVOZR8iBj ODIRtSTCcomlRPNicORtS4syk5tZgIdmKlO1joGyJj9C9si8kv+AA0K/VPGj2jOfTTPS iCVrwzU1hYBDVKmzo7ogr5vvPkMOSV//2RmNsJPTHatePRn+8r5/4vtxUOnpRoCrnDK/ nUWHKsldijAu2F4uMU6NAR0vin3utoaGy0I9rb6GxpEsPAaVdwWnUwt4V+3rGmGHgW3X 5XAA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.125 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk Received: from uidappmx02.nottingham.ac.uk (uidappmx02.nottingham.ac.uk. [128.243.43.125]) by gmr-mx.google.com with ESMTP id a10-v6si18088edi.3.2018.07.12.11.06.52 for ; Thu, 12 Jul 2018 11:06:52 -0700 (PDT) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.125 as permitted sender) client-ip=128.243.43.125; Received: from uidappmx02.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id CD9202FC82C_B4798BBB for ; Thu, 12 Jul 2018 18:06:51 +0000 (GMT) Received: from smtp3.nottingham.ac.uk (smtp3.nottingham.ac.uk [128.243.44.55]) by uidappmx02.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id 36001310E88_B4798BBF for ; Thu, 12 Jul 2018 18:06:51 +0000 (GMT) Received: from uiwexhub03.is.nottingham.ac.uk ([128.243.15.146] helo=UIWEXHUB03.ad.nottingham.ac.uk) by smtp3.nottingham.ac.uk with esmtps (TLSv1:AES128-SHA:128) (Exim 4.85) (envelope-from ) id 1fdfzP-0007qg-2N; Thu, 12 Jul 2018 19:06:51 +0100 Received: from EUR02-HE1-obe.outbound.protection.outlook.com (213.199.180.175) by mail.nottingham.ac.uk (128.243.15.146) with Microsoft SMTP Server (TLS) id 14.3.399.0; Thu, 12 Jul 2018 19:06:51 +0100 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB1197.eurprd06.prod.outlook.com (10.162.124.21) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.930.21; Thu, 12 Jul 2018 18:06:49 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::1d16:d7f1:1edc:7841]) by VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::1d16:d7f1:1edc:7841%2]) with mapi id 15.20.0930.022; Thu, 12 Jul 2018 18:06:49 +0000 From: Thorsten Altenkirch To: Peter LeFanu Lumsdaine , "homotopytypetheory@googlegroups.com" 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?= Thread-Topic: =?utf-8?B?W0hvVFRdIFdoYXQgaXMga25vd24gYW5kL29yIHdyaXR0ZW4gYWJvdXQg4oCc?= =?utf-8?B?RnJvYmVuaXVzIGVsaW1pbmF0b3Jz4oCdPw==?= Thread-Index: AQHUGfM869FCyiwJTU2EDxUwND6RN6SL8uuA Date: Thu, 12 Jul 2018 18:06:49 +0000 Message-ID: References: In-Reply-To: Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/14.5.7.151005 x-originating-ip: [31.65.72.194] x-ms-publictraffictype: Email x-microsoft-exchange-diagnostics: 1;VI1PR06MB1197;7:7KXgJm3ustCoxQKw5cAwr7NzhJDNu8fJACIireVIbTtSnq9NFEsQsVN1kxxyte8Yeig7AuwNICBZ34WPDJM1PLApV0XP3qd+jWRZiKqU4m1KRUnc/VvatefL/piZRUVyz7bKUeZjf0LbiUjrJiCfRpdnpu8fzKtv/wbB7b7zfmR+p5Xs9cJCkk31RNf6fOoVda7ESNldUcy+u1lnQNiTtVU0H0RzTe1g0kIe9x2SuJd4qsEKxdzGxsyrt6fyFCQc x-ms-exchange-antispam-srfa-diagnostics: SOS; x-ms-office365-filtering-correlation-id: 6e4805f8-8866-4df0-e07b-08d5e8223d0d x-microsoft-antispam: UriScan:(215639381216008);BCL:0;PCL:0;RULEID:(7020095)(4652040)(8989117)(5600053)(711020)(4534165)(4627221)(201703031133081)(201702281549075)(8990107)(2017052603328)(7153060)(7193020);SRVR:VI1PR06MB1197; x-ms-traffictypediagnostic: VI1PR06MB1197: x-microsoft-antispam-prvs: x-exchange-antispam-report-test: UriScan:(215639381216008)(127643986962959)(228788266533470)(85827821059158)(788757137089)(211936372134217)(100405760836317); x-ms-exchange-senderadcheck: 1 x-exchange-antispam-report-cfa-test: BCL:0;PCL:0;RULEID:(6040522)(2401047)(5005006)(8121501046)(3231311)(944501410)(52105095)(10201501046)(93006095)(93001095)(3002001)(149027)(150027)(6041310)(20161123564045)(20161123558120)(201703131423095)(201702281529075)(201702281528075)(20161123555045)(201703061421075)(201703061406153)(20161123560045)(20161123562045)(6072148)(201708071742011)(7699016);SRVR:VI1PR06MB1197;BCL:0;PCL:0;RULEID:;SRVR:VI1PR06MB1197; x-forefront-prvs: 0731AA2DE6 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(366004)(136003)(376002)(346002)(39860400002)(396003)(189003)(199004)(256004)(11346002)(86362001)(606006)(316002)(2906002)(53936002)(102836004)(2501003)(6486002)(58126008)(81156014)(7736002)(486006)(786003)(99286004)(81166006)(6306002)(66066001)(5250100002)(6512007)(110136005)(54896002)(229853002)(2616005)(966005)(478600001)(236005)(6436002)(446003)(25786009)(26005)(39060400002)(5660300001)(3846002)(68736007)(14454004)(2900100001)(186003)(74482002)(476003)(6506007)(14444005)(106356001)(14971765001)(53546011)(76176011)(8936002)(6246003)(6116002)(97736004)(105586002)(42522002)(42262002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB1197;H:VI1PR06MB4029.eurprd06.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;MX:1;A:1; received-spf: None (protection.outlook.com: exmail.nottingham.ac.uk does not designate permitted sender hosts) x-microsoft-antispam-message-info: R4i3wbQDlLnm0fX6Fcket719ojDVtxIyFT+FynC5YIgprqyE0wSBC1cV2Uow7Ngwv7vJFW/qmSW0RyYrjSOm4pKLNST3msaf1mAgZ6pAQJSWTnNRAKg+8uD5F5SEJP6+en3DUZuVQIFGucPRvFiu/55x3hr3xqWPMeLM+BArc8j7ATOHveyrJCB7s5mLrbe2jnd9WCpDgIzALYEka7AWzKdFK832/b4IlgDAF2BUFLb8Fa8ZyjauZFVP49/90Tl+5GGEsdlxmY/x1R9ej0hU2VjIY/Wdeh82a6fjPIR8dcNuYz7vmSdO/pCb88UkajKcqs9/D53LQHTiTIobxGC1BTwdLbStGytDde8C7dwf13I= spamdiagnosticoutput: 1:99 spamdiagnosticmetadata: NSPM Content-Type: multipart/alternative; boundary="_000_D76D4F6CAF3A5psztxaexmailnottinghamacuk_" MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 6e4805f8-8866-4df0-e07b-08d5e8223d0d X-MS-Exchange-CrossTenant-originalarrivaltime: 12 Jul 2018 18:06:49.2514 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-Transport-CrossTenantHeadersStamped: VI1PR06MB1197 X-OriginatorOrg: exmail.nottingham.ac.uk X-SASI-RCODE: 200 X-Original-Sender: thorsten.altenkirch@nottingham.ac.uk X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.125 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk 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: , --_000_D76D4F6CAF3A5psztxaexmailnottinghamacuk_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Isn't this what is usually called recursion with parameters. E.g. in the si= mple typed case for natural numbers: the usual recursor can be written usin= g 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 recurs= ion in every slice. A simple example is addition over the 1st argument, wh= ich 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 distributivi= ty 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 but = I am not sure. Thorsten From: > on behalf of Peter LeFanu Lumsdaine > Date: Thursday, 12 July 2018 at 16:15 To: "homotopytypetheory@googlegroups.com" > Subject: [HoTT] What is known and/or written about =E2=80=9CFrobenius elimi= nators=E2=80=9D? Briefly: I=E2=80=99m looking for background on the =E2=80=9CFrobenius versi= on=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 al= l for other inductive types. I=E2=80=99d be grateful to hear if anyone els= e 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. 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 fu= ll=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) |=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-types, the Fro= benius version is derivable from the simple one. Most presentations just give the simple version. The first mention of the = Frobenius version I know of is in [Gambino, Garner 2008]; the connection wi= th categorical Frobenius conditions is made in [van den Berg, Garner 2008],= and some further helpful explanatory pointers are given in [Gambino, Sattl= er 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 t= erminology. (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. One way to show this is to take= any non right proper model category (e.g. the model structure for quasi-ca= tegories 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 vers= ion. 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 However, 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. 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 gi= ven 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 forgetting som= ething obvious. What have others on the list thought about this? Does any= one have a reference discussing the Frobenius versions of inductive types o= ther 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 =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 "= 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. --=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. --_000_D76D4F6CAF3A5psztxaexmailnottinghamacuk_ Content-Type: text/html; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable
Isn't this what is usually called recursion with parameters. E.g. in t= he 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 r= ecursion in every slice.  A simple example is addition over the 1st ar= gument, 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&q= uot; version of the recursor. I think in the special case of + this giv= es 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= but I am not sure.

Thorsten


From: <homotopytypetheory@googlegroups.com> o= n behalf of Peter LeFanu Lumsdaine <p.l.lumsdaine@gmail.com>
Date: Thursday, 12 July 2018 at 16:= 15
To: "homotopytypetheory@googlegroups.com"= <homotopytypethe= ory@googlegroups.com>
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.&nbs= p; I=E2=80=99m aware of a few pieces of work mentioning this for identity t= ypes, and nothing at all for other inductive types.  I=E2=80=99d be gr= ateful 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.  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)  |=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 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.  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].  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 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.  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  Howeve= 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.  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.  What have others on the list thought about this?=   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  =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 Homo= topyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://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 http= s://groups.google.com/d/optout.
--_000_D76D4F6CAF3A5psztxaexmailnottinghamacuk_--