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 26701 invoked from network); 18 Nov 2022 16:59:44 -0000 Received: from mail-wm1-x339.google.com (2a00:1450:4864:20::339) by inbox.vuxu.org with ESMTPUTF8; 18 Nov 2022 16:59:44 -0000 Received: by mail-wm1-x339.google.com with SMTP id 1-20020a05600c028100b003cf7833293csf4734319wmk.3 for ; Fri, 18 Nov 2022 08:59:44 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1668790784; cv=pass; d=google.com; s=arc-20160816; b=ADQQv71BVJ8vQbVSJcbqy1+iXNKq01pa2nkH8JAVMjt3lq1R7yGBovfoncNF3mJWYi smM1kl0rPdU9e4OtG0oIg4dbT6F4WiLGjBR7WsbuHQHdGLWSRLO/U/mHPSQoSe6Ef3qi lpP9pKEjzxypSdkvuCLLVeQUJ2UD8F2Zlfx/yqWCng7bcDbfom5jSivi5XDpBifZFhZE BXzCrF8ii1Eu38iD4gZqLiyTN7umVUPR/rY3mX8Dr3AsDxkZlGea0xzHGEN0g4TquAOH 1/B3OQ94oP/SJAAaHuKIZ8VkkNXo4OgKlvq15Z6epc6oWFaDFXvPyYjpglTzHFmNMwgS KoMg== 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:content-transfer-encoding :mime-version:references:in-reply-to:message-id:date:subject:cc:to :from:feedback-id:sender:dkim-signature; bh=WyLGny9sPjx1DnnCHtPWjfSevClV+Hriv1OmbCIiqdI=; b=zvMyC+XHXvrBHHM0r75RSaqSHflwHeYgzlG7b6/hx+/69E1qtk9LinBskV/rKvEL4B JMDlsBb2d/f2kf3fMF+zgqLGQllqnMr3jDJw//6Fo77O/+3xsBQEHUzRjGOdlXgKiHxh cZbKNa3V1CllO0UCNwMXqZThDx2VY6romxCEznbfQ9AUKwTz0qfnMXXJkQgklNXNCD9b futDsoyEiQY1rdOjnI1eIaSxP7Qz27JOM6COts0C1CBkHtJHvWwNoQzZ3AO9MALLMxnv d2/nu2gxxFvFW4L5ioeLMWDIefnsTkcVjyTZXTUmAYKHJEZDBV5N9U1K51ujlq2msM2E LYcQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm2 header.b=axKVvlqu; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=mdlriypy; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.25 as permitted sender) smtp.mailfrom=jon@jonmsterling.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:content-transfer-encoding:mime-version:references :in-reply-to:message-id:date:subject:cc:to:from:feedback-id:sender :from:to:cc:subject:date:message-id:reply-to; bh=WyLGny9sPjx1DnnCHtPWjfSevClV+Hriv1OmbCIiqdI=; b=el9JS6qTOJBDTzoDWm84dhOc2LKng5S9W0esAZVCBr5q3FDnxuR6gSYvdfj61UaHox AoOnfi7U1mo7/myaoTaAE3oxr/0Ovrr9H7xrtJOVbEiOdxywjUy7b0nHdljvDF0v/qyM eeFtP2WK9q3VNaHBNxl1XU0AYQHxyhIUjENIGdnvpuFt+N7fhh/2/9T6c4B10JNxhNB3 bfNi7bevBL+EiASj+qvLCNqaonrt3k4jeHbIJ/nDvklNoG2eNi1hu6UcSB+l1wXEOIxL 4non4Fbfie8uKIHMqlDMqdva9aLi7a5C1bFbrAJZec10PkQyo9zD94vake6Esuu64ePH qj4Q== 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 :content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:feedback-id:x-gm-message-state :sender:from:to:cc:subject:date:message-id:reply-to; bh=WyLGny9sPjx1DnnCHtPWjfSevClV+Hriv1OmbCIiqdI=; b=8FxjEYu1YBdP3zxkQg0EeLbjLWLLyZGVvTqFn5lLCETs3LVeoVm/8dZHIcVz4V0G7x 7NL5+7qxbsx8sFequJqDKLES3ECE4vj6VMds0xwg7zq/GuLvoBPwLMOrbe3tS3mcxufY pB+w1c9DZIdaaRWl8gxDtTYTdUZLDf1LB9zydyGzEZkrbSKkGDhWIV7dLeKFGRTRQTQV i9rmGKClV8VaNsX9C4JCB5dtoX9lVq57e9MspQwSUn+AGR+pv8RDGCpaBeJ2Gyi6QtOU EvzYOurUzdVi25udf2o64L2yGy70R6oRIyu4OFf94mYMr1qKilIcHHgKxGYy7ZkADgO+ g6jQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5pn6R5Wnuk2jQQ++Dpko6N20bc7eWFW9qT5JLXWLvXc5VC3lhoNU J+YZrI4EimNU+Hut44gDDcE= X-Google-Smtp-Source: AA0mqf6z4V8RJnjiyTSRVq1dh8nd5c6gUVapHLTk33XvqbvRnNn/kpCJCl5b79yexnzxWIcSwYYYSw== X-Received: by 2002:a05:600c:4891:b0:3cf:d367:2765 with SMTP id j17-20020a05600c489100b003cfd3672765mr9200089wmp.12.1668790783780; Fri, 18 Nov 2022 08:59:43 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6000:1f9a:b0:225:6559:3374 with SMTP id bw26-20020a0560001f9a00b0022565593374ls5994247wrb.2.-pod-prod-gmail; Fri, 18 Nov 2022 08:59:41 -0800 (PST) X-Received: by 2002:adf:f2c8:0:b0:236:4ba1:fb2c with SMTP id d8-20020adff2c8000000b002364ba1fb2cmr5040765wrp.431.1668790781677; Fri, 18 Nov 2022 08:59:41 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1668790781; cv=none; d=google.com; s=arc-20160816; b=Uau1JXoTeGzgaK6CaFOh9OXwLq875I0l6+ic/8TEEP2RTsbvYR5wNKMTxpWtMN+/Q3 bTDM3IGroMiXu9fdvWVMGBtTDebNP9rjr+E6IOSeVWKfiQrqdFPs+cNW/CfwinRb679z 1ARVmAM0W/C3ofK2yZ0l/ZyIF7HgrRQ6PG86yaCqocdRefY9ez4hcsBxzIncgrPOLOtd mwaSXEsLgN5yjwPA6A+tbRFTNh5cP/ohaGpENYhMG9Ruzc0djr6fjk58H2z39JZweYAx tbazQ553cKCfuoHCdWe1sDRuOEgoykY5DTMEjO9lRgljkI0zT1/o3LD4FR0+WicDKXCT NihA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:feedback-id:dkim-signature :dkim-signature; bh=3Qk7f+HgyCrGehS8g2CKK6dqP7kVY6QrRnyE7jN20zk=; b=MvVmPAOzsBod+raJFDv3G4zS5J1LgvGF7g9Mj75FaYAgqV+nq/LdQCzJolOU9kZXfL rkc10H5iRuE8DaBS3oNHZ5TAmPPxWKKZx5zEGCbSjXlrChkK87zOBIDpeT/W8cuIP9Ai r0dPjfPR8QK4DF3k6wF8zIFj7OkDmKC8Vka1mEQ2xhjhqUAkGH+bWUL4ugj85Tr2IjBi 8H2+qJaRMn5li+VT4xcpnFhGgr4HVd7nsayOc5x4OpbrtWG1zEng0mFtYp4JainFK0FG LiUfVcaXh/Ve4cmrTSC2YPw3Md0EDFQijZ91tvD1ZzabMVZGRHJxnGSnql0gsUlbk3Ws oPhw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm2 header.b=axKVvlqu; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=mdlriypy; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.25 as permitted sender) smtp.mailfrom=jon@jonmsterling.com Received: from wout2-smtp.messagingengine.com (wout2-smtp.messagingengine.com. [64.147.123.25]) by gmr-mx.google.com with ESMTPS id p36-20020a05600c1da400b003c9a5e8adc5si361988wms.1.2022.11.18.08.59.41 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 18 Nov 2022 08:59:41 -0800 (PST) Received-SPF: pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.25 as permitted sender) client-ip=64.147.123.25; Received: from compute3.internal (compute3.nyi.internal [10.202.2.43]) by mailout.west.internal (Postfix) with ESMTP id 491B8320095F; Fri, 18 Nov 2022 11:59:39 -0500 (EST) Received: from mailfrontend2 ([10.202.2.163]) by compute3.internal (MEProxy); Fri, 18 Nov 2022 11:59:39 -0500 X-ME-Sender: X-ME-Received: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedvgedrhedtgdeliecutefuodetggdotefrodftvf curfhrohhfihhlvgemucfhrghsthforghilhdpqfgfvfdpuffrtefokffrpgfnqfghnecu uegrihhlohhuthemuceftddtnecusecvtfgvtghiphhivghnthhsucdlqddutddtmdenuc fjughrpefhvfevufffoffkjghfgggtgfesthhqmhdtredttdenucfhrhhomheplfhonhcu ufhtvghrlhhinhhguceojhhonhesjhhonhhmshhtvghrlhhinhhgrdgtohhmqeenucggtf frrghtthgvrhhnpeetueegieeuvdehvdegtefhieeljeelveeuueeljeffgfegtedviefg geduieelueenucevlhhushhtvghrufhiiigvpedtnecurfgrrhgrmhepmhgrihhlfhhroh hmpehjohhnsehjohhnmhhsthgvrhhlihhnghdrtghomh X-ME-Proxy: Feedback-ID: if544409e:Fastmail Received: by mail.messagingengine.com (Postfix) with ESMTPA; Fri, 18 Nov 2022 11:59:38 -0500 (EST) From: Jon Sterling To: Michael Shulman Cc: Thorsten Altenkirch , "andrej.bauer" , Homotopy Type Theory Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory Date: Fri, 18 Nov 2022 11:59:37 -0500 X-Mailer: MailMate (1.14r5895) Message-ID: <92CA5128-A764-47EA-8ECD-B6931F7EA7AF@jonmsterling.com> In-Reply-To: References: <96f15467-49c9-43cc-8868-40b1bdf2162dn@googlegroups.com> <41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF@jonmsterling.com> <9B3B568C-452A-4919-A149-CF7C1E91CDAE@jonmsterling.com> <21B50B02-4107-4854-8015-99EA4B14EBA5@jonmsterling.com> <19FCB983-3890-4113-9DD6-A76C2AFD8268@jonmsterling.com> MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: jon@jonmsterling.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm2 header.b=axKVvlqu; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=mdlriypy; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.25 as permitted sender) smtp.mailfrom=jon@jonmsterling.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: , On 18 Nov 2022, at 11:56, Michael Shulman wrote: > Thanks. It does sound like we mostly agree. I would probably argue that > even for type theories in development, where we don't yet know that full > definitional equality is decidable -- or intrinsically ill-behaved type > theories like Lean, or Agda with non-confluent rewrite rules, where > definitional equality *isn't* decidable -- there is still value in being > able to reduce just substitutions. But I think that's a relatively minor > point. > > Maybe we can work out some way to use words so that this underlying > agreement is evident. For instance, can we find a third word to use > alongside "admissible" and "derivable" to refer to operations/equalities > like substitution and its theory, which hold in all reasonable models, an= d > can be made admissible in some presentations, but more importantly can be > eliminated in an equality-checking algorithm? > Cool, it's a relief to start getting this cleared up! I really agree with y= ou that there is a need for terminology to describe the situation you menti= on, and maybe even more, there is a need to define this phenomenon... I wonder if we can think of more concrete examples of this. For instance, i= n many versions of syntax (like bidirectional ones) we can choose to drop c= ertain annotations because they will be available as part of the flow of in= formation in the elaboration algorithm. Would these be an example of the ph= enomenon you are describing, or is it something different? Best, Jon --=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/92CA5128-A764-47EA-8ECD-B6931F7EA7AF%40jonmsterling.com.