From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCB43TOGRAKBBLFGZHOAKGQECCXPWPA@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, 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-x23a.google.com (mail-oi0-x23a.google.com [IPv6:2607:f8b0:4003:c06::23a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 39f5bf05 for ; Fri, 7 Sep 2018 10:30:05 +0000 (UTC) Received: by mail-oi0-x23a.google.com with SMTP id q130-v6sf16149281oic.22 for ; Fri, 07 Sep 2018 03:30:05 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=GAnkRdQEkTW60z78xbwBrJDn10zv2jDNCAISwfDH3Mo=; b=SmEt9GY12y6MA3z8zNJqhhzcUuQmEWbiRYmKQcVDqedaKus0hsnD+ww2au0skhp/lo 9ZlQYN3H0D3YkNewyt0aKr3hH9zh/d0QhdvURysQtUpPxu8YQ2D8ogqp5Gx8gpaSIBha E8QFG3E8HrbSvXxMcsZ+9ALxw8TGORrw90dD0N6zyrjYMGQCswpVryzltQpVsQmIDRjg DzHo7TPTaoz6yQnJJSSpyWMo5b9HAEr8Usyb6vIe8KBbPFzD7E7GDJrD5ZoT0vVUyx+V CijRrbj1zO6YPkak4XcqECnnEYRSuzN/epbhT9hWsJV9NlrkfkyOcKlFoj6RGRZWS+Wv xa2w== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=GAnkRdQEkTW60z78xbwBrJDn10zv2jDNCAISwfDH3Mo=; b=V/S0Dd0HTwTJSxr0h4AyeUsH0wb8sQRWs9Ztgvc2g+kceYJ2nTf1r4LTyzcsPjf5Q6 lF+AcFQ0hm5uySdUJgrgRTcfBi5PnC6UBsoMM78jtrz/ZtKq5qAzVz+Az+XnQPMojIER nwWLAcYyZ8dJfP82IF+WsRj5qmAZxgXqzyKkx8D6Wp6OmKupiq4nfCVr37HfgloHcKb9 GzL+79IfcrDnLkRyO3fp28kojw8QvX+MLc9dDU/kgQS6MD8Qpn18V2GMlee6BOezyakt Y8qq3FZUJsP3ZVnlyEnVUJGGFLRuzf17bSPWBXhTOdbIjr7yLrfI2b4FHqQbWg12wi8j Zg9Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=GAnkRdQEkTW60z78xbwBrJDn10zv2jDNCAISwfDH3Mo=; b=XKb3/7gSRqpqBp4wGUR1R9ax+2QV99yP4WD757u2DoaI7Kp59yMddxh4oeq581q5xd DsOfWlmrD3bV7r4gdZKKuADazM6d8WvOblbA6LzSPYvhmq8PdbGb84V8m6DMzKO/0AEP Nc8oX6TjYJKxdjaYST9ZvJ2T4Bz95pp902BikFV2r7JpOXK/mtkLOvlDD0698pSnLalJ dVKEOmbDaQwJrZ8xJFWVl0oeyUlp+eBVGKg9w3VgQzs7TNmY1nVwPU8rnpQ2LczJIgNa Nd6jIphsXynI+kiH7vsAl/rzykhAB+pPiAAh6SdcA9TntPvWjoxwhSYlAmP7VYKH1skb gU+w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APzg51A0KtjO6+nXa2Gdbl+WBc55g3f91QOvUfmMuJTGHqoeKnhj/FW7 EIObhVCsqF/OwOlqoizQYxY= X-Google-Smtp-Source: ANB0VdZ48uNtylkhgMEeOr0uhfXh/ohflEeFv+TB7XOdEsSkzZD5415M9UOpyACiynPPp0gZz2jfww== X-Received: by 2002:aca:c68d:: with SMTP id w135-v6mr166487oif.4.1536316204460; Fri, 07 Sep 2018 03:30:04 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:1803:: with SMTP id h3-v6ls8139416oih.13.gmail; Fri, 07 Sep 2018 03:30:04 -0700 (PDT) X-Received: by 2002:aca:ec87:: with SMTP id k129-v6mr163162oih.2.1536316203048; Fri, 07 Sep 2018 03:30:03 -0700 (PDT) Date: Fri, 7 Sep 2018 03:30:02 -0700 (PDT) From: Nicolai Kraus To: Homotopy Type Theory Message-Id: <7d8ffaa2-a7c0-43b1-82c3-b1328672c558@googlegroups.com> In-Reply-To: <6d798e22-3850-c667-6df2-c3ca1d11241d@gmail.com> References: <24a741c1-a100-22cc-ccc8-2defdfb3a08d@gmail.com> <6d798e22-3850-c667-6df2-c3ca1d11241d@gmail.com> Subject: Re: [HoTT] Looking for a reference that HITs are a strict extension of HoTT MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_146_342830863.1536316202464" X-Original-Sender: nicolai.kraus@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: , ------=_Part_146_342830863.1536316202464 Content-Type: multipart/alternative; boundary="----=_Part_147_917727794.1536316202465" ------=_Part_147_917727794.1536316202465 Content-Type: text/plain; charset="UTF-8" The addition from my second email didn't make sense, sorry. The first email with the easy argument should be correct. Nicolai On Friday, September 7, 2018 at 7:30:23 AM UTC+1, Nicolai Kraus wrote: > > Small addition to my first remark: > > On 07/09/18 07:14, Nicolai Kraus wrote: > > Remarks: 1. If we knew that S^2 is not a k-type for any k, then this would > work as well for the second step, but as you said, we don't know so far > whether this can be shown in HoTT. > > > Since we don't need an internal argument, it should be possible to use S^2 > together with Thierry's result in Christian's post > https://groups.google.com/forum/#!topic/homotopytypetheory/imPb56IqxOI > But this is only for CCHM type theory. > Nicolai > -- 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. ------=_Part_147_917727794.1536316202465 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
The addition from my second email didn't make sense, s= orry. The first email with the easy argument should be correct.
Nicolai= =C2=A0

On Friday, September 7, 2018 at 7:30:23 AM UTC+1, Nicolai Kra= us wrote:
=20 =20 =20
Small addition to my first remark:

On 07/09/18 07:14, Nicolai Kraus wrote:
=20 Remarks: 1. If we knew that S^2 is not a k-type for any k, then this would work as well for the second step, but as you said, we don't know so far whether this can be shown in HoTT.

Since we don't need an internal argument, it should be possible to use S^2 together with Thierry's result in Christian's post
https://groups.go= ogle.com/forum/#!topic/homotopytypetheory/imPb56IqxOI
But this is only for CCHM type theory.
Nicolai

--
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.
------=_Part_147_917727794.1536316202465-- ------=_Part_146_342830863.1536316202464--