From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCR53C7ITYGRBGPBTXNAKGQE77MCECQ@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-x237.google.com (mail-oi0-x237.google.com [IPv6:2607:f8b0:4003:c06::237]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 52e49f13 for ; Thu, 12 Jul 2018 15:15:40 +0000 (UTC) Received: by mail-oi0-x237.google.com with SMTP id 22-v6sf6991541oix.0 for ; Thu, 12 Jul 2018 08:15:39 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1531408538; cv=pass; d=google.com; s=arc-20160816; b=Sq+zaW3BXmO9I9tAY3I001xmxndFhM67mfMvb+P6PnK7XZNogFcCKHf4kLTTjXXKVQ YQivsvwNm7ywEUhvYRFKXVxbkqg7+JSqafikEKctPqi1ej1hHyVdQleSw7BdCHFFYfJj ryRgjrHZpFP43z/dxNZ0PC7Q1381jTjJ15g+KgECbyFLtMpCNyBlhAt/zcGW2Kw9SKuD ZQLvB64rH6b+T5gmf39KxS6tvTaaoOeEiXQO5f91J8pMdx3QoHLvunfxlZEfgdYVeRyS gzP3dMOX5sqcBuhjjE/QdE2bz6QqA4U1HE/KgHZrWPnWGDq4xs5EcEXfmGBAH/I2sxKH 4DlQ== 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:to:subject:message-id:date:from :mime-version:arc-authentication-results:arc-message-signature :sender:dkim-signature:dkim-signature:arc-authentication-results; bh=+wsM5oV/gGXl1STsrlJ52uVCnZtFBzhN/OlQ/wck7N0=; b=N/17lp+Sujt5eanp7II+juvn9hUPsLJVdKdiZx0tL/JPOXll7sficJbkMbAugOf40v alLobRQ2maCLIrk8dF+vgTFIquUPOwQVZls/1q4VIYm9jrkKAo9vsbnuRp+gR5TdSqax 7Q9UW8n3jB+AOVq7/rIfPRY7AMqDz36wdceTMTyQBrdAC2tRED/6iMEfp+W7AT+czHqL Ov6LLDN43xn3pGsh3AT6zwFqeTaLyz1DTPDtAwwwjuoixNrW30IAi5GNoRz67Bx1AGIE 2mJlez6z7AVZH20LvwdytI2FyBzTJtRoNvwfF8bKgckDJPOs47S9TCUaNq0d9fkEn1jM yayw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=EkkPRD1X; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2607:f8b0:400c:c08::22d as permitted sender) smtp.mailfrom=p.l.lumsdaine@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:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=+wsM5oV/gGXl1STsrlJ52uVCnZtFBzhN/OlQ/wck7N0=; b=SiEwxGIiZbnRb7bm7Pyi4hqUz2w7+dv36bxi24tCn9GQmO+TkzUlppNJYq0PHp0XRr hkDjp/avhQlqjmU/9h+GjDimaqi3acvlJrHlrCCvISZJiexwHbiuWCPvL+kSKKbaCAy2 /Pg9yz8smQeUS2dbo6vLxFjhCEaQYa6Aw8CMBbjeHn4Pu8ckKL0cpAXL8IorFJcmUxa2 ym1cqGoELeUSRN7NOuTDOwHVm+kU15YwAAU8mx3+/Nd4FtU5gGGmT5p7Z4wGIRxBUdTP MJkjHiq0bJmCd4/HtIexAN5zmYJpYJjD+ZJtFkbAU6x9KtkgerJTnACkLOOgj5rY0u9i NDgw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=+wsM5oV/gGXl1STsrlJ52uVCnZtFBzhN/OlQ/wck7N0=; b=oCM5L719To/XPmBLM8fcLf7Nm9wfzPaulra9IUTK/t0bb7AZg7IYBUvuihTRpZhSM1 EiKJiBFHf40xiGlfDUBgshA/vBOYn+T2QdgOdGiVaRJN4kHjebDbLY2RepKzF7JVOPKU L/1LkfthOCWuXAi+fNnX1TlXLZWq1NJHTfBcpNAApifnr681pztv0/vxxygMKnKsPrpD 9MuOwhDNDoORWwRLsorIG1bnMFUAPx3vgyuEbqFn0Q9xSzT2U+qLqZpASLKMLMAZAHIp 5lnskfy1VtY8lk5feFncaCfLLz2E0stRVHmqX1B2727rSw38Ydg7L7+OLiL3Sx7K1gBP AMcw== 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:from:date:message-id:subject :to: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=+wsM5oV/gGXl1STsrlJ52uVCnZtFBzhN/OlQ/wck7N0=; b=Auq8Q8JAkPF6gTkLXoQl80DxyMlmJT1IwG+gOOGXqy6AC19j99zwCZ18dLLhMY7aRs K6frzbwZXo/A/U+yHDBje1nsfvgRUycNMwk4kEnO8bg/p4Vspn0PPKLgrATRt8mXin18 G758RhRWP1BKZpYqhWf45gQdq2qA1kTBpOLJFWs0yanz97p+iDeCZkIMiFsRdfnIzzMb IykMFwpSgrg52cWi6tFj3+kxCdHvUsMO59Y1jow22WPyxS2/voDrm9otrYZhfQiEu4Md Qp+5QhJe4JI7BFcfy7PWbOgS91oL5DmJ0zbrROmvaWbiqNpI1weItNuQ/UkV2emRb9K3 dyVA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlGRZjUAi2ckMAoGxG0rie34B8Gr77gqkfh6nV4YXCWwb1q8fMXG 3OVNorXomrHY1obDi2EB1bE= X-Google-Smtp-Source: AAOMgpe6iJSLg5FEcmwoIZjKENBz9rNAUPNCQxQF8z2t8MfHXBbYCCo4Pu/RgV2B8B9rx1syPuzm6Q== X-Received: by 2002:aca:de07:: with SMTP id v7-v6mr569462oig.5.1531408538166; Thu, 12 Jul 2018 08:15:38 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:e610:: with SMTP id d16-v6ls14611577oih.2.gmail; Thu, 12 Jul 2018 08:15:37 -0700 (PDT) X-Received: by 2002:aca:6087:: with SMTP id u129-v6mr1659280oib.92.1531408537667; Thu, 12 Jul 2018 08:15:37 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1531408537; cv=none; d=google.com; s=arc-20160816; b=kPZ5sTMt9QpX7N9gG73kthEDrvtRSHcpam9ipZen9jXdC2AR1R2pFkhsWrWzpbn96z OkbU7C1golueK3/wPtL3Qs+iR1lFnJlQWfqWXMQNAB8C3zH1W4nHPxEw3XXS+BCbCWs+ Dt4Ac753iJ9tlE/GV8a4O0+eFVZ+tTZS3dsr0vjLPLCCiwbpLCTdBiZXGb0jWhrJM2bd gRoEHKylTYYJSc3FUtunAKXQDYs0Izo/mWzz3o9NQzYHC5FyP7hgNLFuOd0eY29dDFYM eLLR2urbYV1BnQkUZDvXfhCJE0F7AHVeKxHJtkWHug3ETh09TTqHjY9KoVRExXR1wduw F1vw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature :arc-authentication-results; bh=G5Xg0XVHa5bNT5Do/Qgywci2r0WNIfpvOhPX560POwg=; b=eZI6QaFfjLPc6R8aRpFUIFctbSX7grhOrksBmlQzg/7hDSe86IgXbJoQp38YBYDO0R wjRJ5CYclRxHvnAZea7ZHA1/iQ88xp4w+/90F2quJnS3LnEsJC/hFNRzuR55wbQ3/RUJ vYg0emsJRMnhJaLBMcJm//KvOiPywXZ6lR7OIXjkhqpq1X840rKcFBIqofBl8qVg+6az 0vd8JB/q50JD1Yqc9k/BsV/CnBGtf8CVF6WUc4PZlowYUpI+Zcdq9EUjor0HiM1vOMcy kuoOtcnWIbuEbAAAz737+61XR3h5U+5/lvutldLqv0Vq2oOLTtHowRzzwOedEhLyEOk/ EqEw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=EkkPRD1X; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2607:f8b0:400c:c08::22d as permitted sender) smtp.mailfrom=p.l.lumsdaine@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ua0-x22d.google.com (mail-ua0-x22d.google.com. [2607:f8b0:400c:c08::22d]) by gmr-mx.google.com with ESMTPS id m132-v6si527816oif.2.2018.07.12.08.15.37 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 12 Jul 2018 08:15:37 -0700 (PDT) Received-SPF: pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2607:f8b0:400c:c08::22d as permitted sender) client-ip=2607:f8b0:400c:c08::22d; Received: by mail-ua0-x22d.google.com with SMTP id t14-v6so18657522uao.8 for ; Thu, 12 Jul 2018 08:15:37 -0700 (PDT) X-Received: by 2002:a9f:318a:: with SMTP id v10-v6mr1714271uad.36.1531408536783; Thu, 12 Jul 2018 08:15:36 -0700 (PDT) MIME-Version: 1.0 From: Peter LeFanu Lumsdaine Date: Thu, 12 Jul 2018 17:15:25 +0200 Message-ID: Subject: =?UTF-8?Q?=5BHoTT=5D_What_is_known_and=2For_written_about_=E2=80=9CFrobeni?= =?UTF-8?Q?us_eliminators=E2=80=9D=3F?= To: "HomotopyTypeTheory@googlegroups.com" Content-Type: multipart/alternative; boundary="000000000000d74f1b0570ced51e" X-Original-Sender: p.l.lumsdaine@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=EkkPRD1X; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2607:f8b0:400c:c08::22d as permitted sender) smtp.mailfrom=p.l.lumsdaine@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: , --000000000000d74f1b0570ced51e Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 o= f work mentioning this for identity types, and nothing at all for other inductive types. I=E2=80=99d be grateful to hear if anyone else can point me to anyt= hing I=E2=80=99ve missed in the literature =E2=80=94 even just to a reference th= at 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 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 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 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]. 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 refe= rences 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 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 other 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 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 the= case, it=E2=80=99s eluding me now. On the other hand, I also can=E2=80=99t think of a countermodel showi= ng the Frobenius version is strictly stronger =E2=80=94 wfs models won=E2=80=99t d= o 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 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 som= ething obvious. What have others on the list thought about this? Does anyone have a reference discussing 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, 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 --=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. --000000000000d74f1b0570ced51e Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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 literature =E2=80=94 even just to a reference that lays out the Fro= benius versions of the rules for anything beyond Id-types.=C2=A0 The proxim= ate 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 p= aper by writing them all out in full=E2=80=A6

In more detail: Here a= re 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)<= br>=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)

(w= here =CE=94(x,y,u) represents a =E2=80=9Ccontext extension=E2=80=9D, i.e. s= ome 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 versi= on=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 T= he simple version is a special case of the Frobenius one; conversely, in th= e presence of Pi-types, the Frobenius version is derivable from the simple = one.

Most presentations just give the simple version.=C2=A0 The firs= t mention of the Frobenius version I know of is in [Gambino, Garner 2008]; = the connection with categorical Frobenius conditions is made in [van den Be= rg, Garner 2008], and some further helpful explanatory pointers are given i= n [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 su= ggestions 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 take any non right proper model category (e.g. the model structure f= or quasi-categories on simplicial sets), and take the model of given by its= (TC,F) wfs; this will model the simple version of Id-types but not the Fro= benius 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-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/abs/0803.4349- van den Berg, Garner, 2008, =E2=80=9CTypes are weak =C2=A0=CF=89-groupoi= ds=E2=80=9D, https://arxiv.= org/pdf/0812.0298.pdf
- Gambino, Sattler, 2015, =E2=80=9CThe Frobeni= us condition, right properness, 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 http= s://groups.google.com/d/optout.
--000000000000d74f1b0570ced51e--