From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCB43TOGRAKBBRNOZDOAKGQEHDFOXYQ@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-ed1-x53a.google.com (mail-ed1-x53a.google.com [IPv6:2a00:1450:4864:20::53a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id a5ce254d for ; Fri, 7 Sep 2018 06:14:30 +0000 (UTC) Received: by mail-ed1-x53a.google.com with SMTP id h4-v6sf4516179ede.5 for ; Thu, 06 Sep 2018 23:14:30 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1536300869; cv=pass; d=google.com; s=arc-20160816; b=F9vvIC1ljSuLrEOwsKrWQhil6iEUQDI8LUoKmAQ6KGmxP3Tk8drFaB6i90Q/V/lymB 2juSrtvDgYfx92EztkOXyh2ALwYERn0cSZzuzDRoBX0+3QpMPOqTiQwqfH7GPIjQTCUU zjpDU9zC2lFvGGPDACqjJSaU7piGlgPvDUuiB8W5dzdX5gQJFGQjcBHjPaoLuB47Wbcn 2skhsCYbLXB9E2PeMfPSkUmJLTlJQY9oeXYmv+SDfcQqMkCER33DGeJ2Eyn2tKWgcP8I cXX7X3p3d04tnPpU3tiUM/duUlJeVqok8OWNpLEsShJKkXPIz4648Jue5GVCeUnH3rVZ MQ7A== 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:from:references:to:subject:sender :dkim-signature:dkim-signature; bh=uTD5+la+94UQ1348MOQZXUiSG4dGkeb50DNsUQfqT5o=; b=k4C0El1Rudlc7tAEcGmkOpzxJQ4ikuEzo+n4nCUJix+fYY/ToIdFax+05306U9GKIV iLeEECmUTu3ef50+afLv8TLJTnyRdMH+Ugqd1Q/uUPDNn9a7Kd8EL0LzlFunOAtgCDxg lCBN7EzcjSipO6GFTFMXYeBd5vtvM8jyVRP9SWGFrFBoC7dKVIJ+Q8huyJwlldRJ2zZd jW5P3A5K/q6d1kfPIq+jmqDihg4rqiVqizO7aulxQx74pHE6/4Uy/k+PasIXg0q19jFg Hb4fmf4sDi/MNKiewP9VAfFhp31GUZ3KIuGm/mDDmx/ptGNXGRNZiIwG0nljKEfxx5FE NIdQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=lp1VN4ff; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:400c:c09::234 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:to:references:from: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=uTD5+la+94UQ1348MOQZXUiSG4dGkeb50DNsUQfqT5o=; b=VVHYvx63UYXFFykZBLpF4TFCLEW8XYbF7VnWj0SMutURh6XtNszVlFy9wwbHBPz0i2 Gr3ctn+haeG50+TAtmLqIqP5Di37NwNkn1s5I2iWPsHR9AZW5Lk1/F9DJ1Xb4sGCOPA/ TI+fKGbK7IWnipavaFzvx1S9NWl8KLczCsUaKhVuinIFtsOdE+IyAzLxPuKdbub3jR6w sCvxqDjhbx6kmq/e26hWs1VW10hgjM2Ef7pE2D25essHH1TGLdXPCXlAqzI9ggXwhtTU g9BW6QOjGJuYEfoNQ/7QqqEVKZlUuiGHpdayELdMqunf74kUG/okr8AeTvWh4H7Tfmgl FnHg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:references:from: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=uTD5+la+94UQ1348MOQZXUiSG4dGkeb50DNsUQfqT5o=; b=LAeK9jq9JgGi6B7cBK/lHDTdLqviF2uUBaAFZ/cUncE0S5AuqSsU7F8HGtC8uPVOpI P1XYAQTMKXfhRTngXnwqUffp3At+fRVa+kodpA0ddTgVt52mqU72oujdMkKX8GfueA13 1imb8h2XuUoUe9MohSZ/yXb67zeronw0EtI8ms0KK0sC2gqoGl2JgNZF9QY+DTSOVI/B I8VylxigLhREWktTugVjA49Wq+tu+9v63W3ZidsPz5u27Jkbsw/S3X5b9POAZIEDWjOv IKYJVJ7PvH+xY3uyA5G74OZRnRrIoHXLTYHzucOioF16JTsC4TFmyQenJVnPwtpbNneV vmzg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:subject:to:references:from: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=uTD5+la+94UQ1348MOQZXUiSG4dGkeb50DNsUQfqT5o=; b=ugwCPl2WiI7rbi3Et1ecN3uBYlwpkpxez2becqnyngmUpAqgCRAcV9hlyOajGrMCLG ZuGO20u4clGDPbwHUETW6EhJM0nPEyHPzOT0HTVbAFgvUhi32UWvtff0lkxAp55OLaAQ 6SDKOH+iOgLQ5Umv5duuv5K7JePDDyoLXFXT51RjXNzkTywjAvTSbbTo1AfluwMXdhhm HapuTS+DYYrqj2uaiCXt3kUhzM5+xva/o+vba52aRcFVAthEZipD34jHaBmO9iFQRZ9q 1Ix54MKYSHt7hhP93vmoF7rGOO5K6esLoUld1W5sLDtrNkFG9Rio2emhAUy+UGM9XnPY E2mg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APzg51C/Eij+H/aG+8BIz8X9DIqgIKOu0chuSyKqq+h8xf7eBqBgEIqc 8O1a+9P2XwyBsJWTkUB6vG0= X-Google-Smtp-Source: ANB0VdY+Q03k7VYhx0ZiL3H8ME38aX5bsQmVshvz4yxgBZahoaJ5L/y4koyy03SCguVe1q3x9ASUAQ== X-Received: by 2002:a50:e807:: with SMTP id e7-v6mr37407edn.7.1536300869864; Thu, 06 Sep 2018 23:14:29 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:c8c9:: with SMTP id k9-v6ls3451410edh.1.gmail; Thu, 06 Sep 2018 23:14:29 -0700 (PDT) X-Received: by 2002:aa7:c415:: with SMTP id j21-v6mr1472863edq.3.1536300868982; Thu, 06 Sep 2018 23:14:28 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1536300868; cv=none; d=google.com; s=arc-20160816; b=qNVQ18CY/lIcaelFn8kzXrck3536TVf7bTs4KYmXswwxFWDiGgBO7Am9f/A494FsJ7 2K045qLA/3rtksSVLyA+4d3+X5t4X/S0hUpELZtgI2kXueobd/MrWJe4/Gl/KAKkiV35 PsqmpfXDW8XELh7gO4i6MXOg7dhFwfVB6DwLOsi3Sy4IMtc/9lodkQgYI9qyIJomhl0M KSUOKgkD/dc5bxJH1+6s/0YhT4NfbAw2LJtxp+aBvyqbd42L2BHdrT4e+6//rBs1aJAE 3ICKr1ym5U6H0X1KCEq4ZARKc/iqAVBCpGr35XQAsO5XgO3zuktETk6ceqMRGkpqUrhm b89A== 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:from:references:to:subject:dkim-signature; bh=xIo9oljajzMkzyoetbbuasg6VLQtwGtmwlMdMwOAeBg=; b=GOWerwk+xBCAnwN+vxXnf/JhYOmzxbL267CzHX6nvOeGkeceVEKNZ95nAQ8fthwjeh 3gK9ZB8zjdgyuirWJ+NNY0Fc19HDB5CwXHj/cJkmm4Bo2gXVeJYgcUX09ct4xy4lTiOl fvIyxxLiVpFRoXx5iuX95YvHoICoU/B0a4ukx9oSV5yPpm/AMIlL63JGG7Okex0SnQwp 7eB9pecvgxCV5q0criBkbeR6ULC9ATaAQC2nSw4NXFHeZxid5W2iYR864OZUiHqjjWSp Ax2Nf1AKMTlTi43I04sQC9eU5Iz8TEiGOQYG5wXAiSycIrk8JvKAyfm/dIu8j/3MqmxN rKlg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=lp1VN4ff; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:400c:c09::234 as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wm0-x234.google.com (mail-wm0-x234.google.com. [2a00:1450:400c:c09::234]) by gmr-mx.google.com with ESMTPS id y4-v6si231467edp.2.2018.09.06.23.14.28 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 06 Sep 2018 23:14:28 -0700 (PDT) Received-SPF: pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:400c:c09::234 as permitted sender) client-ip=2a00:1450:400c:c09::234; Received: by mail-wm0-x234.google.com with SMTP id j192-v6so13449053wmj.1 for ; Thu, 06 Sep 2018 23:14:28 -0700 (PDT) X-Received: by 2002:a1c:a941:: with SMTP id s62-v6mr4456835wme.76.1536300868202; Thu, 06 Sep 2018 23:14:28 -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 d22-v6sm14092916wra.80.2018.09.06.23.14.27 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 06 Sep 2018 23:14:27 -0700 (PDT) Subject: Re: [HoTT] Looking for a reference that HITs are a strict extension of HoTT To: Jasper Hugunin , HomotopyTypeTheory@googlegroups.com References: From: Nicolai Kraus Message-ID: <24a741c1-a100-22cc-ccc8-2defdfb3a08d@gmail.com> Date: Fri, 7 Sep 2018 07:14:26 +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: Content-Type: multipart/alternative; boundary="------------89510D1DAE2724D82082065F" 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=lp1VN4ff; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:400c:c09::234 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. --------------89510D1DAE2724D82082065F Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable Hi Jasper, here's an argument: Without HITs, it's consistent to assume that every=20 type in U_n is an n-type (since, as you said, all type formers preserve=20 h-level). But with HIT's, consider the type =C2=A0 Sigma (k: Nat), S^k. This is not a k-type for any k since the k-th fundamental group is=20 nontrivial if you choose the base point correctly=C2=A0 (see Licata-Bruneri= e=20 CPP 2013). 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. 2. For more general universe hierarchies than the one you use, for=20 example indexed over omega+1 or indexed over any poset of arbitrary=20 height, my argument won't work; I can't think of a proof for that=20 situation off the top of my head. Nicolai On 07/09/18 04:56, Jasper Hugunin wrote: > Hello all, > > Many ways of doing HoTT (Coq=C2=A0+ Univalence Axiom, Cubical Type Theory= )=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 difficult,=20 > 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 of=20 > 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, send=20 > 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. --------------89510D1DAE2724D82082065F Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi Jasper,

here's an argument: Without HITs, it's consistent to assume that every type in U_n is an n-type (since, as you said, all type formers preserve h-level). But with HIT's, consider the type
=C2=A0 Sigma (k: Nat), S^k.
This is not a k-type for any k since the k-th fundamental group is nontrivial if you choose the base point correctly=C2=A0 (see Licata-Brunerie CPP 2013).

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.
2. For more general universe hierarchies than the one you use, for example indexed over omega+1 or indexed over any poset of arbitrary height, my argument won't work; I can't think of a proof for that situation off the top of my head.

Nicolai


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

Many ways of doing HoTT (Coq=C2=A0+ Univalence Axiom, Cubical 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@googlegroup= s.com.
For more options, visit https://groups.google.com/d/optout.

--
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.
--------------89510D1DAE2724D82082065F--