From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.2 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,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.2 Received: from mail-ot1-x33e.google.com (mail-ot1-x33e.google.com [IPv6:2607:f8b0:4864:20::33e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id eca0ed4c for ; Fri, 11 Jan 2019 11:49:09 +0000 (UTC) Received: by mail-ot1-x33e.google.com with SMTP id n22sf5892899otq.8 for ; Fri, 11 Jan 2019 03:49:09 -0800 (PST) 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=d9INuVymYjeppW7r2mEhPq6Vz0CElra5dLEjrQQw+hs=; b=ij934V9lBHJlf8Ok5wI/wtPE7X/kvqTeZr1T1EyXZylwgGdfrnprvqWkPsitrYkOWo v7HKJ+G2kznsIhWIvnyhxC9adgqqq/lzrtPLuomMzvI+mGFIqQ3P17r5LqzpPCj8V50P GUHti/HB8XWIbXDOKBPySqzRRATGfmJVCdL3aaOyTe/i+v76MJS7n3pijVHeZ3Ry/7X3 TaOFM6Q1bWZek42eLvLl1PMeXyOeVrG/5lIJGJ6qWhLnh07Ow16nBCPYjtnPqVBzGSgF doqvbcQv7guIK2UrsHfFgZL2tNADN9XYVpbN2x0F0+ziQbvVi955uuYvyWpqJwK340U/ cldQ== 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=d9INuVymYjeppW7r2mEhPq6Vz0CElra5dLEjrQQw+hs=; b=MLG27G8l8ijhSBPXKVIya37SNVsujhd4w4QUa7/leZKboSxOD2woSFS/pvC5PtkB58 E8I3w6vWR2SAQkzp0UtlqzWqLrPN1g0u14ow0MV2sPaHZGj5Oz3IBl8UrnSgJAULbjcp fwbi90/rTAd856WJmGyStYaqIup9qePQqqfY97ixL6zLqBr0ElulXIe344Hs4y0EnlqD nvdP9aeJEisNMfvlZNbTjXXQ4i1z4FVxB14gE/bvt3FqdzsLcFEwXQxgqQSg70gerp+y y/fEuf0dN5drtsfM1ZBTOD0ezQ65MSHBEkxJDEU4TFHCXxsnJ8O2AXEg2CnFg1GJpGPy IUdQ== 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=d9INuVymYjeppW7r2mEhPq6Vz0CElra5dLEjrQQw+hs=; b=fLjRnADMX9YT8NzGsDMsQcHO+ZMTnFOEALCZG0p79lXaHPw5qWyE5pjAzRz4GLNJR4 95m2zwknF/t3BLUL31ntQ4EQ60wUWoyLgz/x/pTcqzPxN85UOnLM6a7PhKbEtYZa/1Rg hU7q/7WPdu5uWtRUxnyGL6uN+fm7QRbxmZe6LH78e7Z72/5nqHCMAYBM9bLAPi0wKC+E 2VTzyhM12+oFJAnewM5gugM8BVgvqIWApXhXE2w0xt0FQpXrKM16lwKmqIpaqSyh3r81 YShJ6p9A1Rcs5vb1b1z2YQSRu+8OL1T6jdPu3izGnA+2fbWD1zcAlmV7toG2Ph6wFMsG /t0g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukdwIBC3W4ju0EigP0De+Z4WOK/QtY+sw9A5xlc5+g/k7PxgTrLT gkJy56fv4lnGBTeOoLpwU3s= X-Google-Smtp-Source: ALg8bN5VGKNvWUFTIp6+gBrLALvqZ9ewHeA8DZMcTZ2pgi9F2KSB0Gded9BibsUzbUceg1NfeobxIw== X-Received: by 2002:aca:cc0f:: with SMTP id c15mr85762oig.3.1547207347557; Fri, 11 Jan 2019 03:49:07 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a54:4605:: with SMTP id p5ls6002354oip.0.gmail; Fri, 11 Jan 2019 03:49:07 -0800 (PST) X-Received: by 2002:aca:5884:: with SMTP id m126mr85974oib.4.1547207346890; Fri, 11 Jan 2019 03:49:06 -0800 (PST) Date: Fri, 11 Jan 2019 03:49:06 -0800 (PST) From: Brian Sanderson To: Homotopy Type Theory Message-Id: In-Reply-To: References: Subject: Re: [HoTT] Homotopy type of simply connected spaces. MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_766_170169950.1547207346314" X-Original-Sender: brianjsanderson@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_766_170169950.1547207346314 Content-Type: multipart/alternative; boundary="----=_Part_767_1854672870.1547207346315" ------=_Part_767_1854672870.1547207346315 Content-Type: text/plain; charset="UTF-8" Thanks for the references. So am I allowed to say a type is simply connected if any two paths are equal, or is that a meta statement which has no meaning within type theory. On Thursday, 10 January 2019 21:12:13 UTC, Michael Shulman wrote: > > Yes, you have to truncate the equality. See section 7.5 of the HoTT > Book, and also Exercise 7.6. > > On Thu, Jan 10, 2019 at 12:36 PM Brian Sanderson > > wrote: > > > > The type of a simply connected space would seem to make it just a set as > any two paths with the same endpoints would be homotopic. I see that there > would not be a continuous function from the space of pairs of paths to > homotopies between them. What would the type of a simply connected space > look like? Can I say in type theory any two equalities are equal without > having a function? > > > > -- > > 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. > -- 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_767_1854672870.1547207346315 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Thanks for the references. So am I allowed to say a type i= s simply connected if any two paths are equal, or is that a meta statement = which has no meaning within type theory.

On Thursday, 10 January 201= 9 21:12:13 UTC, Michael Shulman wrote:
Yes, you have to truncate the equality. =C2=A0See section 7.5 of t= he HoTT
Book, and also Exercise 7.6.

On Thu, Jan 10, 2019 at 12:36 PM Brian Sanderson
<brianjs...@gmail.com> wrote:
>
> The type of a simply connected space would seem to make it just a = set as any two paths with the same endpoints would be homotopic. I see that= there would not be a continuous function from the space of pairs of paths = to homotopies between them. What would the type of a simply connected space= look like? Can I say in type theory any two equalities are equal without h= aving a function?
>
> --
> 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.go= ogle.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.
------=_Part_767_1854672870.1547207346315-- ------=_Part_766_170169950.1547207346314--