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,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 27022 invoked from network); 15 Nov 2022 22:39:01 -0000 Received: from mail-ej1-x63c.google.com (2a00:1450:4864:20::63c) by inbox.vuxu.org with ESMTPUTF8; 15 Nov 2022 22:39:01 -0000 Received: by mail-ej1-x63c.google.com with SMTP id jg27-20020a170907971b00b007ad9892f5f6sf8265111ejc.7 for ; Tue, 15 Nov 2022 14:39:01 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1668551940; cv=pass; d=google.com; s=arc-20160816; b=Ttbbd2St+upsXs5smhJ6uAOvUCebTJ1qb3++9/ub3HEoTUAhnKDiZF8zQHk3mqmB28 cSDt5sJSe2zm7ddEcimWny21MwPlRGBkTJOjKdwctzz58/PuW2tROl1/Q//rzf+JeAXG Hq0az8lHP5Dll4a60s4+X5oAyJe1YMrO90BVmbaUIj9nt6EdLdd8l34ekFHyR5OAEozf HG5mXyU8x7R/NPLJXbAIeMlwKYuOFPzya7BlFncioDiX9Qb+Zs5JvLKlbvQSdPFICshg OprSdVt6sFfeJtbF69qKd3c84Sb6gBg9Rb4ob2v3PrrqmPYggzGq5ntD7l+O2MGNr0N8 RRyw== 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:message-id:in-reply-to:to :references:date:subject:mime-version:content-transfer-encoding:from :sender:dkim-signature; bh=fhjFvT+eBZxDiX9iymzlkMH1qLj+ijkLeA7cmN2gp4Y=; b=yO/yRMN1oAp7WXEhlD6HSbkPS1SSDqCTK63nfJ1V9LN9Ncs5K7/nglVZ/Na2RQ6Wo0 c/Anyos7kuXZqz97fXC4WP1+/kEJVvp9BP6GHJe/YghiKcg/l3L8Jjsz4PzYtOGfxpKc at2hNea5vZVYXPfHsJxUoCp2FVOVu2V4Z/XrXYEtRMT9b2I1AbgKwzTx71xZpWW/oIlc kfi/dA2yexY7/K2rYrnXWasUSML9JHuN9zmVLw9UKnuknht8iqXp+IiuRGEcN62vKW9t cLXezpjfY7wvg97lmm/nyWC4q12pa1mIVa/cL5vVm+Ala8FoE6lVS1bg5k4CQ3CSfsJm waig== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@andrej.com header.s=sig1 header.b="FGgb/63q"; spf=pass (google.com: domain of andrej.bauer@andrej.com designates 17.57.155.22 as permitted sender) smtp.mailfrom=andrej.bauer@andrej.com 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:message-id:in-reply-to:to:references:date:subject :mime-version:content-transfer-encoding:from:sender:from:to:cc :subject:date:message-id:reply-to; bh=fhjFvT+eBZxDiX9iymzlkMH1qLj+ijkLeA7cmN2gp4Y=; b=FbXVPOept3yDgEaycEyR93sRRqDlyRtWw5YNKfKkju3KKxxlsYlJCv/HPt08aU0cdi OkLm1yYuG88JgcZpPrpq/3mOdTeSB/y5s5yQWNVXQ+YxZF36+Au1CvB469rego8oWDas SqOvf/F79pjswH07U0JQPmF5me9U4HfTduLKvsosq9gvfHP+2FZJIC3pTtq9AuYBv82U 55E5EGcNFqgQcbV8fJogs2J6G9WQveSMPWtv0fJALWuqLopSd+AyygS4FVi9zf1MQhT3 KeJRz1WclebFpX1zfZFnfrPrt5+0A7AWC0PSgR1DrkGJQVkDhWpRN+TrSKzqOhQxK/j8 YioQ== 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:message-id :in-reply-to:to:references:date:subject:mime-version :content-transfer-encoding:from:x-gm-message-state:sender:from:to:cc :subject:date:message-id:reply-to; bh=fhjFvT+eBZxDiX9iymzlkMH1qLj+ijkLeA7cmN2gp4Y=; b=al78lMYrQgR7KaRykssjDCz241nEby9BltnGs6Tg+telH2pBLGQWwJJLSObAKAxLhc AGUZQfTrkZaCHA7BjqejABx4PT70SeCzWb+VUzy+Q3iWHuLXnd/4MSoc0H6QPUfLkg2Q YlxOn16OsunPQVIvQBa+cqZfq5O0DC4sm6LxQ9iQfNSv1TlnqNRWMoBEH+jXoWUgXz87 qcOyq/w2I6jUZXcfZl0wbS4zVoJQA9i3UyEvcLtTtyTJTK1KVCzrSC9ytYXl9bS5/nA5 QBq4DXo1CNhEP3A/gmmzeRFuz/vR6qQVsp0PbnijUqk3gXqm4d1009VKcnrClKlpmd+y Pi+g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5pn0l52HGyKqGWUN0bUGyZhRs/UDgiQPjta8kH/eeERhX1xoNsW7 5SIBDj2EsMJ8LuSNe1K6So4= X-Google-Smtp-Source: AA0mqf5KfixwCBE1JRhrTML2UgxLfndvHm7Rlm3IMi1qeDHGDKQ1DUtjMQWKmyNP6V7uBZOvmtA8/w== X-Received: by 2002:a17:906:fcd8:b0:7ad:d18f:c2d6 with SMTP id qx24-20020a170906fcd800b007add18fc2d6mr15875544ejb.271.1668551940046; Tue, 15 Nov 2022 14:39:00 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6402:2708:b0:457:99eb:cba9 with SMTP id y8-20020a056402270800b0045799ebcba9ls4930060edd.0.-pod-prod-gmail; Tue, 15 Nov 2022 14:38:58 -0800 (PST) X-Received: by 2002:a05:6402:c05:b0:460:5340:d522 with SMTP id co5-20020a0564020c0500b004605340d522mr16563890edb.87.1668551938001; Tue, 15 Nov 2022 14:38:58 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1668551937; cv=none; d=google.com; s=arc-20160816; b=SHIcO4JxybGjEqMdamWVCaJ0k6Qt96TUaDi3GeRfhJlUv1GTYjgOfp6+qy+Kv8/WQV EbT/4VapQ5CKrQzFrPcuatwBMlnvu5GsvtL87zSWWobcO4vI1VolFrLy7etvws0ppyQ7 1dvFhNcWNno9SiXyTrtaoKmlGMaScIf2/rkqdQV5U6LYuIip8uerDW1bInJXKkCDqfFV 4G9cW/MHApSmofXjBwpCvgMNV5HuneAuKv5SRb85sBCZgp96LolffN7SGye0LHAWoNcy wpzlcZ6BkBRo7ONKzX1+VndsCG/jyvm0sZIxaP+2rCQBc0JOLgrbivnvjAw3BOwRQdrv +6ag== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=message-id:in-reply-to:to:references:date:subject:mime-version :content-transfer-encoding:from:dkim-signature; bh=MxGO+8kUKoeNc9o3pX28YBBzsKx98QMovbjfc7AfkEY=; b=rrjiDZouU5syxMXv897o8ZTGidFW9fWXP4JTOihzVmwzbqMB9NBVtu9MYGKgxcyY9G h+aBfZLHWkeT8pYgowFvS1WLhCPki6UQfYU+pQJHV7FyJipUMivDlJSeC5y1RuO/yGs8 1mAAAGLkzswGf3IJ9mpZDFBDQwITrm6GQ0o/YQuqsbJ5GA+pCOgFU/gp+8A4jVT084qq LfelSTG+o+Z/u3hEuKub6oaB0BI67JTypn3TSrWEKQS9jNZOMbHC2tMicAm1gi09xR8K xqQkiD+EAj+03NEkoz66nbvW5NcZnFtB+NH5GUe3lwz/RcLfhjK1XIoRrUCbOZtH/mtH jrLQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@andrej.com header.s=sig1 header.b="FGgb/63q"; spf=pass (google.com: domain of andrej.bauer@andrej.com designates 17.57.155.22 as permitted sender) smtp.mailfrom=andrej.bauer@andrej.com Received: from qs51p00im-qukt01080501.me.com (qs51p00im-qukt01080501.me.com. [17.57.155.22]) by gmr-mx.google.com with ESMTPS id a10-20020a056402168a00b0045bcf2bacbasi517360edv.2.2022.11.15.14.38.57 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 15 Nov 2022 14:38:57 -0800 (PST) Received-SPF: pass (google.com: domain of andrej.bauer@andrej.com designates 17.57.155.22 as permitted sender) client-ip=17.57.155.22; Received: from smtpclient.apple (qs51p00im-dlb-asmtp-mailmevip.me.com [17.57.155.28]) by qs51p00im-qukt01080501.me.com (Postfix) with ESMTPSA id 5221E1980626 for ; Tue, 15 Nov 2022 22:38:56 +0000 (UTC) From: andrej.bauer@andrej.com Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Mime-Version: 1.0 (Mac OS X Mail 16.0 \(3696.120.41.1.1\)) Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory Date: Tue, 15 Nov 2022 23:38:54 +0100 References: <96f15467-49c9-43cc-8868-40b1bdf2162dn@googlegroups.com> To: Homotopy Type Theory In-Reply-To: <96f15467-49c9-43cc-8868-40b1bdf2162dn@googlegroups.com> Message-Id: X-Mailer: Apple Mail (2.3696.120.41.1.1) X-Proofpoint-ORIG-GUID: jCx1WA5tDljlnvJ_hHjvsw3DSINjAwwW X-Proofpoint-GUID: jCx1WA5tDljlnvJ_hHjvsw3DSINjAwwW X-Proofpoint-Virus-Version: =?UTF-8?Q?vendor=3Dfsecure_engine=3D1.1.170-22c6f66c430a71ce266a39bfe25bc?= =?UTF-8?Q?2903e8d5c8f:6.0.425,18.0.572,17.0.605.474.0000000_definitions?= =?UTF-8?Q?=3D2022-01-11=5F01:2022-01-11=5F01,2020-02-14=5F11,2020-01-23?= =?UTF-8?Q?=5F02_signatures=3D0?= X-Proofpoint-Spam-Details: rule=notspam policy=default score=0 mlxlogscore=326 malwarescore=0 phishscore=0 clxscore=1030 bulkscore=0 adultscore=0 suspectscore=0 mlxscore=0 spamscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.12.0-2209130000 definitions=main-2211150155 X-Original-Sender: andrej.bauer@andrej.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@andrej.com header.s=sig1 header.b="FGgb/63q"; spf=pass (google.com: domain of andrej.bauer@andrej.com designates 17.57.155.22 as permitted sender) smtp.mailfrom=andrej.bauer@andrej.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: , > Does this also include the structural rules of type theory such as the s= ubstitution and weakening rules? I would just like to point out that substutition and weakening typically ar= e not part of the rules. They are shown to be admissible. In this spirit, t= he question should have been: what is the precise version of substitution a= nd weakening (which is a special case of substitution) that is admissible i= n cohesive type theory? With kind regards, Andrej --=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/D66F4584-A005-4F69-8E75-E976E0FF9957%40andrej.com.