From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCB43TOGRAKBB75VZDOAKGQEV2U6RLA@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-wm0-x23a.google.com (mail-wm0-x23a.google.com [IPv6:2a00:1450:400c:c09::23a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 884a17e0 for ; Fri, 7 Sep 2018 06:30:24 +0000 (UTC) Received: by mail-wm0-x23a.google.com with SMTP id r14-v6sf8890260wmh.0 for ; Thu, 06 Sep 2018 23:30:24 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1536301823; cv=pass; d=google.com; s=arc-20160816; b=zYpr/9fVhforH3mA1Na6rfLEqVFfJ3+d/iqBVnZZbBh26eCvhEldYTTYgU64LggemT NXaVkcvQHTJbC0XA6hB5EOmg+pcz2X9vKZdAO4KQ3KwgjKtr0m1yoMgkvTU6wzjiqUXQ ooftGxKcusH9ZseC4daRp2wbUSRjzroFuNyOOVAdGDYx2HOL681htxmRb2DghW6fCE6q H1IPGUemxKjYglsnd5AXb3/jyFM+MCk0cDPi1P2W92ABEJaLKvzHlg66A9CI1hAX7Q1X X43T+tyyRwHox6S43x9y/zQgKgs0V5e7OMg97OgNIt5ZJI6ZUBNp47/FVoNW1WbO+vcO L8uw== 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:in-reply-to:mime-version :user-agent:date:message-id:references:to:from:subject:sender :dkim-signature:dkim-signature; bh=qqt888UYXZ7zl/47DaEmIKNwkCdXTUxmzS7gp3FDh3s=; b=yejjCnOmIHA5vM3YbLOB/+mqgkdWBmulz5BabzOjm11wvW1CK1fxGjgT4Wj10glptN NdAgiJm9/MDpSARNI7I0MQySA+qkNPnqnYnt4GhPOq6BILwgc5wxDvaTsnOU1DCNby+f zqHaD/Rq5RfNV89fofJSbCfmQdmhyRT5dLyqGcBA28UjCFJRZolcjsqUsZwo+pBapItp 3vMg8JG7X+pYa6Y61GQ5v/wi9x+ucsEUJhw9ft4ngVlAUAL2AMKtU2gN7xoRxHMC3l5j MEBsj0nYfHEQg94QU625/ZtSzREToXa3cg+qmHFQyJPPcZGbTSWqGkcHBNms5GYpzO7W UDCA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=X0UaiiFf; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::42e as permitted sender) smtp.mailfrom=nicolai.kraus@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:subject:from:to:references:message-id:date:user-agent :mime-version:in-reply-to:content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=qqt888UYXZ7zl/47DaEmIKNwkCdXTUxmzS7gp3FDh3s=; b=WILpgaOEanRc1XKm0lP4UzTVc8rPpQMAVES6YvEQTgqYDHvdBrZFBaBCpJpPC+WVi1 ZufyWXkqtsBzJxjD3ZLCbQEoHodMQaUx8yA5IqZ73YW+oOxur+mkEnGeZ6xzq2If/fNc Fnc4BNOy9IWjnL/oOHqiIsE0Yayqa4F6cVAOLFfomjkTqx2LgRhwtezwE+vj5vD+4JQx miTFPHZbde1JgvPx2ih2VJuqwY9uM7GtPhT0fGZnTSx7j0mPv7HfgbkGsfxU5g61LXyy A/kYcNvktErZ0qG1Fxvnmv9CdmZFMDF9I+sRZVDvzianNyVJBbqMeFVGqGT9/lr/vTEz Nl3A== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:from:to:references:message-id:date:user-agent:mime-version :in-reply-to:content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=qqt888UYXZ7zl/47DaEmIKNwkCdXTUxmzS7gp3FDh3s=; b=g+cGlB3qPRsyE+c+ZfP5zSwuZS0LLjw7vQ66zzyx4G+pCq/XueJza1zXr4swx0+4lx ciZEduQgkrdbF1cIW22eT7P4mK5Z6/QquI6zQ85txWQZuPQWbQt/5PjRzzNiX74o0iW6 4bPC9tBUqjncFwBC/JPKi6woPGjb8tjlUvJdXpRgjVfwsM/LuDzbNmCPJpE8JBGWeBSJ Aj2dbjP09FfvMvpLkjHdlB1sHPM3XE2sEYiPV4HVJpVASG5rPbRUkaZPRLkpyRe4Y+MT xat6SwdO6zyRxJM7l8NxpNmU1vM2RtGkHipxgN7Je4VoNaNtzCGA/3eIWztOc/lOcABE cSiw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:subject:from:to:references:message-id :date:user-agent:mime-version:in-reply-to: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=qqt888UYXZ7zl/47DaEmIKNwkCdXTUxmzS7gp3FDh3s=; b=RRNh8oNa2rWV1/wtSq0dNeHNxhZHabi1Jiur8UMd5VH9Oczj20G5jQfaxRLVT0iM3P 2rq+90+DUgXpQHejULvPq5ELpuQ6XC8z0SAMulUKZpj1mUNgq+EkWADOE3/v8UsAKkp+ 9fabzcljcKrCvr2QRwnqU2QdOhtyWCFCdfDpaiI8WjXYvlWDVWPsnBd+UkTtzq81vM/1 Sj+U3sjrRWodNdjVnYeqawYxN8pXT9v9g9pLFN2A4Iuv/SvYVFYCi4DQhgThfOuwjyY2 gPnVtVZaMEYgF/RYAbFS+lJHT6IYth5s55Gk6QzJaPjfknACrQeSmfRqCU7WQkHgGV/n eE4Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APzg51BKaUyk5aHeL+c29WEktda3yXw9KFYN1B3d6s1zGv7NsOJ40o4D 7f09KCANaIzI3Bc/nqtifxI= X-Google-Smtp-Source: ANB0VdZDf8AZNajHJBWdprpLTjLc3vju0ZOxYNVcBxIml+P4TkuXW+N9ccieZux/5mr5sGEgtNH1pw== X-Received: by 2002:adf:b70a:: with SMTP id l10-v6mr84132wre.1.1536301823338; Thu, 06 Sep 2018 23:30:23 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:adf:8265:: with SMTP id 92-v6ls2405112wrb.2.gmail; Thu, 06 Sep 2018 23:30:22 -0700 (PDT) X-Received: by 2002:a5d:52c1:: with SMTP id r1-v6mr512304wrv.0.1536301822831; Thu, 06 Sep 2018 23:30:22 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1536301822; cv=none; d=google.com; s=arc-20160816; b=JKITVHJ4OkGUfLjY4CN8VPuQ40N/b402G0GnS+5R8+gL4X5RwiIqubBiqqn7y2jo82 4MV1pSAeeB95oAo8rTMiyn5xXCnauZrE2Qn6n6endNFnGyAlbr3iu3m/Hn6nr2bLXaE0 oB+fyTdB3q6iziX7Q12be5L4KS+ay0zs6LPvIlPKEw1YHbA2h3t6uT6DXY/yTureYQ8c YtcPJkCCYE4M+fY2CPrc1o9I0NYB18sEsOKY/YM+AMmwvqnZ9C9An+riJHSFS9QTWlIO YrwaL/Ob6/bT3hmEdTzDrw3KyE0GYH1Zo5D/6uaZRyjn89yO1VNjKFqP5EU471afdbd5 9cPQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:in-reply-to:mime-version:user-agent:date :message-id:references:to:from:subject:dkim-signature; bh=/Z4MW9ez4KutFdUl4kpUyqU5Ij+AZqEVvfOVVxFjtRs=; b=tJlKo+pqL2mpLNE5zkPl/BBFArWhtra2JgcDBRZdEEquWZwpPiR/oj4FHYuSo2Wvz5 KekWUSkRgYoAqxbLbl7O4Y3HM5PFYAVKuUcpCAl4OgIyAFvjXc1JHP3A2Nz2IyHHz3yn jF5uPG71QX5oEQi8bsqSRUcFm9RRdyVIBBRRwpBCwwgD2FwN3BpqgbD0DPDv9qUki5MI cS4mPRMdc2hd+2WxuGsnASVDNvSys+iQl6ur+eN57QEguUAXi4MQirrJLnsSsrvskyND 0hCrkqSCCSI2ivrMOPoiSmLbclpKhNpOQSHwNUngQryLplLt/9XZG4OpM4udBYCdj4dH FT+g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=X0UaiiFf; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::42e as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wr1-x42e.google.com (mail-wr1-x42e.google.com. [2a00:1450:4864:20::42e]) by gmr-mx.google.com with ESMTPS id v18-v6si288254wmc.1.2018.09.06.23.30.22 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 06 Sep 2018 23:30:22 -0700 (PDT) Received-SPF: pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::42e as permitted sender) client-ip=2a00:1450:4864:20::42e; Received: by mail-wr1-x42e.google.com with SMTP id s14-v6so4759701wrw.6 for ; Thu, 06 Sep 2018 23:30:22 -0700 (PDT) X-Received: by 2002:a5d:488c:: with SMTP id g12-v6mr5091591wrq.0.1536301821991; Thu, 06 Sep 2018 23:30:21 -0700 (PDT) Received: from [192.168.0.2] (cpc86229-nott20-2-0-cust356.12-2.cable.virginm.net. [82.7.65.101]) by smtp.gmail.com with ESMTPSA id h73-v6sm18939468wma.11.2018.09.06.23.30.20 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 06 Sep 2018 23:30:20 -0700 (PDT) Subject: Re: [HoTT] Looking for a reference that HITs are a strict extension of HoTT From: Nicolai Kraus To: Jasper Hugunin , HomotopyTypeTheory@googlegroups.com References: <24a741c1-a100-22cc-ccc8-2defdfb3a08d@gmail.com> Message-ID: <6d798e22-3850-c667-6df2-c3ca1d11241d@gmail.com> Date: Fri, 7 Sep 2018 07:30:20 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.7.0 MIME-Version: 1.0 In-Reply-To: <24a741c1-a100-22cc-ccc8-2defdfb3a08d@gmail.com> Content-Type: multipart/alternative; boundary="------------B0CA73016ABB248BD557C828" Content-Language: en-US X-Original-Sender: nicolai.kraus@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=X0UaiiFf; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::42e as permitted sender) smtp.mailfrom=nicolai.kraus@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: , This is a multi-part message in MIME format. --------------B0CA73016ABB248BD557C828 Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable 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=20 > would work as well for the second step, but as you said, we don't know=20 > so far whether this can be shown in HoTT. Since we don't need an internal argument, it should be possible to use=20 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 > On 07/09/18 04:56, Jasper Hugunin wrote: >> Hello all, >> >> Many ways of doing HoTT (Coq=C2=A0+ Univalence Axiom, Cubical Type Theor= y)=20 >> make sense without including support for defining Higher Inductive=20 >> Types. The possibility of defining small, closed types which are not=20 >> hsets (like the circle) or have infinite h-level (like the 2-sphere,=20 >> conjectured?) makes constructing HITs from other types seem=20 >> difficult, since all the type formers except universes preserve h-level. >> >> Does anyone know a proof that it is impossible to construct some HITs=20 >> from basic type formers (say 0, 1, 2, Sigma, Pi, W, and a hierarchy=20 >> of univalent universes U_n), up to equivalence? >> >> - Jasper Hugunin >> >> --=20 >> You received this message because you are subscribed to the Google=20 >> Groups "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it,=20 >> send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com=20 >> . >> For more options, visit https://groups.google.com/d/optout. > --=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. --------------B0CA73016ABB248BD557C828 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Small addition to my first remark:

On 07/09/18 07:14, Nicolai Kraus wrote:<= br>
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/#!t= opic/homotopytypetheory/imPb56IqxOI
But this is only for CCHM type theory.
Nicolai

On 07/09/18 04:56, Jasper Hugunin wrote:
Hello all,

Many ways of doing HoTT (Coq=C2=A0+ Univalence Axiom, Cubica= l Type Theory) make sense without including support for defining Higher Inductive Types. The possibility of defining small, closed types which are not hsets (like the circle) or have infinite h-level (like the 2-sphere, conjectured?) makes constructing HITs from other types seem difficult, since all the type formers except universes preserve h-level.

Does anyone know a proof that it is impossible to construct some HITs from basic type formers (say 0, 1, 2, Sigma, Pi, W, and a hierarchy of univalent universes U_n), up to equivalence?

- Jasper Hugunin

--
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@googlegro= ups.com.
For more options, visit https://groups.google.com/d/optout.<= br>


--
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.
--------------B0CA73016ABB248BD557C828--