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 21653 invoked from network); 18 Nov 2022 16:16:41 -0000 Received: from mail-yw1-x1138.google.com (2607:f8b0:4864:20::1138) by inbox.vuxu.org with ESMTPUTF8; 18 Nov 2022 16:16:41 -0000 Received: by mail-yw1-x1138.google.com with SMTP id 00721157ae682-367f94b9b16sf53314537b3.11 for ; Fri, 18 Nov 2022 08:16:41 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1668788200; cv=pass; d=google.com; s=arc-20160816; b=sYiTwiqqC0276XBMmQvDPe/R1sxpFXLJ9HddcnLTViXkyz6cczsY6MpjowuCpW/uCC fo1OIALupb0oyOSIGv/ht9mOfQ2QvK8mP7jF3XIfZNJmBwmE3/7ROhmzZOuf6knFNFTd CGd0UZgDsYok56Ytro1Zfzc0DA34AnGQ/wV5xC2gtXcUgEqO6q/2Vv/oiB3Jzq9kbwy7 v+vm2ZT+L13KhM/lCig2kGz4yERPwYLKSp3tDo5B8ToeM5/Gggoh6cTdc2TzLdeaQStZ /c4j26FZQJo7VL+iVAQtnNrhcmTkavRXtzSoPdFnGz2nD3RAHPbKbwnvhW/nt9MlrB0P CT9A== 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=hu08FXPWr1pDyK224RXmFpHZ+afVjIfZXt0mryaF9Pc=; b=PqHCmQSrRzkIebspeNtGNlUId+TI3C+pWR9EWKYaK7syiSZRhxQn/lPr4Xqnf3bvYJ I6njyTuU9fkiHGV/fBu0Qe3LxiBcJBddWvESAVY+JcTnX/n2JXLt0798rzdTLnIc1nej 2nDj+8/TM+u6qPOE8SWBmNlN1r9YCAMqffkwTPmKgZVGwPOY3Z5tkbIl1hd8gOY50J7E j13QU5fl/PmmyMppi8lMF2u6Qz6EDqT+D6QZFMNGybbyco7tYNJLsEo5SWTxkGJvoYCP qkqJoplOIy0CQJd3ODHyDNuHb3Rh47hDjgoHa2a19e0yOmWix0vpTdW7hOo0UOB0Rski XqjA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=JbFIWyvC; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::1131 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=hu08FXPWr1pDyK224RXmFpHZ+afVjIfZXt0mryaF9Pc=; b=HBGc7nxXJMjPJWb5kPM4XWJLWQOZAJlRZg59p0elKKA7HLsOW5FDqgRYdxxNBLmR7K tkH4Q7pVPfCP+EFtbloUdQU2NNinPrtRdM4Vs+BLigqDL5oodyi4sPDleaabu25t1nQQ W9RhQbFmgvkYrbSnKoc2RMIjO7XvcaCJ7fhG7zaA6BKeIhL9ASG33jyRkyn+gPhTA7VO Mu8/dIU+IA4qfla5N+LiOtSy8+MqXzWFt3L37uUV6dIu6i9boh61jgP0ulUb50spvev/ mciCrBJaxxmqfO0Q6IammoXQJ6adpgi8udqIWOn51mtP1Ve7j9fSbdiSHtKfrZ5TMyoz 7N6Q== 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=hu08FXPWr1pDyK224RXmFpHZ+afVjIfZXt0mryaF9Pc=; b=CwA12kqBRGMsVr0WNSsl4JrXLFFPJvg4z706SciRFrlZn5NZpq5ZHW5hf2XVZuUJgt j7sMAp0WROMqEVdaJ9jQL5lQG535AF4M2mxLDV727rtviyR2Js09eNxPzZRWpI+LrTA1 KmrmHNK5hIXp8myl2kiC15Qk+D04N3Jd8xhjodRvoKctkadtyXniKNunHB26K6HDPimk qF0k9eEMzliUYrwiiS/CYT+GJXnHPKu/NFSsuvaMt0E/J64sbPqxZo6WH4u8p0Y4XGq0 pea+dvkY0BSWxf9XpX0uAuhcRP2nQqVj2T63m2JmFLWHfSQ5I7rME8LA7UExFpWP2S7U I3DA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5pmWQfxV4gK7/4cgz2jo5KpvJx8YQ3wLPuWdNqgaJR9LhHfPQXQy H+b4LsF+LFHGl1MGz76GrbM= X-Google-Smtp-Source: AA0mqf6ZH6O2GdjsdjWniO+F/J+9YGyzYnPDPuph/pTEq7pbQNmv9GweGsTJfoDAhHSdZEfDmIikdQ== X-Received: by 2002:a0d:ddcd:0:b0:378:a018:4b04 with SMTP id g196-20020a0dddcd000000b00378a0184b04mr7094325ywe.186.1668788200587; Fri, 18 Nov 2022 08:16:40 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:e53:0:b0:360:d89f:2b52 with SMTP id 80-20020a810e53000000b00360d89f2b52ls2605058ywo.2.-pod-prod-gmail; Fri, 18 Nov 2022 08:16:39 -0800 (PST) X-Received: by 2002:a81:5cd4:0:b0:368:963d:c74c with SMTP id q203-20020a815cd4000000b00368963dc74cmr7448467ywb.84.1668788199030; Fri, 18 Nov 2022 08:16:39 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1668788199; cv=none; d=google.com; s=arc-20160816; b=gL5dWxG/BGO0wRm/mexcrj8cSanvD5Tc1q8j/IdDZlTd37jFXE79mRxMOdIrHYaq4V 2DSN5zSlvV5lc9SPUdHfdlLzJgORTqfK71QvdtpsYOW24yLLog5m7en5rXtdeNedgqAD s1ccNUnGMNx/yWFyDDanNJP2YhT1C3GB4PnmhMV2mZ9egyvtro9OXWzLgTg05Yca0cGz o72ULv4aRmdoN9CaH502q2hmvPHdqrnEVqY1zDGJFGqSraPTbUaUlHEpc1uqldnC0GtA 7mGmGp6XNwa/QpKYYbB/P8a2d/+pD4X5dd2NiygdCuLi35M8Ucp8hokNy3mNqYCsUxrV IFgg== 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=DpbdpBOC+rN/qbtBwc2ZOr0Ug8TjuIFfq0xpXeSCWOA=; b=lWjY+deD3NsQkbT9tsg3XOiVVk51LJzqlvPyRjeXTgmLjtnYL34Woy3ILrmTqhZYlE Al+6i8m1GZwzejpdxL0+br5FW7cVgKavq4O9b5fE0dy2ee9B313QtYBUXWWpgm+e5LFW n1rENXNyypDoRyCHWk1A8PfWEXBteFB0Ow3i5aORdpo9jsU/a/9wCqUQE7p9Wa7WI7f9 eSqjx8dmTuqntYnQAPm+dAO58yNWT5TCS3mvSVbOFpLKsboL/iqEwgeiMf3e5ubZ32qX QbwvyE3b2t7wBNoiFfdr7yczTYdFinoOM+NxTIvBjAI14/b/L51S0rA4JN50zkHUxvlO NKHQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=JbFIWyvC; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::1131 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: from mail-yw1-x1131.google.com (mail-yw1-x1131.google.com. [2607:f8b0:4864:20::1131]) by gmr-mx.google.com with ESMTPS id p128-20020a25d886000000b006d3034c7baesi197706ybg.3.2022.11.18.08.16.39 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 18 Nov 2022 08:16:39 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::1131 as permitted sender) client-ip=2607:f8b0:4864:20::1131; Received: by mail-yw1-x1131.google.com with SMTP id 00721157ae682-3691e040abaso53863547b3.9 for ; Fri, 18 Nov 2022 08:16:39 -0800 (PST) X-Received: by 2002:a81:25d8:0:b0:373:4467:e0c6 with SMTP id l207-20020a8125d8000000b003734467e0c6mr7167795ywl.340.1668788198747; Fri, 18 Nov 2022 08:16:38 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Michael Shulman Date: Fri, 18 Nov 2022 08:16:27 -0800 Message-ID: Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory To: Jon Sterling Cc: Thorsten Altenkirch , "andrej.bauer" , Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000caca6205edc10732" 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=JbFIWyvC; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::1131 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: , --000000000000caca6205edc10732 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Fri, Nov 18, 2022 at 2:59 AM Jon Sterling wrote: > Hi Mike, thanks for your comments =E2=80=94 regarding modal type theory, = please > note that there are state of the art general modal type theories that do > not employ admissible substitution! MTT is one of them. > Split-context modal type theories can also be presented without admissible substitutions. Making substitutions explicit is easy; it's making them admissible that's hard. And as far as I understand it, MTT does satisfy the primary desideratum when making substitutions admissible, namely that all rules have a fully general context in their conclusion. MTT is also not equivalent to split-context theories, and IMHO is less pleasant to work with in practice. I believe there should be some way to combine the ideas of the two theories. By the way, in the followup paper "Modalities and parametric adjoints" by Gratzer, Cavallo, Kavvos, Guatto, and Birkedal (three of whom are also authors of the MTT paper) we read "The admissibility of substitution is a central property of type theory, and indeed of all logic" (section IB). --=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/CADYavpwz_Y61ST5eauZiH1b9E79BF--oroXinvzd2odHsycyjg%40ma= il.gmail.com. --000000000000caca6205edc10732 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Fri, Nov 18, 2022= at 2:59 AM Jon Sterling <jon@jo= nmsterling.com> wrote:
Hi Mike, thanks for your comments =E2=80=94 regarding modal type theory, plea= se=20 note that there are state of the art general modal type theories that do not employ admissible substitution! MTT is one of them.

Split-context modal type theories can also be presented without admissible=20 substitutions.=C2=A0 Making substitutions explicit is easy; it's making= them=20 admissible that's hard.=C2=A0 And as far as I understand it, MTT does s= atisfy the primary desideratum when making substitutions admissible, namely=20 that all rules have a fully general context in their conclusion.
=
MTT is also not equivalent to split-context theories, and IMHO is less=20 pleasant to work with in practice.=C2=A0 I believe there should be some way= =20 to combine the ideas of the two theories.

By=20 the way, in the followup paper "Modalities and parametric adjoints&quo= t; by=20 Gratzer, Cavallo, Kavvos, Guatto, and Birkedal (three of whom are also=20 authors of the MTT paper) we read "The admissibility of substitution i= s a central property of type theory, and indeed of all logic" (section IB= ).

--
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/CADYavpwz_Y61ST5eauZiH1b9E79BF--o= roXinvzd2odHsycyjg%40mail.gmail.com.
--000000000000caca6205edc10732--