From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.8 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE,UNPARSEABLE_RELAY autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-lj1-x23b.google.com (mail-lj1-x23b.google.com [IPv6:2a00:1450:4864:20::23b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0b2730d6 for ; Thu, 25 Jul 2019 09:58:32 +0000 (UTC) Received: by mail-lj1-x23b.google.com with SMTP id s7sf10651850ljm.5 for ; Thu, 25 Jul 2019 02:58:32 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1564048712; cv=pass; d=google.com; s=arc-20160816; b=UAvsOSq5v/zCIz4WH4/K0ySWIBo806f3EjUDk4VN8XP6Da0eHAgaWe1Hq7C0Zei4g+ 3rY1Efod0xgjjYRlmww+lJGIGMSNUltQRcSF3yapkxtOWEQhwDxrt3HmnGaJpz7ZlLWy Ki1qNM3Z2jfSbIQvke8Qlfg5yYf88meOeXW/pFVQSy7IaVM2lH3pgEwwZbBHMf3kjn4O bIElcu+nespcam4UR93t3peFFH4vvX/JwItga7+ZcuNuL9ViqUOuPmqaGRmhl/AJkMTR fR/t1we0uU0bWI/ZYnLZpC7lJ9fSw3L7um6jBg6pk9GzkTdPAjIuJopFFNUClP1IN3uC C6zw== 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:content-language:mime-version:user-agent :date:message-id:to:subject:from:sender:dkim-signature; bh=gvJE3Qo6Opu3dO2vn+q+Pq0PNZfPS5oidzwpTyc566g=; b=1GMMbHh1AGEmuH46UVzXR4Z5KyovzNChMKbFmo3lrG4e6DXhznL4Y4UiIqgFkTSSbC a+Skd9xC4Uv6BCK9bxU7qZAChaRhjT+X7U6Uvs1ti4MX7qOZjJ+f3cAIESbeymC43blx mkU8iEusyJxIcAn520VFI8+APqbBBJK1mtLZBt0sqprYfY8zCUXqeF8vxjFBimPvby8O V76hdb6BU7rjO2nnRJ7DrhCy4Yp7P3t3Cdgr5WQtcuKbWxvMfRGj7fAimNrJoWdHDWBM vyX1SVS/zgf/x1MsY7LMmvinJxktlaipaCQcsOEBU4ibrtdm2/NfCQz1je6kFCgGBKON Ks2g== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of rafael.bocquet@ens.fr designates 129.199.96.40 as permitted sender) smtp.mailfrom=rafael.bocquet@ens.fr DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:subject:to:message-id:date:user-agent:mime-version :content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=gvJE3Qo6Opu3dO2vn+q+Pq0PNZfPS5oidzwpTyc566g=; b=VU5+BnbFu3I8ACX1lvhAgzpwznid6tG4DqHGyi7qAWMMptpTRA5Vd6SdyRBj5nPy1u SW+Zx9j2s3CG09xcRml4jLaNBn5boXVDcBm9V6cF2psAbd1OwEyciub+YbM90OSKnk7j fZMstCcVsJ0sDnWs55wtnNdAYtZ8HAcIYbcXxQjWaF7Kw5GDBraCsuFcsdGLn1+fzxcH wOKVugnfs9ABTJmZoEBFSKgMVAhxaMUrhCheMWEpP9shGb9WDn1Bhlm7IkLZNym+2bNB cRxh9ZUytovUNBJzBg02eJKJybaTPHRvQooWx6gU0N8Qcf6KgS/fuuhassyUXZlUQ00t 0amA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:subject:to:message-id:date :user-agent:mime-version:content-language: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=gvJE3Qo6Opu3dO2vn+q+Pq0PNZfPS5oidzwpTyc566g=; b=hEOE6gKcvZFmZIt7gfjzLiwqtTD8CACiG6gd6In2/gxmMrfL217sQJifRDFZMASPtn xWQBC4pibCZpdIgeC5o/MKE0fQGMhlcx4BrakVSy6dgkzYFsoXrVa1zHCjnU94/39skZ kc63HUwpH1yqkzYnTApuOTIpRxU6HGn4Bfmwy5cNFdxIFS2GGqmLuDjMQNQnUFoD2fUU elc3Mk/xaklwnkwwNk/mYCTj9YQXth7i6mvg5uN9TceZuWPc1jHsHmrx93mj1J+tfnvY Z3KXVk/fBgnUT1SjPSs7sJfiRd5Xc1xDQQwjP41YBnasx1kTPUrkjLqX2TVm8DalY/xR IvXA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUhgTot14yfOuTRyEnSbYAw6GjH7N3SK2WHXt9k6ZMpbtGMT3w8 Elu76+CVaPSIWW/jO2QMJNU= X-Google-Smtp-Source: APXvYqxWB7EIjRhfl4F+/0QefuOamw6gtQBKMgOOxYM11RP55GQg7A4AiuhWWR4wj+I5YhCi3sId+g== X-Received: by 2002:a2e:8e90:: with SMTP id z16mr23785001ljk.4.1564048711870; Thu, 25 Jul 2019 02:58:31 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:8198:: with SMTP id e24ls5634063ljg.15.gmail; Thu, 25 Jul 2019 02:58:31 -0700 (PDT) X-Received: by 2002:a2e:9213:: with SMTP id k19mr42868643ljg.237.1564048711337; Thu, 25 Jul 2019 02:58:31 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1564048711; cv=none; d=google.com; s=arc-20160816; b=BTVHQtkF1hPhSIJFwPL6XvcOxKiLJ5s4syL9fuamdRctj6vJ+1fKEwLunlMcqpv1pH DceEZ7DnhmRhdeY054o13mW2d2bqqpa9HRQ8o5NmHkSt06JcmQr3thdjYw/u1jUPwWk5 gYB+KUvTWF8UEbtneJZdQryJOVjr9kGFhyFia9P5uRvOF7xsoPv1pfXX7/zM2x6sLEk+ pXMzrGLVxU3sqZXuFxGhPuYpTA4U11QKTawBT4/GW11U+38U9Q0tNMkNrKXFd6NhNfwN uzKp3rwVPgOQ7IC6cllpEXv13JYEh1+YJgaLiubPoYsxoTauKJFkNMNPkUKvOvehGZBX gbvQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:mime-version:user-agent:date:message-id:to:subject :from; bh=UhYadL74UwexMmesJqRO96jNWdshakZzlkM68Bm90nI=; b=IqhKJNXTGWoDDbWV6bmF6FADkkkZPudqW4xhUP2a6PEKdUYP427t4Y07lhSETK4gDI c5k3J23iT2TqpnZUErBR0U+E7+XVh/gCM6h1cU6e6wtL5g+cgtyMCnb8iAZnw//X90Uk N1DqSXol8GVOq9deKTcvemi7eV++36U3LV/wltAxPk6UBhVzKDdb5u0vc6+pZpQKweiO KJTD4OmLGAow8tl9uCtipkDI4HrlKAwTz04XY+hoQbb04i0Bk6FciQaj7RrbKP6TiT/y FUJzX1JM95ZI1cnJTZd8ZFCclkroXOsCc+Jzh55hQBKMYxYV13o1H9No2N9KMzWLD1E5 mg7g== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of rafael.bocquet@ens.fr designates 129.199.96.40 as permitted sender) smtp.mailfrom=rafael.bocquet@ens.fr Received: from nef.ens.fr (nef2.ens.fr. [129.199.96.40]) by gmr-mx.google.com with ESMTPS id h11si2603903lja.0.2019.07.25.02.58.31 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 25 Jul 2019 02:58:31 -0700 (PDT) Received-SPF: pass (google.com: domain of rafael.bocquet@ens.fr designates 129.199.96.40 as permitted sender) client-ip=129.199.96.40; X-ENS-nef-client: 129.199.1.22 Received: from clipper.ens.fr (clipper-gw.ens.fr [129.199.1.22]) by nef.ens.fr (8.14.4/1.01.28121999) with ESMTP id x6P9wUjR026167 for ; Thu, 25 Jul 2019 11:58:30 +0200 Received: from localhost.localdomain using smtps by clipper.ens.fr (8.14.4/jb-1.1) id x6P9wTnM071483 for ; Thu, 25 Jul 2019 11:58:29 +0200 (authenticated user rbocquet) X-ENS-Received: ([37.164.137.80]) X-Envelope-To: From: =?UTF-8?Q?Rafa=c3=abl_Bocquet?= Subject: [HoTT] Frobenius eliminators To: HomotopyTypeTheory@googlegroups.com Message-ID: Date: Thu, 25 Jul 2019 11:58:26 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.7.0 MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="------------0D36F11CA71F222A9E17B4AD" Content-Language: en-US X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-4.4.3 (nef.ens.fr [129.199.96.32]); Thu, 25 Jul 2019 11:58:30 +0200 (CEST) X-Original-Sender: rafael.bocquet@ens.fr X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of rafael.bocquet@ens.fr designates 129.199.96.40 as permitted sender) smtp.mailfrom=rafael.bocquet@ens.fr 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: , This is a multi-part message in MIME format. --------------0D36F11CA71F222A9E17B4AD Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable This is related to a previous discussion on this mailing list :=20 https://groups.google.com/d/msg/homotopytypetheory/b96TBt0Bn7Y/IiAcnUL2AQAJ= ,=20 "What is known and/or written about =E2=80=9CFrobenius eliminators=E2=80=9D= ?". I noticed recently that the Frobenius eliminator for identity types is=20 related to the notion of strong logical equivalence (the trivial=20 fibrations of the left semi-model structure on the category of CwAs with=20 Sigma and Id introduced in https://arxiv.org/abs/1610.00037,"The=20 homotopy theory of type theories"). The Frobenius, Paulin-Mohring variant of the J eliminator is presented=20 by the following inference rule: =C2=A0 G |- A type =C2=A0 G |- x : A =C2=A0 G, y:A, p:Id(x,y) |- B(y,p) type* =C2=A0 G, y:A, p:Id(x,y), b:B(y,p) |- C(y,p,b) type =C2=A0 G, b:B(x,refl(x)) |- c : C(x,refl(x),b) type =C2=A0 G |- y : A=C2=A0=C2=A0=C2=A0 G |- p : Id(x,y)=C2=A0=C2=A0=C2=A0 G |= - b:B(y,p) -------------------------------------------------------- =C2=A0 G |- J(A,x,B,C,c,y,p,b) : C(y,p,b) (where "B(y,p) type*" means that B(y,p) is a finite sequence of types=20 over "G, y:A, p:Id(x,y)", i.e. a context in the contextual slice over=20 "G, y:A, p:Id(x,y)") (In the discussion linked above, Valery Isaev gives a proof that if the=20 type theory includes sigma types, the "simple" Paulin-Mohring eliminator=20 is strong enough to derive the "Frobenius" variant. This is also proven=20 by Paige Randall North in https://arxiv.org/abs/1901.03567, in a more=20 categorical setting.) I consider roughly the same framework as in "The homotopy theory of type=20 theories". Recall that a contextual morphism F : C --> D is a strong logical=20 equivalence if it satisfies term lifting and type lifting conditions: - type lifting: for every context G in C, F_G : Ty_C(G) -> Ty_D(F(G)) is=20 surjective. - term lifting: for every context G in C and type A over G, F_A :=20 Ter_C(G,A) -> Ter_D(F(G),F(A)) is surjective. Let C be a CwA with Id and refl. The J eliminator for some pointed type=20 (A,x) in some context G can be seen as the statement that the contextual=20 morphism F : C[G,y:A,p:Id(x,y)] --> C[G] (where C[G] is a notation for=20 the contextual slice over G), sending (y,p) to (x,refl(x)), satisfies=20 the term lifting condition. Indeed, the input of the term lifting=20 condition is the data of B, C and c, and the output is a term J in the=20 context G,y:A,p:Id(x,y),b:B(y,p) of type C(y,p,b), such that F(J) =3D c. The type lifting condition can then be derived, assuming that C does not=20 include weird type equalities (for instance, when C is cofibrant/freely=20 generated, or when C is equipped with a hierarchy of universes ensuring=20 that every type belongs to a unique universe). If we only require F to be a weak logical equivalence (a weak=20 equivalence in the left semi-model structure), then we obtain=20 propositional identity types. I think that asking for F to be an=20 isomorphism forces the identity types to become extensional. Has this been studied before ? Can this be extended to the elimination=20 rules of other type formers ? Best regards, Rafa=C3=ABl Bocquet --=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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/a20122bc-289b-4fce-1183-76b66aed395f%40ens.fr. --------------0D36F11CA71F222A9E17B4AD Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

This is related to a previous discussion on this mailing list : https://groups.google.com/d/msg/homotopytypetheory/b96TBt0Bn7Y/Ii= AcnUL2AQAJ, "What is known and/or written about =E2=80=9CFrobenius eliminators=E2=80=9D?".

I noticed recently that the Frobenius eliminator for identity types is related to the notion of strong logical equivalence (the trivial fibrations of the left semi-model structure on the category of CwAs with Sigma and Id introduced in https://arxiv.org/abs/161= 0.00037,"The homotopy theory of type theories").

The Frobenius, Paulin-Mohring variant of the J eliminator is presented by the following inference rule:
=C2=A0 G |- A type =C2=A0 G |- x : A
=C2=A0 G, y:A, p:Id(x,y) |- B(y,p) type*
=C2=A0 G, y:A, p:Id(x,y), b:B(y,p) |- C(y,p,b) type
=C2=A0 G, b:B(x,refl(x)) |- c : C(x,refl(x),b) type
=C2=A0 G |- y : A=C2=A0=C2=A0=C2=A0 G |- p : Id(x,y)=C2=A0=C2=A0=C2= =A0 G |- b:B(y,p)
--------------------------------------------------------
=C2=A0 G |- J(A,x,B,C,c,y,p,b) : C(y,p,b)

(where "B(y,p) type*" means that B(y,p) is a finite sequence of types over "G, y:A, p:Id(x,y)", i.e. a context in the contextual slice over "G, y:A, p:Id(x,y)")

(In the discussion linked above, Valery Isaev gives a proof that if the type theory includes sigma types, the "simple" Paulin-Mohring eliminator is strong enough to derive the "Frobenius" variant. This is also proven by Paige Randall North in https://arxiv.org/abs/190= 1.03567, in a more categorical setting.)

I consider roughly the same framework as in "The homotopy theory of type theories".

Recall that a contextual morphism F : C --> D is a strong logical equivalence if it satisfies term lifting and type lifting conditions:
- type lifting: for every context G in C, F_G : Ty_C(G) -> Ty_D(F(G)) is surjective.
- term lifting: for every context G in C and type A over G, F_A : Ter_C(G,A) -> Ter_D(F(G),F(A)) is surjective.

Let C be a CwA with Id and refl. The J eliminator for some pointed type (A,x) in some context G can be seen as the statement that the contextual morphism F : C[G,y:A,p:Id(x,y)] --> C[G] (where C[G] is a notation for the contextual slice over G), sending (y,p) to (x,refl(x)), satisfies the term lifting condition. Indeed, the input of the term lifting condition is the data of B, C and c, and the output is a term J in the context G,y:A,p:Id(x,y),b:B(y,p) of type C(y,p,b), such that F(J) =3D c.

The type lifting condition can then be derived, assuming that C does not include weird type equalities (for instance, when C is cofibrant/freely generated, or when C is equipped with a hierarchy of universes ensuring that every type belongs to a unique universe).

If we only require F to be a weak logical equivalence (a weak equivalence in the left semi-model structure), then we obtain propositional identity types. I think that asking for F to be an isomorphism forces the identity types to become extensional.

Has this been studied before ? Can this be extended to the elimination rules of other type formers ?

Best regards,
Rafa=C3=ABl Bocquet

--
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/a20122bc-289b-4fce-1183-76b66aed395f%40ens.fr.
--------------0D36F11CA71F222A9E17B4AD--