From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCR53C7ITYGRBF4CULNAKGQEOAHQUQA@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-x23e.google.com (mail-yb0-x23e.google.com [IPv6:2607:f8b0:4002:c09::23e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 70a08e33 for ; Fri, 13 Jul 2018 10:38:17 +0000 (UTC) Received: by mail-yb0-x23e.google.com with SMTP id x14-v6sf30138366ybj.9 for ; Fri, 13 Jul 2018 03:38:16 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1531478296; cv=pass; d=google.com; s=arc-20160816; b=BFCJamI6p3Sp9Ri4eW4WHWAcsIAHgHe23Hy9vl+H43C4hcYBUiyyl9YUVI5m6nYR9r 4XQPazVizk/ItQOlPvhTFzF1FJzjx7op1WHSTkPVSXpcvdrP3PE2XcaNed5MocU77k20 KR6zTDVMtvNmCkk+A8ircm/CT8ry4u3vyKhzGUMs6ntGHpmwrj64vRRC9TBBhQ2zQ+zp rcrrSwhaF6W+hARoJL4ewD28auiDNnvriY+KxlD09e+UpJG+N5T/HJSLsptxkl2P3eWY 4ydNHvkMCEG6pA4exrUDLLwigU5qBH34OZ6pDZ3pHvygXRe9LVDiGOhToeyD1jN0lYZz zaBA== 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 :in-reply-to:references:mime-version:arc-authentication-results :arc-message-signature:sender:dkim-signature:dkim-signature :arc-authentication-results; bh=V+Kww4uXZyBFGNdXF3C6VNShAOPYDct/qiIeeikBLkA=; b=k/acD9+uuLM1zUW6+/Cmoe/DWQjoyRgA/WHPf8uW6r0jP3+xYxVWe0Mo+He8ovfAVY 4cWgmmDT/XMxQrPsH95szwFjuckiPjpqvHjX1d1POrdY4TSrio8/W8Vm9ARR3yREZyi4 y54+f3xkXHgXGb32DhUybgCAbl9ViIb7PQZuwf3lueJurhCTQYR9JKMffRBwTymKgsUj WIt79Ez6MlSJmPnrNDg9e/pDHFzO/pozVDsIz7IwrBX+oWEYbeMFR0/FdYaPLWxMCiaS NU3zKT0VW4RWUbkRSm2KjYXT5rik7PmbljmOkxXI6VQoUnlkYnOWmn74CQtQhvdlPe1s w5Lg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=A9O4nqZQ; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2607:f8b0:400c:c08::234 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:references:in-reply-to: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=V+Kww4uXZyBFGNdXF3C6VNShAOPYDct/qiIeeikBLkA=; b=HdICgP9eKm9WV8hSw1YI3jchbqwbimYLjdfQKhCT8cSD3z+mCbEG8bAqhEMElMzN1O d1Xgxh4B6kCkbvyaWebqUBl2IEjN4rMS+0dakxk5BWCEfMI9zlNJgoYUP0oB+mMHp8Sw l87XETI54U52HnGMmjPjwtD93KKrd7yYHJXXqc4Oxk1/aVNhKrHxpWfrFQunCUQCMLR6 EWz4VKQYHDXB3kAF5XpXmHfSnH3Z5H6iY1OH3LR82JlB3m4bkLjjnF5ep0eaOv8tCtwE Q3lZW1GFzNS2MkkoIXAj6ToYtXQCLNKZR3WTGhDl0feJDrTZd0RmP31F2ESSpAFGeZXs L+qw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to: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=V+Kww4uXZyBFGNdXF3C6VNShAOPYDct/qiIeeikBLkA=; b=eC5AQz/FDmRKgnQ5YhlNoUiJ8Z22zH8ilDSb0yyJi44S0+00FBbQOkTUwYbakduKFE MOL6YWIiFdsb/BXoAqsh6ciGMDnJXAs1PuA2GXxJIyEJcWkGB+CJnxnVJxlfgfOT2c/S e/uLkHqC0Q2ebRR+zgpQIvGqPOZ7g7akAdXkeA5qrGCzvbortiO/81icXCtVHVFixrbB 8Rr+iJInq9Rj8HWMQgE/86SDXbwwwptnDUldvSvRVMbKnPveM4nagTZZ/40mPFPg+kR9 +YjFFhiaroREFicY0YgQWAfPE98ZG2ATWXqCeUYGyWfbCI6tY73zd40SQ0CRHyynqVl6 8Lww== 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:references:in-reply-to: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=V+Kww4uXZyBFGNdXF3C6VNShAOPYDct/qiIeeikBLkA=; b=NNrURjylTtQsnLP6wbKcvqSusUd6wgWaePYnFpMwvDirkrm3CL8dY43/rjvWiBhUkx G8nUKF+2y3e+f64wLATtTwutx/Xb8ursL9o6odEP9YSh5BPyuzDJhCXf8W/AOR77Hz+6 DPXB9uOdWt2dOENXKkwoCT0KX5HK/gjCYSZoYomBZO5brFs5hDNokSPgb7tmSmbE+qap F+Tl7v/XCtbKLw0mHqRRymHFYCsr2QXgLwjof3VEqcbRtDhsbhzJr7ScrjzPT/XMScAR bnX7URtmliYEQrzfMDcw0Qnaq4kaHbq5DIKKpzgnTU+UWFa2OR/lQPf8UO++sPRqSwZO wuPA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlGQGR/sxTy/sOsF+u9rnZM/bz73H7jt6/vAHvFsPfe1/NRJR+iX awkq+ius+sgsumqlQq3GKXk= X-Google-Smtp-Source: AAOMgpf9HLccl2/C9ruS50wqfWt66OwsD5Um5jrMqn+EObPW3E4iKDSmcsUvrwWbDU3GsD+Ei0k0Xg== X-Received: by 2002:a81:5705:: with SMTP id l5-v6mr567644ywb.6.1531478295968; Fri, 13 Jul 2018 03:38:15 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:5c0a:: with SMTP id q10-v6ls541922ywb.31.gmail; Fri, 13 Jul 2018 03:38:15 -0700 (PDT) X-Received: by 2002:a81:2656:: with SMTP id m83-v6mr1773950ywm.73.1531478295614; Fri, 13 Jul 2018 03:38:15 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1531478295; cv=none; d=google.com; s=arc-20160816; b=XRDKn2rUbdKNsdznirojm1QqLWNCB+Fxi/Tk4AR3iHTXzUmjtkQTHkA7I0G4xOwB8l zl3IqXqDQkJ1tbfThKkKmcDtZ5AJMW91uoXGS7jXtMfHo1OOkoO/g4k13ssRmdSa1Pm2 DF+ulq5O9A4FHqpraEu/sF60jzKuEx2ZM8lQmsfk/CWJXyCi2fkqP65DB1lpunOzTfE0 jBS32XMbIBJ53j9DKnHifAOp+mhCi/MOAa31wXN6sIfK64Rt4bRcKCka4xAKH2EIWWh2 s9q3AmzyDHFdJdYO9qXHs9swuBsJGFZdDH/h6n1l+9/OZKHZuh/WxEIB/4ZY4ENgup0F 3CvA== 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:in-reply-to:references :mime-version:dkim-signature:arc-authentication-results; bh=0K1WrKY6UfN9df98M6sXYjkxvQk9mNep3z+XkRHM9vM=; b=lCQlvdo9Xu4uWyijVwzgea3dv8xAiKndH+oExV2MTH1mJSatTA+na/dzyTbaSQDjq8 LrNW8zOLxbwoWNOxiCW2SIDIJq5hVlQToVMrkeH1RQPRN8WRp63yCPKypGA5tyXUCyOH Bf6NwCQAQQ4WN/2G15S3gG5wk65Z+7rpmPhIgGw6zb7q931wnX70wsDFUtJ4srCcsvJ9 YETiU245xGhK4+lfJBmrw6AtuV4ceCEQZfuRxYLRbawiOz0HQEx7bavcsoytFp3OfKp5 D+fBDszpg5MWNOqCmFxapNqf9se0KHCFwJFJbpxQnsl541Rmj8eoXfQNgmvmjxMdVoF0 Cxfg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=A9O4nqZQ; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2607:f8b0:400c:c08::234 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-x234.google.com (mail-ua0-x234.google.com. [2607:f8b0:400c:c08::234]) by gmr-mx.google.com with ESMTPS id v79-v6si1555883ywc.2.2018.07.13.03.38.15 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 13 Jul 2018 03:38:15 -0700 (PDT) Received-SPF: pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2607:f8b0:400c:c08::234 as permitted sender) client-ip=2607:f8b0:400c:c08::234; Received: by mail-ua0-x234.google.com with SMTP id x24-v6so20316586ual.10 for ; Fri, 13 Jul 2018 03:38:15 -0700 (PDT) X-Received: by 2002:a9f:318a:: with SMTP id v10-v6mr3849502uad.36.1531478295326; Fri, 13 Jul 2018 03:38:15 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Peter LeFanu Lumsdaine Date: Fri, 13 Jul 2018 12:38:03 +0200 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: valery.isaev@gmail.com Cc: "HomotopyTypeTheory@googlegroups.com" Content-Type: multipart/alternative; boundary="000000000000c6341c0570df13df" 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=A9O4nqZQ; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2607:f8b0:400c:c08::234 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: , --000000000000c6341c0570df13df Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Thu, Jul 12, 2018 at 7:07 PM Valery Isaev wrote= : > Hi Peter, > > I've been thinking about such eliminators lately too. It seems that they > are derivable from ordinary eliminator for most type-theoretic > constructions as long as we have identity types and sigma types. > Thankyou =E2=80=94 very nice observation, and (at least to me) quite surpri= sing! > I mean a strong version of Id: > Side note: this is I think more widely known as the Paulin-Mohring or one-sided eliminator for Id-types; the HoTT book calls it based path-induction. 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 i= s >> to take any non right proper model category (e.g. the model structure fo= r >> 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. >> >> Are you sure this is true? It seems that we can interpret the strong > version of J even in non right proper model categories. Then the argument= I > gave above shows that the Frobenius version is also definable. > Ah, yes =E2=80=94 there was a mistake in the argument I had in mind. In th= at case, do we really know for sure that the Frobenius versions are really strictly stronger? =E2=80=93p. --=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. --000000000000c6341c0570df13df Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Thu, Jul 12, 2018 at 7:07 PM Valery Isaev <valery.isaev@gmail.com> wrote:
Hi Peter,

I've been thinking about such eliminators= lately too. It seems that they are derivable from ordinary eliminator for = most type-theoretic constructions as long as we have identity types and sig= ma types.

Thankyou =E2=80=94 v= ery nice observation, and (at least to me) quite surprising!
=C2= =A0
I mean a stro= ng version of Id:

Side note: th= is is I think more widely known as the Paulin-Mohring or one-sided eliminat= or for Id-types; the HoTT book calls it based path-induction.
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 t= his is to take any non right proper model category (e.g. the model structur= e 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.

Are you sure this is true= ? It seems that we can interpret the strong version of J even in non right = proper model categories. Then the argument I gave above shows that the Frob= enius version is also definable.
<= br>
Ah, yes =E2=80=94 there was a mistake in the argument I had i= n mind.=C2=A0 In that case, do we really know for sure that the Frobenius v= ersions are really strictly stronger?

=E2=80=93p.<= /div>


--
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.
--000000000000c6341c0570df13df--