From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDGJPXM2QALBB2HNY7OAKGQEILPPSTA@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, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI,T_DKIMWL_WL_MED autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-qk1-x73a.google.com (mail-qk1-x73a.google.com [IPv6:2607:f8b0:4864:20::73a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id d2fdc3e3 for ; Fri, 7 Sep 2018 03:56:25 +0000 (UTC) Received: by mail-qk1-x73a.google.com with SMTP id u129-v6sf9635948qkf.15 for ; Thu, 06 Sep 2018 20:56:25 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1536292584; cv=pass; d=google.com; s=arc-20160816; b=Rn5MWqtdnqZHBPqgbAFwKI0yhGdvJl6hw2irS6+kKfugWCm839XAbAdxLUiQ1zmq1j bAJTXpV+JU78eyB8/zpaBvj5R50bnQa4vS7Lhl/PpDpg1GqtCOhIcrDfnTxpfuiA+CqJ KNDxdmTIg8Rb5KBnKO/XblNItEErtWVauHlFkmhz9kB5RnII6ax0nPcvNdz8KIXNFwdq lslharGm1zFfhoNQsrwWYSO/IEi3knW8ycKOxwBdonv7ry3zM4GiX534ID7cEbjJeEKC X4er0kDaoedOX6RYTKF6+d5mjmQgbDRITQRhQ8etP3iHpnA8UVz4dICtfoT+gMVV5fUY VSwg== 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:to:subject:message-id:date:from :mime-version:sender:dkim-signature; bh=MZjy+HBug4uVTozZVVHDN2EeImrUDxVyZKhdXB/GSs4=; b=Jqbq1OqN7sGxVBlhJqmFVqzXNBU6J85yBkqnsy1i44Y/fVI9FmVIGSa0CENjn0RZ7F on4W7NGwQ4H7VmBj3DEgkXHkbX3EP50QYyLaWwbNmtwvdr02DWv2X/zxxsja6HKx7UN3 82At036fXssn/YGptxdWenSy0UL0gjQo2e64mvhgiQG6d3lnIh6zMoBssB2TWcC1iVZ5 +lbx8tRJpap6wcwOG0jRrRV12qKpX1ovWrH/ukx6LLUBcup4Yesfd2DawU0fbZiBLNP4 g8WX62Qbv13vIeHyn/OrZ70IqJOgM6aA4Bv/SEHTz5lBB2YZv7TsN0SVM2nAd1056dJS 4RRw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@cs.washington.edu header.s=goo201206 header.b=KQR9WOHp; spf=neutral (google.com: 2607:f8b0:4003:c06::22b is neither permitted nor denied by best guess record for domain of jasperh@cs.washington.edu) smtp.mailfrom=jasperh@cs.washington.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=MZjy+HBug4uVTozZVVHDN2EeImrUDxVyZKhdXB/GSs4=; b=IY0SK+57qk4gQI36YNdgPbWNm0b0sQX4YTp/ycy1I/BhP3mQn52NDpZFMbH1Y5zULI cukr4wE+bQDGQEPLv0jR8EG8iGmn9bl84yfeKnlqG+CbgaGRpoA9HCY4tTZRWy5wQ0p2 WLAXKtfatcb+91EuybSOn2oNCYOh575quCiVMApdV3nw3mxdpXNimOKLIdBgAblz612P sp8g6mhofTfr7KY4bJ6aNlFpSDPbFvvYbloQgLo0QyEPinp+SHsXwKsss6kpo8T8WZbd BYfbudaKG3Rn7hXdfqptdpl3/HSg0w5bl+892coWdhMnH4zFnLcvXDbpY1F/EjdQ7ekV kzjg== 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:from:date:message-id:subject :to: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=MZjy+HBug4uVTozZVVHDN2EeImrUDxVyZKhdXB/GSs4=; b=q1J0FEYZg5rXV8rxpGOyS8mP49+Xsx0xBLcqwoW8n7XpHUMBbDC5iy9oVJ7ab3fOtV wJc2nmX4CA1BsaUd+lCi4UBhfIDN3SPLWpekaUNUEhB+nUpfOcjj9nmkNkEBzsMybTSk rcnV6dkVuIgmQrI9sE31WU//yzwgeGWI2bfdVTFoW1uopzp8I02bZ7JCDq7jufc6j/F+ l/DjpmIxFDak7Q9eAwlMAKWpGGtzxiFdC5bHXtIG1LVoy33txTIwI20l4zqb5UbzOCD8 ngfloSRnRH6F7oJH+OFznzCm9ylAJBt8bWvOKOgP+TUauCRr+K+XDeiDPfaBafMEaGRY 88Ng== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APzg51D3Q99lpDt11uxSQNjZymvkmlNn2ALw8CeTBxhGZO8LF/y/bxFS 2a0HNY2oIPv2Sej5x1c8P5U= X-Google-Smtp-Source: ANB0VdadYbX7L9n3qDGDm/P+PEl3QtN2TFUV9AFJ+L/wFvKHBagPD6Rkx55wQcKwMiDsg5JubuDrQQ== X-Received: by 2002:a37:1f45:: with SMTP id f66-v6mr65505qkf.1.1536292584490; Thu, 06 Sep 2018 20:56:24 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:643:: with SMTP id e3-v6ls2859814qth.2.gmail; Thu, 06 Sep 2018 20:56:24 -0700 (PDT) X-Received: by 2002:ac8:405:: with SMTP id v5-v6mr2093743qtg.52.1536292584119; Thu, 06 Sep 2018 20:56:24 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1536292584; cv=none; d=google.com; s=arc-20160816; b=m3sKlHFYlCyV73tKnmw05ZTm0lQrU/bp/QsKlpA7JmxHTTEzSQI++Tu20v+E5JtVxF TQHYkUX7A0UmSk9ASOqvAUb7TW+qFU6quQEPrAZROemkPaJJKQuD4IhK+mbQHbceNEYB HrENRG0YP0ll3hqEkajO8bWZK4w5FZbHpqHfOhD0bsa5Nl6mzhO/+60bw5hmKSO8tLQp 6UutXECufo+GHiGLnpiewGidEpP3kZS0bSqk8upVq0lRrS/OhQ8eJdo7yivPTcPJ/axs oofFLMN7kwlszAobls8ulLxReNI72AMPX6F5GQF6HtzPiERkHf9sU5P6xTPoF0YC03VG yJoA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=PrCqn6gijCAvy7Jm7rFzXVhlth0WmUl9eoHeY3baH78=; b=Dd0i7/+bCHOZSCMBxcfkay/GsVAjVHmKnnIu46OsXVNFjXKVPMu9LDlyTUJJ7I0wFJ KeVsb9lLOQoGwvf7BnZAjFZX7Yxru0VYX1UEhkqYewxX5m1fSEDuaMBNH6byQeKNKeEV oEPrsYIPVcgyJvaTTEPfubb8enjichXUogVdmh/C1waKKVrLzCxGSE6vmLrb6ctbLd3v cgjlvJNbZP6UlQmKRZKuuZlUso/kQsF/k5C3g5puWlqZS5Go6Qcrcz8Mjh5dMNaob43D WAX8qRFD3DNUYYBXn+xm3BDhYb1y+8R5LQsoYaPsIz9eGuh2Ud1Sh3u9dtC7RQfG9plR k8Dw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@cs.washington.edu header.s=goo201206 header.b=KQR9WOHp; spf=neutral (google.com: 2607:f8b0:4003:c06::22b is neither permitted nor denied by best guess record for domain of jasperh@cs.washington.edu) smtp.mailfrom=jasperh@cs.washington.edu Received: from mail-oi0-x22b.google.com (mail-oi0-x22b.google.com. [2607:f8b0:4003:c06::22b]) by gmr-mx.google.com with ESMTPS id a76-v6si322236qkb.2.2018.09.06.20.56.23 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 06 Sep 2018 20:56:23 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4003:c06::22b is neither permitted nor denied by best guess record for domain of jasperh@cs.washington.edu) client-ip=2607:f8b0:4003:c06::22b; Received: by mail-oi0-x22b.google.com with SMTP id y207-v6so24749806oie.13 for ; Thu, 06 Sep 2018 20:56:23 -0700 (PDT) X-Received: by 2002:aca:758c:: with SMTP id q134-v6mr6240723oic.334.1536292582973; Thu, 06 Sep 2018 20:56:22 -0700 (PDT) MIME-Version: 1.0 From: Jasper Hugunin Date: Thu, 6 Sep 2018 20:56:11 -0700 Message-ID: Subject: [HoTT] Looking for a reference that HITs are a strict extension of HoTT To: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="000000000000adfb3c05753ffdcf" X-Original-Sender: jasperh@cs.washington.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@cs.washington.edu header.s=goo201206 header.b=KQR9WOHp; spf=neutral (google.com: 2607:f8b0:4003:c06::22b is neither permitted nor denied by best guess record for domain of jasperh@cs.washington.edu) smtp.mailfrom=jasperh@cs.washington.edu 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: , --000000000000adfb3c05753ffdcf Content-Type: text/plain; charset="UTF-8" Hello all, Many ways of doing HoTT (Coq + 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@googlegroups.com. For more options, visit https://groups.google.com/d/optout. --000000000000adfb3c05753ffdcf Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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 s= mall, 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 impo= ssible 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 &= 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.
--000000000000adfb3c05753ffdcf--