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-qt1-x83a.google.com (mail-qt1-x83a.google.com [IPv6:2607:f8b0:4864:20::83a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 4a8532a4 for ; Fri, 11 Jan 2019 12:02:12 +0000 (UTC) Received: by mail-qt1-x83a.google.com with SMTP id d31sf16428574qtc.4 for ; Fri, 11 Jan 2019 04:02:12 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1547208131; cv=pass; d=google.com; s=arc-20160816; b=Hx2Iovdba1XryOy2TkG+JMYnA0Ef7dnn58R+XYtdfjpksM5dvFlKS8UoxfQ4rJYUoJ 5EVUOkSKu4zf34vcThfcaLuiEN5LBmB35XPpv+eWud/2qM9gEMaO0zJGtYVNGEOsR0W5 OdGoQIVeehg7vHzIiw4K9IvbqktYrYbLnETZmdlzItWMNPv1NRQIQOsNIiDWrNLCKecu ufq3xmF0VTxBfDnS1CnE1TjsA/6gAXsqpOSFEXeJrnr9CvoEL8OTJmDtplxmd1qyAW2Q SYNRzawcZ6t4mzhoYVAVPqRnJxZHzp0e94tyinfTiwcgsvV0M+eLyjlm4iTWOmBki3LC ziEg== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=kFmmScvy7DIR56eBivBsgkjxxp0ZEDNow1L/x0B7RHk=; b=lUkgnNygBH1jPYVXvbluxmxbVK77jJKpfnBahLTfDdC5kJbPS0aHkx3W7QEbU1kCnI Yg0znix4/0IIy9iKGHa45tSTXtfupY2Oa9qe9LOeFYEJq2dy0P4IgwjGP0uTye8HK2jc PQ4L1b0BOJ4wZCyzn0sKv8+IG4Com3cg0rMmAf8XXb2E6JKl8TF8WBSoJ9a8wZRO6OkM YkBVBFA9ZEWeUbpvBIQL0QvgukQYBFEq4ptBAHFwwmP7ESqnIyKbH5chP80+6njg65md YHi/V3PLHdQRMuYI3EV7JvcibxEgvkrep2PK2GhYFrrk+e8QKtZ7f5wTGuRNQXchXkaC TCaQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=u1Xl0hRS; spf=pass (google.com: domain of cory.m.knapp@gmail.com designates 2607:f8b0:4864:20::d2f as permitted sender) smtp.mailfrom=cory.m.knapp@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:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=kFmmScvy7DIR56eBivBsgkjxxp0ZEDNow1L/x0B7RHk=; b=iqWW2+r9it/K1OzsroA9iO3KyZUpDxIpSzQHPMaHuYl7DE0CKzQ+0pOSGt44Yx2YXE c0649mg72RRqrtklQDsoL8oSv74pbMKr0/ozKFuSpV2C2SKnpgjyVHMg2IDwpS1rn8+0 ITV/aU5U9s7RUrUEQoPPXpdXM11RJj2f8sd/RkEmc5dPu2wrf7hXo0+fAxod6JIdnTp1 yBnRWKPF6aaao98ZWSCem/CJFQz9F/to0KzXtN6LPCkgniSa87RyF6TRmGybQzxJg2Oi k0vT1CQB167VS9+EXoUwq3YwLCznau7ibWOgKtQn/RGLfGcIL4ogBHRoAwDm8imK0bpL i2tg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=kFmmScvy7DIR56eBivBsgkjxxp0ZEDNow1L/x0B7RHk=; b=mIrcKAqLuSSFTIKryKOfv6x+qdEojPkE07/eaIgZTAriwdQsPCtC7r9mF1oGEvSacR 8XHCeDMW5jreqhjX7BK3FosaAu9YJdC1eh4EvAMn6rOZA2Rcu8qyq+GPjrE/lG+89CVc VpPtP+bYsD/mgfk/oX4dub6ID9sBjdcddFZavsgFGn9d6MYmS4jBNYqs5oohSun/9TkO tX4zgX3Uxs+rLxEowkTVR9o53Tao9RD2MoYzrNUL+JxcDs20TuPXswhkLxhBc8aU8Dw4 xejRPysbk4wpclrcs7W9vLEtiVNFoEo0la2k2Cs0bFOp2ZAcc06J1AEGoHmrtzxsbKke qkEQ== 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:references:in-reply-to:from :date:message-id:subject:to:cc: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=kFmmScvy7DIR56eBivBsgkjxxp0ZEDNow1L/x0B7RHk=; b=iumvtkw9ZsR5JMaN+qGLwFBdZSj96ABl5b10k42M4HwnGiMT48WhwjiFyG6dC3PuaA c2DBKl7/B6MhpLQlCmMPGWPE/gGraAi2naCtnv6m1JbDSKUjBvXl6ziuJMHdxzt/Gp6H TpmLGPhCvTkG6C5hbk+/Obfz1LZ5wx6U/qHp+qvNt8ctUDWea8f/0Jby4j3OBX1ICOHq JWt3izw3TIKrY7kO8xl/f9as2LfvYPWf/7gOw4uXJzVpKgwo2mSgZDX6si+WesjsUNv8 hWO4RjPRy13Amd0TB8v0DAX8E/Vs8HLfEqyr9S5VXDyPgKdjhJRPR39ltd5zOSPREa7Z VkvA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukeZdTQyV9LKjzRRRB5UKFpB7xDf+6FwvrJ/9Hdd7c6iE6Uy+D9a GraPnJ7LKNHceZ+g0l9HOOs= X-Google-Smtp-Source: ALg8bN7+bDsNMWwyX5i/g3aaIXlu1AiAmkhV0VCjxapiFvJNjxc9ZVzRFsq3NiZsoyks+IHj6NaR7w== X-Received: by 2002:a0c:9ad7:: with SMTP id k23mr150876qvf.2.1547208131472; Fri, 11 Jan 2019 04:02:11 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a0c:bd9d:: with SMTP id n29ls7247487qvg.7.gmail; Fri, 11 Jan 2019 04:02:11 -0800 (PST) X-Received: by 2002:a0c:8b4d:: with SMTP id d13mr6406635qvc.2.1547208131130; Fri, 11 Jan 2019 04:02:11 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1547208131; cv=none; d=google.com; s=arc-20160816; b=ZAp5Iv+wZ5+W0cDOn42wAWBxCkxjvrDERbbiG78dv9LrvGtSP72wxJhtTuGaf7IO6i 7UxQ7CtBxqwAq33jhp3CMlt2ni4lT68ZC0NVe/bIlKl5ylrwM54KdsjfuZQEJqNJZV8v cV2BXvvmYmlSVA3Vr3bR5kJ2dsutMHWKF3zSdDCagAlMUwJtXYwbZV/rn0/BqydajUp4 J8oywa3SdJ8A9OPgwNwfXLs3lnJPd2jXwT7p+PkgA3ra+cepvZICQPJALJLha+oOlhDM KWzOMA/4eHjPPyqNAN9y2eH8wEgi17Imyk+iq+Bjg03PG6nhCPe1oBTY/TyHzkjRUPv4 qAig== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=Fi3vMMa8kgOP6YDixLdnxsoOiTLx+Pq4sfO8AUsxbpY=; b=OTkTRJVHSn/Y8JYCURtsH6bbz8aYN3PIa6Uu5qpkkVr83KsOzivuD1oJSnUF6cy+Zv TQcLVOrPD5/mT/gBH5m7bbwKJbJmYvscJsJihOzTodQKjtzkofTm6xjTWp0xUDOufvYN aFzUJ8pv1wrwCMBg8o5EYQ5uoXh8RhlmebqdOEn7y5nOnD20SwlDlNIiTK8NGJ8QNxC3 NwQ15fMOXwPMsNgFmN9stAIPg5M3786EDYl1nRzwXj8UQin9vyULEY2dXAZGwjFeACVq nw+Cqt/wRAGu6iamnl3IeSrNQLsLI5PJk9KR7ByouOlU9VAygk4UjfdULkUBZ3wAgCRb 4uLw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=u1Xl0hRS; spf=pass (google.com: domain of cory.m.knapp@gmail.com designates 2607:f8b0:4864:20::d2f as permitted sender) smtp.mailfrom=cory.m.knapp@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-io1-xd2f.google.com (mail-io1-xd2f.google.com. [2607:f8b0:4864:20::d2f]) by gmr-mx.google.com with ESMTPS id u124si1798813qka.4.2019.01.11.04.02.11 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 11 Jan 2019 04:02:11 -0800 (PST) Received-SPF: pass (google.com: domain of cory.m.knapp@gmail.com designates 2607:f8b0:4864:20::d2f as permitted sender) client-ip=2607:f8b0:4864:20::d2f; Received: by mail-io1-xd2f.google.com with SMTP id v10so11954548ios.13 for ; Fri, 11 Jan 2019 04:02:11 -0800 (PST) X-Received: by 2002:a5e:8b46:: with SMTP id z6mr9059677iom.7.1547208130769; Fri, 11 Jan 2019 04:02:10 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Cory Knapp Date: Fri, 11 Jan 2019 12:01:58 +0000 Message-ID: Subject: Re: [HoTT] Homotopy type of simply connected spaces. To: Brian Sanderson Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000073820057f2d7797" X-Original-Sender: cory.m.knapp@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=u1Xl0hRS; spf=pass (google.com: domain of cory.m.knapp@gmail.com designates 2607:f8b0:4864:20::d2f as permitted sender) smtp.mailfrom=cory.m.knapp@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: , --000000000000073820057f2d7797 Content-Type: text/plain; charset="UTF-8" Using the language of the hott book, a type is simply connected if there *merely exists* a homotopy between any two paths. On Fri, Jan 11, 2019, 11:49 Brian Sanderson wrote: > 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. > -- 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. --000000000000073820057f2d7797 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Using the language of the hott book, a type is simply connected if there *m= erely exists* a homotopy between any two paths.

On Fri, Jan 11, 2019, 11:49 Brian Sanderson <brianjsanderson@gmail.com>= wrote:
Thanks for= the references. So am I allowed to say a type is simply connected if any t= wo 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.=C2=A0 See section 7.5 of the 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@googleg= roups.com.
> For more options, visit https://groups.google.com/d/optout<= /a>.

--
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 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.
--000000000000073820057f2d7797--