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.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-yb1-xb3a.google.com (mail-yb1-xb3a.google.com [IPv6:2607:f8b0:4864:20::b3a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 6c5a3d98 for ; Thu, 10 Jan 2019 21:12:13 +0000 (UTC) Received: by mail-yb1-xb3a.google.com with SMTP id v71sf6130819ybv.17 for ; Thu, 10 Jan 2019 13:12:13 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1547154732; cv=pass; d=google.com; s=arc-20160816; b=bQWS7c66L4CBXB5lzsVtY4luvSP85PLYdjv4xhOgiEBcGk1E+KmKxyI2HPjmUa9xq0 BvMZ93U38L7nVPaWSFASx5Uf5SVK21PcSvJ/ahDVnVQMmO05vZebYPMVte0dWq5LtimR +hYkerIsqXxhG+WY8nUENN7dfilVVQbsRMhmWudhATiivjKXmT1Qmv0gm+6enqXNlYRD SXP3128KaGYYArWSyF+m99d3NF/Ciah4GwtkxIgOlVOX7zaQFblc4yn7KG3xOp1SfYnz h3tkFMOqIaOPEuIOkbWhWxjhBFKYFZGqt7kh5KU14AnqvS5Ly1RJARmdscd7+Ywx/q9y 49hw== 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-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature; bh=lOWDefAe3SCFeVkw1IwnkZPxxzuqpA9OEN0sv55XN8Y=; b=Dc8vObFtVc4NHef5lyhVPLa+Zae90OgWL8Q9B8U2KxaAzu1pRrnQ7hOyFYRWSWpGQV mB5EGBuKe6/0iqC3o0fVdU9577rmWBgdHwJKPjeUuoibRUW1yODtt1zMv03u/sNKfKHh abxWADM1EWWnvB5hknKv5zZaO4mvpizXOzSzT+yIOAP+bNm71qb7V3QsBt4ft2Q4KgfT qhVFf2uvYtdV9voNJ1wNd4j800dJKDowHiPkgkrkhe+7FcdP6tVQmDO/A7SRVbLuTCU6 hwLfw4GUDndwUowNbrq5HIwSHbNfAhXOu4M6lGP4g0mk8/70xeq9SuF/+9QTdfagZtlX 1yqg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=KxSHL8rO; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2c as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=lOWDefAe3SCFeVkw1IwnkZPxxzuqpA9OEN0sv55XN8Y=; b=dcItPQVcyFFJMvqcHZPJe5pZl0kQXBsKcgPLIafHeDwHBgNINeOnHx4W2dFrVCHSqK 3Dlaxvg+RXM5S7uW1J0WONRb4a6BTAZzvzKoW22bYqebL56MDSWRZ5bShgoMGLyqFILm clBLfa1DeZFvuNQlxqrxAnRQvB4+4RJGIga9cREAqV1BgzAw3HK3nAW5c8Bwr858X23j LwzgXqJWytrQ3ZC1/uTFxB6WK5QItXG6VoG8ONUpsDHDuPqZl/bszlijg+s22MI0mkl2 zlO48ni2/Zl2+05kbSND+GSp+M8AoggJvK58kmhOEvIKALh6E30lAQAZQti4Nv5Huosm cGIA== 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:content-transfer-encoding :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=lOWDefAe3SCFeVkw1IwnkZPxxzuqpA9OEN0sv55XN8Y=; b=SUAWWp+osk8e/fxJnPL9bcgiG+vEE60ykvVTCCT+fkvu6FzMKppcXdHe5ob7waVKtr GVSQBGHEs0GHYswoOKQf8gyK11IXloqdVwmvZfXP0YobLHFIrpMLTzhGTuxMx9jhjvDc dxE4VME6sOLB9FGIkfmtAYxgHkk9GmCDnzYObDmoVO519Ev37VCCVYYdCOePIJKQqr4K kWHEOd2+qdx2UXIsOu0hO9zoRzYCCN0FqU9banv8nhkrv3O7ZIrm/Jqv0+gylPL7gfY8 9GPK+WtvHQcTSJm7JqdvH61wkRx4HAcWjF5+G4B5O/etYCPQkrPvak1eZgeCrlzWY3Ct I95Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukd4UVNAtYy+jGgmdiQ6rxsds8De9RWHp+CxV8YMQPq9u5gVmqMJ IvIPTjFhCBx4zPqWh4Wl9BY= X-Google-Smtp-Source: ALg8bN7b1lPdv4sVoDcggfAnmcIKxi9ZN5coz19sTIK8yJFM8LW5niDc56wJMFX97vaf7Oh+dCy9TA== X-Received: by 2002:a81:27cd:: with SMTP id n196mr86535ywn.2.1547154732673; Thu, 10 Jan 2019 13:12:12 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:2491:: with SMTP id k139ls4225210ybk.3.gmail; Thu, 10 Jan 2019 13:12:12 -0800 (PST) X-Received: by 2002:a25:69ca:: with SMTP id e193mr3549187ybc.62.1547154732355; Thu, 10 Jan 2019 13:12:12 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1547154732; cv=none; d=google.com; s=arc-20160816; b=N3Zj02Ai65CkR66WViRCCcZJlr5s2dBBaQH+8qfqt09FN1UFTH1kCx4+fBdALMMo0d XBVAaNDgzBUKkknHP3wSwwCTKVawFnQ7rVmt+pX//ZAidfO0KYjx7qrwS7+SbG/LNmNC g31ze/dWlQJFpkMk7GRypIYK+Vb2VtYxB4qM2gfkeHVy/0+tkMS1AIpcf7hVMz5rr752 9gXIzLj6TKFwPlUVgUoaF88BFmkPRUi9sUBeY+/tMH+tWEmUs5P0Gtz02qkkl4WYBsDF AdvwSj8rfS9dDbfbfxQ4k04yzpFSPrNZztsYVW/OIT2vO7dwUFGMBGMpXFEe7HeInszp dRRQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=Okyr2t+5bvvrBAzTlYB8BQfejGnIxJ60MY+xtbmev6I=; b=qaQiHYb+0CNl4CxW5eJgR200LT+A7Dmh8fkGo18FrHRtiJver4uHfgjUKxWGr7NP5J KjLevYMBXg/3B5UDXUVTgqzRhDFaue5717ij/zf+KmGrx1kPHum4N7o6omj8ZtLugCJ0 qVMDmR8Yw3j6pag3K5OION0Sc4F7iAjCj+KsXiMrkI9LKtojMHSz2MfPdyYxeoYlv3Sb YpEm1P05ZXHMtIiULbNyWIvNMSEli7+IGR3p0V/MmQooaRG4KztPVzsro5BS5PVW5Msx j44+ziD9qcvVkl2bEfRyXj1FG9vH0n4WjPKyK5opSL0WTEJklIjkHmSj6rAdVZUHBFDl mJOw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=KxSHL8rO; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2c as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc2c.google.com (mail-yw1-xc2c.google.com. [2607:f8b0:4864:20::c2c]) by gmr-mx.google.com with ESMTPS id q68si3264885ywg.0.2019.01.10.13.12.12 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 10 Jan 2019 13:12:12 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2c as permitted sender) client-ip=2607:f8b0:4864:20::c2c; Received: by mail-yw1-xc2c.google.com with SMTP id d190so4968937ywd.12 for ; Thu, 10 Jan 2019 13:12:12 -0800 (PST) X-Received: by 2002:a81:7c04:: with SMTP id x4mr11526322ywc.264.1547154732029; Thu, 10 Jan 2019 13:12:12 -0800 (PST) Received: from mail-yb1-f182.google.com (mail-yb1-f182.google.com. [209.85.219.182]) by smtp.gmail.com with ESMTPSA id j136sm196405ywj.88.2019.01.10.13.12.11 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 10 Jan 2019 13:12:11 -0800 (PST) Received: by mail-yb1-f182.google.com with SMTP id o73so5030774ybc.0 for ; Thu, 10 Jan 2019 13:12:11 -0800 (PST) X-Received: by 2002:a25:384:: with SMTP id 126mr11426568ybd.357.1547154731163; Thu, 10 Jan 2019 13:12:11 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Michael Shulman Date: Thu, 10 Jan 2019 13:11:58 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Homotopy type of simply connected spaces. To: Brian Sanderson Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=KxSHL8rO; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2c as permitted sender) smtp.mailfrom=shulman@sandiego.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: , 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 homo= topies between them. What would the type of a simply connected space look l= ike? 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. --=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.