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-oi1-x237.google.com (mail-oi1-x237.google.com [IPv6:2607:f8b0:4864:20::237]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 1a293f73 for ; Thu, 10 Jan 2019 20:36:37 +0000 (UTC) Received: by mail-oi1-x237.google.com with SMTP id w128sf5690759oie.20 for ; Thu, 10 Jan 2019 12:36:37 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=cZqS76ZfQfxHUwjXZM8zpLOv9CTCNHqBnU2OsqGZ3IM=; b=SiZ3fkN1Pb1hr4Jm0Kmw+makX0/LOCnElnP414EIJQg9640dL2z5bfwgY16LDG+y5E /pl+uE5J56RKrAaX37JxjSI/Qi48CuGZnGUkZk2U0ltSy1ucr88vsdv9+crDvTVqOVAm TqoBwOLfWd4SDXazseqh4EMCBcVXkUR8/h3FBbypCwgWHPstau7zryg3Gxg84WXI+mC3 hvda0bKMi37MotsydAIVUrPq1oZcxv4RabijEC4v51rUuCW6v1u+KBWo+IEfhfEhpx2F NQJVhXJtWOBD1aLvGGFBXrdT5fCCPwsu1IyO9QT+ixGmrOaOm/RYeho+eKiDt2CNhXuE 2DYA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=cZqS76ZfQfxHUwjXZM8zpLOv9CTCNHqBnU2OsqGZ3IM=; b=jg4K9iWc6IW3DGzT5t8dElwJeT5GIufhK2qzC3stkROI9QRBcLUpzMA+/1Db4M45kB AcYsKeq1raQpKvDuy2woiMy4k2aSew3HanBj92ysv+2AoSELWFaI2QVMgp8W1wTK/QMw 3XA0Az2Ya/V52TI/bN+t427w6CflbAmyp19nkl9JHxV4PjoZBmwTq0Fe8FWU/QqCjV9Z xWdrGSNlaVmmoT/4bhRAaY9mP1+3j0Ez7WZF3e06jL6jSWzUx5tHdUFpJIsnLRSmr9Cp DUr7rWLbsXs9IF8uOMGEIhnKCq1AZ76nabOXSVZwOVM7wvq6U8zG6lE71z6p8fKJKiw0 nzbw== 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: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=cZqS76ZfQfxHUwjXZM8zpLOv9CTCNHqBnU2OsqGZ3IM=; b=n9qO+5KIc8DS46W1R2U97Zwg0my7kwpcNj76wVwhBeoaq1JWj8AiHq6pBfVG+EhQ4s IQSn3AKBxI1cL275HRB4NTPqc0xEWIXyldSk8UA450YNOy2/ZXKXxsfhj2VgLbvc0UQT dmecT0FKfzF1FX40hdNbr9tmOLwAboS0oP5yWuYmF0z1lpkjC077c37dy9O9tXaDt26K jPZMqHMPOvGmHuUmq5TACXXXIcupl8WuMbBsLJsC/HPDxKssTGV6VlQHkal04Blr8ezq 2Q/vkexec9oUGyBIuyP2C6slXJpAYFT3uaNpZyCWHZ/Ipe4S7Qs6H/DEdIya73M9XDXX r1WA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukdEl0IySz+VzFxoHWREIf2JKjmsK/DOu0/dW0CMfFtBCQS66/Ne gABYNLR+E9qnmLlsA984sB0= X-Google-Smtp-Source: ALg8bN4GnslppClNDL1xBK+vKd8xVxmdG71R+lS0/ezK0IbUJnd8TZSZaBO7Zv8b/t1QxI5nzrmjRw== X-Received: by 2002:aca:c703:: with SMTP id x3mr64382oif.5.1547152596439; Thu, 10 Jan 2019 12:36:36 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:803:: with SMTP id 3ls5817817oii.3.gmail; Thu, 10 Jan 2019 12:36:36 -0800 (PST) X-Received: by 2002:aca:cc0f:: with SMTP id c15mr65596oig.3.1547152595952; Thu, 10 Jan 2019 12:36:35 -0800 (PST) Date: Thu, 10 Jan 2019 12:36:35 -0800 (PST) From: Brian Sanderson To: Homotopy Type Theory Message-Id: Subject: [HoTT] Homotopy type of simply connected spaces. MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_512_523439618.1547152595240" 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_512_523439618.1547152595240 Content-Type: multipart/alternative; boundary="----=_Part_513_2133521989.1547152595240" ------=_Part_513_2133521989.1547152595240 Content-Type: text/plain; charset="UTF-8" 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. ------=_Part_513_2133521989.1547152595240 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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 o= f paths to homotopies between them. What would the type of a simply connect= ed space look like? Can I say in type theory any two equalities are equal w= ithout having a function?

--
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_513_2133521989.1547152595240-- ------=_Part_512_523439618.1547152595240--