From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,HTML_MESSAGE,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 9681 invoked from network); 11 Nov 2022 23:47:47 -0000 Received: from mail-pj1-x103d.google.com (2607:f8b0:4864:20::103d) by inbox.vuxu.org with ESMTPUTF8; 11 Nov 2022 23:47:47 -0000 Received: by mail-pj1-x103d.google.com with SMTP id x14-20020a17090a2b0e00b002134b1401ddsf3401285pjc.8 for ; Fri, 11 Nov 2022 15:47:47 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1668210466; cv=pass; d=google.com; s=arc-20160816; b=O5CDwr7LLlLbc/SjHdZRFl7dZeklEUwUOFhEgCzw3O026oz5m8MSf7LHceFgUSkK47 LEQ6cFpGGxeHLxADRmsHcGWz52FGdCSuoXDA5yCOThqFaVvyc/c+Y3NybfbRSIa5yL17 WwaMRz9sYm+YehW+3+pKhplaIdyEGEAdQVMfd6yzWuLWz+GYvTCnW4p2KCYSxvl4Rser OPgxXk73LAlmKHpZM34QiMPVI7z2AgYYg50BO0VNfSUCzHsJVnelP0QnUe66RVHbPuIB uVpIgFxOvporycc+5DMAdCW7qZaNOiF1NxSYuuoaSc/wZJMYKKBAMq3odHbuzuYEC7A9 wwOA== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe: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; bh=Z9pKQpj7JIs61G0vAE9GNqXfQ1sSnPVg79XJEI1YHTA=; b=M9O6EXCqDihaGCLl0CVj7UiG7IoIUMi4yVXkU+bG+hsf66gj+238/EZFDpPBcWkOEC 3c1faypsD2ZsT6fwnbmQCbNMt2RElzczkRcpswgJVrhMUUzD6je9b7k9NpQ+4wAast1+ RzuKAhYpkM3msB5tOrvFYuoc9bYW0K+dvcXXtrn1+aCTXfLolGohjffxht++sgk50QVe Tpuau2s+ENvfZB02LseJkJcBVnfwxnLzdVddP9s7n3Q8GqbmtJoz40QBwPeKrP6Jo+pl 6hqXRjO3fwJ5i1HewA7ILFlO9MlMG+4c1rIN0qCGilOpYkbjbTlDVUaqMiZUi4w4xC+Y fBVA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=M47JCuWh; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::112e as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:cc:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:from:to:cc:subject:date:message-id :reply-to; bh=Z9pKQpj7JIs61G0vAE9GNqXfQ1sSnPVg79XJEI1YHTA=; b=YDvqk4Z59I4cRV5kiFkD6CvZw/9GmtS2L0D3HK+kf/yctD/gdTidmGaC4jPp21OYZ9 U/1UQ38wZRYs1Gxz7OeYll8vZz7swjhbj9/goE0pzEHajXzbHpRqXvTXboosyV7HFS2a fTGtgZeav2NEgVR5HIFaKKyT1J6EasfWVRiyMRWoXYb6Og6QRUKU/H9YZEjmwfbltxfJ TmYP5IssM3/MhtHyMue2Lg9vHZZ4Qbnww8Nqn75IneAs3eA0/Qs63CxvIn5GXk6k75pD Rd/QzDrCpBqnlloMhpptSm60B9PtiLxH0YFPyLnSKJbzdf1EQ0hMsfiE28ShaI5FuwZa C+6w== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version :x-gm-message-state:sender:from:to:cc:subject:date:message-id :reply-to; bh=Z9pKQpj7JIs61G0vAE9GNqXfQ1sSnPVg79XJEI1YHTA=; b=PAlXbo30/2poRslC5uGTPauljenP5PdIn0xCiQfTeIlj/UZdIQhDRxOIexiDfzUmOe CSxiHgsK5gWDfpaq2X0P7dak1m6VOjA5qqu5lA/+3olkomrrNK7kNi9U6GH4/3nURy9I pl+LwtLOucVcK4FWLkR+E2joX1uHkocf51hh8PJfRrcyDS26jsQlexQy00uBHdEhB4Pp 9hKrA+/ZGZFe4Fbn4eKZbCUMcXlAWEwvrhPNMsewY5m6/B4imMAcc8M8OBVHEFbmyJUK o/fKqkglWc49MMOFz+V1s/HjLZX4PiEvsdYTV3dGJPKeQ5T3o3NqN0i1MhwfTgF0sMQD EnHA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5plXz1bihDDNNb/OUEjTYc6JT2wgY/mqTbjLawIrwJ5qMtnnLQwF pd+CRrzMw4T5G2/OCHnWl9s= X-Google-Smtp-Source: AA0mqf7POFsWA4jMiojQ8SJ1AvBU12lhIqkCrDax9Znx288MS3/BkCkRKIef5TwfCtnvL+KGTux9YQ== X-Received: by 2002:a17:902:e8d2:b0:187:3c62:582c with SMTP id v18-20020a170902e8d200b001873c62582cmr4629424plg.114.1668210464792; Fri, 11 Nov 2022 15:47:44 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:90a:a002:b0:210:6f33:e22d with SMTP id q2-20020a17090aa00200b002106f33e22dls4429794pjp.2.-pod-control-gmail; Fri, 11 Nov 2022 15:47:43 -0800 (PST) X-Received: by 2002:a17:90b:2415:b0:212:cf2e:2b0b with SMTP id nr21-20020a17090b241500b00212cf2e2b0bmr4183605pjb.169.1668210463194; Fri, 11 Nov 2022 15:47:43 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1668210463; cv=none; d=google.com; s=arc-20160816; b=X4iWM6eRztUf0bRHLCMkcSK9JIOjlXk9jiRr3tQfM4tTP0T6W6hSieKJrYgL0IiNfW cTrAShOhqpm8VgzeRdFhOUmAoE1sFHs1bJ0VNG9YU50HR9cH4AdWGdVhvFn/O7KVJ+Oz YIdj1ECw+tYyO7A3uB3KIC5pXq24oFsicGO5j5xxNJx5hNPiPsKY/qJYnjyp1x3fZhx2 ZG5xbBdds58Il84/YxxkGs8PgI7cZD2mIjNlLcRkMLqbO65HuJ9eYjB+bzdX+6tZPTF6 0fOzwf6DCrqJeawlaQc3F5Npw54ZpB0bwpqFwtJ+xLMyt2t8Gzt/0qf0DP25YeDTdqth 2EnA== 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=G3uMf7BFSIkUBrgIRrU1rEP5ceVuT8cTw7AbOnhEvAY=; b=Idq8iaK5eGciU4Hb/wKJ8xl7jEbe9OV70TZoE0ceI1qTeMbO3JE8/+9ZrACZiUEu0u rYCuMu6RkhJgcy5/EcD6lWMPDROdKyzfxcoOW962VwZHyjVRUiaeQmppCAuLoobO/UUy vbyvJy9HAOTjSAw1RKsHntX7h9+AHavPl/tTmunjLLEXmRf1m/9qurvC+RGDvNHW/c8t NP0TvrkFRkhMZBQ4Cnu0/UvqE6jgMG37j+cTbCESk4MEDXsCGX7sDaMeQ6MIQCjvld6a 6897g67UwkuPnioyiOwId1iGz0ZvdGLkcLgfHQCk1EJS7UUIEQ/doUYuregfYJ8xEMyp M99A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=M47JCuWh; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::112e as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: from mail-yw1-x112e.google.com (mail-yw1-x112e.google.com. [2607:f8b0:4864:20::112e]) by gmr-mx.google.com with ESMTPS id l8-20020a17090a850800b00213e4d5cea1si411134pjn.2.2022.11.11.15.47.43 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 11 Nov 2022 15:47:43 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::112e as permitted sender) client-ip=2607:f8b0:4864:20::112e; Received: by mail-yw1-x112e.google.com with SMTP id 00721157ae682-36ad4cf9132so57182217b3.6 for ; Fri, 11 Nov 2022 15:47:43 -0800 (PST) X-Received: by 2002:a81:70e:0:b0:35b:fdb5:ce84 with SMTP id 14-20020a81070e000000b0035bfdb5ce84mr3962774ywh.312.1668210462463; Fri, 11 Nov 2022 15:47:42 -0800 (PST) MIME-Version: 1.0 References: <96f15467-49c9-43cc-8868-40b1bdf2162dn@googlegroups.com> In-Reply-To: <96f15467-49c9-43cc-8868-40b1bdf2162dn@googlegroups.com> From: Michael Shulman Date: Fri, 11 Nov 2022 15:47:31 -0800 Message-ID: Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory To: Madeleine Birchfield Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000006b8c005ed3a8413" X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=M47JCuWh; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::112e as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=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: , List-Unsubscribe: , --00000000000006b8c005ed3a8413 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Substitution and weakening hold for all types with the restriction that only crisp terms (i.e. those involving only crisp variables) can be substituted for crisp variables. This restriction is mentioned in the beginning of section 2. On Fri, Nov 11, 2022 at 3:14 PM Madeleine Birchfield < madeleinebirchfield@gmail.com> wrote: > In Mike Shulman's presentation of cohesive homotopy type theory in his > 2018 article Brouwer=E2=80=99s fixed-point theorem in real-cohesive homot= opy type > theory, he states in section 2 that "All the ordinary rules of type > theory (=E2=88=8F-types, =E2=88=91-types, =3D-types, W -types, HITs) are = imported into our > theory only in the world of cohesive variables." Does this also include > the structural rules of type theory such as the substitution and weakenin= g > rules? > > Madeleine Birchfield > > -- > 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. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/96f15467-49c9-43cc-8= 868-40b1bdf2162dn%40googlegroups.com > > . > --=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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CADYavpymP9gVGU8oy-m-NKtS_8f7fgR5WRBoMaY3NUSRfPejFQ%40ma= il.gmail.com. --00000000000006b8c005ed3a8413 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Substitution and weakening hold for all types with the res= triction that only crisp terms (i.e. those involving only crisp variables) = can be substituted for crisp variables.=C2=A0 This restriction is mentioned= in the beginning of section 2.

On Fri, Nov 11, 2022 at 3:14 PM Madelein= e Birchfield <madeleine= birchfield@gmail.com> wrote:
In Mike Shulman's presentation of cohesive hom= otopy type theory in his 2018 article Brouwer=E2=80=99s fixed-point theorem= in real-cohesive homotopy type theory, he states in section 2 that "A= ll the ordinary rules of type theory (=E2=88=8F-types, =E2=88=91-types, =3D-types,= W -types, HITs) are impo= rted into our theory only= in the world of cohesive variables." Does th= is also include the structural rules of type theory such as the substitutio= n and weakening rules?

= Madeleine Birchfield

--
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.
To view this discussion on the web visit h= ttps://groups.google.com/d/msgid/HomotopyTypeTheory/96f15467-49c9-43cc-8868= -40b1bdf2162dn%40googlegroups.com.

--
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.
To view this discussion on the web visit https://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CADYavpymP9gVGU8oy-m-NKtS_8f7fgR5= WRBoMaY3NUSRfPejFQ%40mail.gmail.com.
--00000000000006b8c005ed3a8413--