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.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 5571 invoked from network); 11 Nov 2022 23:14:29 -0000 Received: from mail-yw1-x1138.google.com (2607:f8b0:4864:20::1138) by inbox.vuxu.org with ESMTPUTF8; 11 Nov 2022 23:14:29 -0000 Received: by mail-yw1-x1138.google.com with SMTP id 00721157ae682-373582569edsf55622047b3.2 for ; Fri, 11 Nov 2022 15:14:29 -0800 (PST) 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-sender:mime-version :subject:message-id:to:from:date:sender:from:to:cc:subject:date :message-id:reply-to; bh=F5uU/144HFW1cJO8rsCN3LS/nXhTo01zlbmhPGkFBcc=; b=b3NTcwMOElSiJh/CPfzB1aoXIX5YvliCKwKJBG20KfqBGimdj+2DmaOka1Wwrt7ZZC y9KE4s/tFLyOnflH77RYP6a4F+NEFqmdCyXOwOmlONkqFgphV+i9QohCnPiyFPC28JoQ 9/JB3Y2yHYCQvcqj6GfRflsq4GzEpuUzdFYlZSbTydPSqyNX0eGOyiwnkMdf/289zH9q AtF1DymO+uBa7JN8EwHBauF74pZVORIM2v7Hpyp/LhRlaqentFQqXMon0jKG39p8zgCf bb90bewk/b4hfdZcDzm1KNC0BcpiuIdB+qfglZylr5S/hDtvGlTjmsiU9YRDS66IfJpc EGog== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-sender:mime-version :subject:message-id:to:from:date:from:to:cc:subject:date:message-id :reply-to; bh=F5uU/144HFW1cJO8rsCN3LS/nXhTo01zlbmhPGkFBcc=; b=gqDw6MdydvZ4wcL+nVphTnF5geic/4+VPaopxHKLx2PgU46ECJfjsiKmHDeg0hF9bL Wk3AtlcbfXFz6ljNxVLpY2ezyN4RZfZcqTGHfQwIy/zg37QsgHg8VRTDJ5GHsuz9dDR6 DAYBNMWS8L893GbsUIG76TqUtOYeDr4qEU9eCRGPEqQ4swXsF7m7E5nNiunJZk3htA0n TnmomSkeNeY42lY+Km2GpngUzDZFLBZeYZkh11ESNeUTCB5DKjOkAfvs4s9NV6H4d+G7 ytSqtA8zIduvXf6cadnsDS7ywVt/nD0BhoaxQMQ/6Y1L2uY8yQadKmJFrZfsuMsnZA+9 NSnA== 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 :list-id:mailing-list:precedence:x-original-sender:mime-version :subject:message-id:to:from:date:x-gm-message-state:sender:from:to :cc:subject:date:message-id:reply-to; bh=F5uU/144HFW1cJO8rsCN3LS/nXhTo01zlbmhPGkFBcc=; b=j+a8eMDK8+Sm+aGtvuVgG+Jcexdtxj1A82vZXWgjaNrF1s09Efmgqajohx7YjZzv4X rjp4N9s8uOPLryd/zRrk+luywXPJJi+spfvldbz2wjDKA0a5hpPWIaAMHhxdDEcHhzQk p/J1QwrI9KdrIioFXHddHoINa0Co+7dTOhGLZyC26PaKeYFgoD9Yd0gy8u6ew7M+ktvl UB43IVM3/vNdhf0ROF9+3AvjCtW74oUFo0kaxalLgSq5jQuask5/l/5LNFqkgzxIdoPe nyxhxFeopq9HrlcU5lqGtxS04j0ePp49RXC8ftd0ZVRG/UsL6lFcD9GbJI1gEyb8AyBu sRcQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5plhlfZ+J0s2Bt65KZbTgp0y2csrD+e+Iaq+0+QxEovr8h22/eyt meUlbCj0uNG3D6HmUp08IUY= X-Google-Smtp-Source: AA0mqf7dAAZ/g6A1qLr36qlEvpwE+d0j2hJm7LwQh3T6KT762PuFgGQpJlEWpbpqI/QsxyWhC121wg== X-Received: by 2002:a81:5056:0:b0:379:d225:4360 with SMTP id e83-20020a815056000000b00379d2254360mr3862558ywb.423.1668208466429; Fri, 11 Nov 2022 15:14:26 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a0d:fc42:0:b0:373:6b5d:4369 with SMTP id m63-20020a0dfc42000000b003736b5d4369ls2990462ywf.6.-pod-prod-gmail; Fri, 11 Nov 2022 15:14:25 -0800 (PST) X-Received: by 2002:a81:a18b:0:b0:377:7d37:f293 with SMTP id y133-20020a81a18b000000b003777d37f293mr4021347ywg.198.1668208465387; Fri, 11 Nov 2022 15:14:25 -0800 (PST) Received: by 2002:a81:f48:0:b0:36a:efd4:b0e6 with SMTP id 00721157ae682-379fe2bfa63ms7b3; Fri, 11 Nov 2022 14:53:23 -0800 (PST) X-Received: by 2002:a25:d808:0:b0:6d2:e45c:71c0 with SMTP id p8-20020a25d808000000b006d2e45c71c0mr3850036ybg.153.1668207203466; Fri, 11 Nov 2022 14:53:23 -0800 (PST) Date: Fri, 11 Nov 2022 14:53:23 -0800 (PST) From: Madeleine Birchfield To: Homotopy Type Theory Message-Id: <96f15467-49c9-43cc-8868-40b1bdf2162dn@googlegroups.com> Subject: [HoTT] Question about the formal rules of cohesive homotopy type theory MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1458_170633278.1668207203226" X-Original-Sender: madeleinebirchfield@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: , List-Unsubscribe: , ------=_Part_1458_170633278.1668207203226 Content-Type: multipart/alternative; boundary="----=_Part_1459_291683346.1668207203226" ------=_Part_1459_291683346.1668207203226 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable In Mike Shulman's presentation of cohesive homotopy type theory in his 2018= =20 article Brouwer=E2=80=99s fixed-point theorem in real-cohesive homotopy typ= e=20 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 i= nto our theory only=20 in the world of cohesive variables." Does this also include the structural= =20 rules of type theory such as the substitution and weakening rules? Madeleine Birchfield --=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/96f15467-49c9-43cc-8868-40b1bdf2162dn%40googlegroups.com= . ------=_Part_1459_291683346.1668207203226 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
In Mike Shulman's presentation of cohesive homotopy type theory in his= 2018 article Brouwer=E2=80=99s fixed-point theorem in real-cohesive homoto= py type theory, he states in section 2 that "All the ordi= nary 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 var= iables." Does this also include the structural rul= es of type theory such as the substitution 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 https://groups.google.c= om/d/msgid/HomotopyTypeTheory/96f15467-49c9-43cc-8868-40b1bdf2162dn%40googl= egroups.com.
------=_Part_1459_291683346.1668207203226-- ------=_Part_1458_170633278.1668207203226--