From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.202.195.15 with SMTP id t15mr7441621oif.43.1508272846055; Tue, 17 Oct 2017 13:40:46 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.202.69.70 with SMTP id s67ls693243oia.20.gmail; Tue, 17 Oct 2017 13:40:45 -0700 (PDT) X-Received: by 10.202.56.69 with SMTP id f66mr7153927oia.49.1508272845135; Tue, 17 Oct 2017 13:40:45 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508272845; cv=none; d=google.com; s=arc-20160816; b=U+kb2fS41hRP9p9zsL45byButhet61zauRokvZ+cd25t9xZtmVpaC86jepo0uXmdqJ FZH4yFx0rOJ7O5NSj5r713Aho33PxZCQPSCm2C32qdZAkwIt+G5XJL2v0A6gRiN7lz/Q N4DBpa3JQb/TQo8NoIVXOROcV6aZ1Tm9UlD7HJmLOAd/FEi8ty4UIQiLpv4x7QsN2uGY mxopUj7uWJ1Runz7swMKEzodkpXmQrYj3xTSFCLJgjFe/PqGlvIg63FEqs8sa1ftoptk Y79wc2nKUOq6fTstnQjETjQujg72l2Oj0a0zJ0Ivd1TQTmzazg+0vevKrRg3ztOqBXMn +B8A== 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:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=rb5FZbe1wWw0z9FmnskSI6L1SYz6VsA89cXpAb5TRGc=; b=eHersm/aJmV2hc2adPK60z9poSEUDcVj9WdzpsHRAAClMiRkl9DshnjZr2huGWPnm1 xMDx5GgktuNGE91MSiewGj2i2I8Kj1bEHkY/Lhh5GaMfokvkLHucsFeEHqqcMsVqyYvY Z2wW9rqHF+YAH6nacQGhWWN7sPn1pCZVzMQxHda4qm8YKbgQo1DBD/T7Bmw32hl5Nr/w QaQ1EFkla/mMfLkSGXvVbyHoC1p61UVgYMgoH0A6WyqK/gvALABnj8Hyb0cgUh2SIA1A +9cSvZM0+nMtuCuFu7spUPaUcxRxRf4vOG13rGXx51bmpvFZb4Yfo8dXRmOJeXX/vDsX eVEA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ik2x9NXH; spf=neutral (google.com: 2607:f8b0:400d:c0d::236 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-qt0-x236.google.com (mail-qt0-x236.google.com. [2607:f8b0:400d:c0d::236]) by gmr-mx.google.com with ESMTPS id f130si531235oia.2.2017.10.17.13.40.45 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 17 Oct 2017 13:40:45 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::236 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:400d:c0d::236; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ik2x9NXH; spf=neutral (google.com: 2607:f8b0:400d:c0d::236 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-qt0-x236.google.com with SMTP id z19so6415294qtg.11 for ; Tue, 17 Oct 2017 13:40:45 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=rb5FZbe1wWw0z9FmnskSI6L1SYz6VsA89cXpAb5TRGc=; b=ik2x9NXHljJvI1QeYVMOBm9YyArFLMI074ZrhcuohpFHX5yjcfIZyt7Hw3T9FtzAYh QB1itmX5MltHNCftMPu7/tWIbXSNA431RYTjs8pL6gPiAm7QZGR/nF41UtWT/PIyvsDL NYqB4es84YEm2fOEK7kKiMTRWTyuGgVHn5vkMMoSJQBYCkULQpet4ut43jJ6FSUad1fY AQNMm/0ygFB0EUDc4goPXOxtlga4Dl2fYGZ2gWRiipduTXCWIINq9zGrYIsnuAGMe8w5 tAYvm9ho2usL1wWw5tXNsrHsvr1rBOhI2LPtmyYdttxlgTeHesRk5723LLyrxRxrzQ9Y BX6A== X-Gm-Message-State: AMCzsaWsodkL0M95oSTlFZ1CxCcWvAEtE52RjZgPxkxol6jOSzhF4C4B KHJBNqkor6XCnzKafdJonveWvqLW X-Received: by 10.37.219.79 with SMTP id g76mr3665210ybf.268.1508272844659; Tue, 17 Oct 2017 13:40:44 -0700 (PDT) Return-Path: Received: from mail-oi0-f49.google.com (mail-oi0-f49.google.com. [209.85.218.49]) by smtp.gmail.com with ESMTPSA id c74sm7957002ywh.19.2017.10.17.13.40.44 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 17 Oct 2017 13:40:44 -0700 (PDT) Received: by mail-oi0-f49.google.com with SMTP id g125so5328926oib.12 for ; Tue, 17 Oct 2017 13:40:44 -0700 (PDT) X-Received: by 10.202.63.214 with SMTP id m205mr7892612oia.137.1508272843944; Tue, 17 Oct 2017 13:40:43 -0700 (PDT) MIME-Version: 1.0 Received: by 10.157.7.199 with HTTP; Tue, 17 Oct 2017 13:40:23 -0700 (PDT) In-Reply-To: References: From: Michael Shulman Date: Tue, 17 Oct 2017 13:40:23 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] The Interval type in Hott vs. in real analysis To: du yu Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" The higher inductive "homotopical" interval is a very different thing from the "topological" interval of real numbers. The connection is that the homotopical interval is the "shape" or "fundamental infinity-groupoid" of the topological interval. The tradition in homotopy theory of identifying topological spaces with their shapes, or differently-put of studying infinity-groupoids indirectly by way of topological spaces whose shapes they are, leads to the confusion and the coincidence of names. On Tue, Oct 17, 2017 at 9:39 AM, du yu wrote: > I have seen the definition of Interval type [0,1] in HoTT book as higher > inductive type and in cubical type theory as De-morgan algebra, and in real > analysis there exists continuous function from [0,1] to Real,which means > [0,1] is equivalent to R . How are these thing relate to each other? > > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.