From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: <> X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-2.1 required=5.0 tests=DKIMWL_WL_HIGH,DKIM_SIGNED, DKIM_VALID,HTML_MESSAGE,RCVD_IN_DNSWL_NONE,RCVD_IN_MSPIKE_H2, T_SCC_BODY_TEXT_LINE,UNPARSEABLE_RELAY autolearn=ham autolearn_force=no version=3.4.4 Received: from AUS01-SY4-obe.outbound.protection.outlook.com (mail-sy4aus01on2138.outbound.protection.outlook.com [40.107.107.138]) by inbox.vuxu.org (Postfix) with ESMTP id 12181283E4 for ; Mon, 5 Feb 2024 08:30:48 +0100 (CET) ARC-Seal: i=4; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=pass; b=Qf7QY1QtBs1t9Lp5FNgb5xCs55ViDXvAXac3R4Ftv9RcZrYj7nMaFEbue1xo6IVFMnNUbuv/aK45din7WI59RLgRUD91dSmG4Q/UG7wP2QIx6t63Q2pFkYwClqa6gIDgg8WPULE4m1Zm1EzVuFK2fGYNVgm2HMWFicbqKL3BozAGkRXOmCq8bne0CU2T4jryb9yI1zbspUjhE+c21L8NDgN7oLZpBRCdhrpnrS3Vkc9mIRAM4VM2Ng/SkzeeUSrbZfNxr7pNijko2xQ9TDVc5GhiYBYvnBy5PTGpQOR7xFYilZqfEG39PG8reyt3qgl4aGbsBFoxcyA/VM4bw6gV0w== ARC-Message-Signature: i=4; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=7DLAFI85xlAHcV4gyeCwlg1/6ECVo8XXQ3iNyOTnv+M=; b=mR/gYmTrg1vMdL41OVkqSTMfPMhVsj3+4HKi9oX13cGtSKR1Q89dxj9xkTVYWMRuW2KKJg3uPOf/HqWpjJvQ6uhYJGUh7jV1yd31qSW6WlCNy6YY+pdsLC9xzwaGGQwQEGIxsGuC/fflmn0LMQn3+ShnYO4d+cn2daqR84xZCY+8pohxDvFa6FooQkFVa7pd/uEkuTYLEIQWDE+HNlIIHQCkQABKFm1+DtJwxndaRcBra8VMOr8fyiYFK6+BSZH1m87Yal2tz3p4cuavfCcx2ToDRPqI/R2M6deCZinpj1Q2g/h2/cXkdvP012E+Ed0Yb8PC+jaoaan4A23/XQ3f+g== ARC-Authentication-Results: i=4; mx.microsoft.com 1; spf=pass (sender ip is 130.239.40.25) smtp.rcpttodomain=mq.edu.au smtp.mailfrom=cs.umu.se; dmarc=pass (p=none sp=none pct=10) action=none header.from=cs.umu.se; dkim=fail (body hash did not verify) header.d=cs.umu.se; dkim=fail (body hash did not verify) header.d=cs.umu.se; arc=pass (0 oda=0 ltdi=0 93) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=groups.office.net; s=selector1; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=7DLAFI85xlAHcV4gyeCwlg1/6ECVo8XXQ3iNyOTnv+M=; b=cbP2u1ycPRT5F0DhZSl+oVZx7O/OjFu2EcBhSkMg/chCtA+vo3mblgkB0FNJcjztOb4N/hvi82YWNqFwP25WAEhXjkqy7iaQMv1U4WpzYfjR9RcqL8hLltVBL41pjeiBKsqaB9m239Qn9x6VO8TC/RoeWtzj4DQjj8lZ5lMFfF/wMy5SMu6iovDY5zHWZHwbiJeRSBrFv84P3xLAHixuT8nQwnqF9QBPyfNHOzDITpSZ1GfAfKt8AJ/TyF5Y2JzRCdcM9POlzTPATiqb4m7vpQPQiRs+lEUfSvYJdd6vFpcO+GZc4+XjED2OGdbIQybm7GhnBB77eI1TbW6uaZvBLw== Received: from SmtpServer.Submit by SYBPR01MB6064 with Microsoft SMTP Server id 15.20.7249.33; Mon, 5 Feb 2024 07:30:44 +0000 ARC-Seal: i=3; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=pass; b=jWa5x/9rh+Mii9kc9ZAoY2zsqo6R1IocfSyLypOaoxnr9CRn4rRWs8kX8wrXqJnh/gE+7oNBqA8FZbilAQe8Ul8igbNQBMFthm1Ygia6J/h7b0qTyokpAFv+ksjo35/MnSeJGpAGCTqpGvHdWfzJzBxd/rXpdNC/DpD3Vl1iTAnQQ/Ztr7H+RgTLnNnqhnddgERFwdU/VC/isE4nP+0s9/jA7XLity9Vv9PO8UXvX9BTOyhWqxFElVgyUT/fIEjpmPDzZEKoUiZvp6oRN07J5udppv63m2hvt6imPFLFzsID4SlJEMRXXCKhE3XPB4o68hvaCA+03A08YfL+nqLmdw== ARC-Message-Signature: i=3; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=OmcJLBM69jLdQ3Qb7g28tnmAH49r9QTRvlqsoKlSvz4=; b=IdDQQIpkNf67dehjiDHj/90Fbk872pEOtx/Dz/KCeVxI6ekBYGh853ncgtEaqW8/PbDRTxX1uTFPfnAhK8gwhmUhYU9lYDRIHqTa2Yne82i3Rv3QWnhvaSjewFHaoUzUTCaOcQCe7NVzKnEBm0qYH/lkPeodfQAHEXagaOrAV4Kbs00OmexQX0V2XyW4cnJYIgPqNgXQJ0IoBv4UdfdA4FAj6faddJAhYswVLanP4fxFvzurzFruapc+MbhNunMQhccSG7hjnC4+1CK3xXVU0xrpTvgWhVLx5DcnI1eIyu7TACJ8x9gga9uI7YNpnAuSB4AJ/CabBAcFw/Q7W4doSg== ARC-Authentication-Results: i=3; mx.microsoft.com 1; spf=pass (sender ip is 130.239.40.25) smtp.rcpttodomain=mq.edu.au smtp.mailfrom=cs.umu.se; dmarc=pass (p=none sp=none pct=10) action=none header.from=cs.umu.se; dkim=fail (body hash did not verify) header.d=cs.umu.se; dkim=fail (body hash did not verify) header.d=cs.umu.se; arc=pass (0 oda=0 ltdi=0 93) Received: from SYBPR01MB7180.ausprd01.prod.outlook.com (2603:10c6:10:13d::11) by SYBPR01MB6064.ausprd01.prod.outlook.com (2603:10c6:10:97::14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.7249.33; Mon, 5 Feb 2024 07:30:38 +0000 Received: from SYBPR01MB8556.ausprd01.prod.outlook.com (2603:10c6:10:1ab::6) by SYBPR01MB7180.ausprd01.prod.outlook.com (2603:10c6:10:13d::11) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.7249.34; Mon, 5 Feb 2024 07:30:35 +0000 Received: from SYBPR01MB8556.ausprd01.prod.outlook.com ([fe80::4e39:67f9:325f:6487]) by SYBPR01MB8556.ausprd01.prod.outlook.com ([fe80::4e39:67f9:325f:6487%7]) with mapi id 15.20.7249.032; Mon, 5 Feb 2024 07:30:34 +0000 ARC-Seal: i=2; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=pass; b=iF4lb0Jpk0e8jqqNSiNcsUtkH0h/B/CL/KZZ+xwOWFxC2x+vbAAtflh9MRPlF0/OiFuGmIAtqi3kUsor0gddlMd4pjr4BcmodJYPp6hQLpSpsagQ6hd6pvJSmiHp/khZR0o4oIrcKlxWGWIryyoJDZGotRST6kWVwRFjwbU5/Epr4NHIhkJMqu654wjQ09J6bHhPx1CvIMKZLppnMfWAWrpTTgJOlIH6d0vQGHZmaKtzHMB/3Hg0pf9eienrHRdtwTbTRSkQtDrKy0mHNONffUKAILihL6v3rFYdnvN6TRHdfeapw9xuCBsWWyDPh7qHGNz+df4mi1gxlF4LIulwzQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=OmcJLBM69jLdQ3Qb7g28tnmAH49r9QTRvlqsoKlSvz4=; b=JKxoysr6CFLG/ZyBL0M1phz88aTjqzrjZCrBpr2ZDDs6CQDfwM9NT0EMIGREaoYi9Mp2IV2nkUNM5HPCsxUbGPNPGeOMWzxOHIPQzwhE7GTg27YQIH2XS4fzfmv/i8r7VR0fO5KVnA/pnBUDGm1r2IdLumR0S+Sxdnrz9C6qjGUlhjFQUKDvQ7N2nEPdCqFmvedV+qDwqZvaSRRWnXbdSUB8ggNIPwC8QfDakxXx2kiHSjY9LW+xxj0zvW1u+BrEFwzgHxP0fZiNG+lmq78as4c3DQW6u9qj6gFeOVZIyhg8hD/RBsZ8bu1IMCXyeUN0L3DokVppYyWBzsWF1c6T2w== ARC-Authentication-Results: i=2; mx.microsoft.com 1; spf=pass (sender ip is 130.239.40.25) smtp.rcpttodomain=mq.edu.au smtp.mailfrom=cs.umu.se; dmarc=pass (p=none sp=none pct=10) action=none header.from=cs.umu.se; dkim=fail (body hash did not verify) header.d=cs.umu.se; dkim=fail (body hash did not verify) header.d=cs.umu.se; arc=pass (0 oda=0 ltdi=0 93) Received: from SY0PR01CA0015.ausprd01.prod.outlook.com (2603:10c6:10:1bb::23) by MEWPR01MB8783.ausprd01.prod.outlook.com (2603:10c6:220:1fb::21) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.7249.34; Mon, 5 Feb 2024 06:44:36 +0000 Received: from SY4AUS01FT018.eop-AUS01.prod.protection.outlook.com (2603:10c6:10:1bb:cafe::98) by SY0PR01CA0015.outlook.office365.com (2603:10c6:10:1bb::23) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.7249.34 via Frontend Transport; Mon, 5 Feb 2024 06:44:36 +0000 Authentication-Results: spf=pass (sender IP is 130.239.40.25) smtp.mailfrom=cs.umu.se; dkim=fail (body hash did not verify) header.d=cs.umu.se;dmarc=pass action=none header.from=cs.umu.se; Received-SPF: Pass (protection.outlook.com: domain of cs.umu.se designates 130.239.40.25 as permitted sender) receiver=protection.outlook.com; client-ip=130.239.40.25; helo=mail.cs.umu.se; pr=C Received: from au-smtp-inbound-delivery-1.mimecast.com (103.96.22.101) by SY4AUS01FT018.mail.protection.outlook.com (10.114.156.133) with Microsoft SMTP Server (version=TLS1_3, cipher=TLS_AES_256_GCM_SHA384) id 15.20.7270.17 via Frontend Transport; Mon, 5 Feb 2024 06:44:35 +0000 ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=dkim.mimecast.com; s=201903; t=1707115474; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version:content-type:content-type: in-reply-to:in-reply-to:references:references:dkim-signature; bh=OmcJLBM69jLdQ3Qb7g28tnmAH49r9QTRvlqsoKlSvz4=; b=DpsduCb/h0ZC/iIbYApgbixxPuIqxOy7UNqEOfgZ/fQkHBsBkHZRGDFfP5GXyS1uOmPh9U /23qs+J50DR1iPNroKPCuZmE4njgn9Hq2A/c/9YdOS+wTMRBmF9uQIS6ZZrakbtaIoP83z gVGBOemBF91M3sEkR2j4qIwV9fuyDua17N6c8Z6VB0PVrWU92YHc+28flvMv3w6oyVAfii JR8VDKioPM8mLu8pwd/vQ2scEiCltQQJfo2F4ZgUAPo63ev7himMXZxucfzWIDi9WOyqg6 BDxAdoH7i7QZryTR8RPt45p3Cmqvv1XXTgY7umbBut32U1Q6StduL0KzOSr3+Q== ARC-Seal: i=1; s=201903; d=dkim.mimecast.com; t=1707115474; a=rsa-sha256; cv=none; b=gY3jEJRfIxNggKHR+U+DL90TAgpWmgq/IsV3ayqS4RbHL4Xl7c1J0HNMvYMTV6HVBdodVb P3brlT/rpVePaKtSGiLEILSM6B94uZCktKY0n20NZSaQO5/1dBUrcZr9M8K3Z7rxdZtU/s b17IstOBdqBYu1JyIEzbhzLD1xht/4jktOGeQB1rYVBnP6QUnQoqN1cDd794pwY97q2fMH olDn1dQ4ids8SvXs6+m/htRntT9o2xsY/uh6OTUOk8uxupLFcgX6/veN1EcnD1FoS9n61S 7aK9EMIMbkABIEdecLOryvGL6xEkbAWtpbyt4vJqXGEG3ZjJgxfR9+qHNnKrSQ== ARC-Authentication-Results: i=1; relay.mimecast.com; dkim=fail ("body hash did not verify") header.d=cs.umu.se header.s=dkim header.b=CElKUYqk; dkim=fail ("body hash did not verify") header.d=cs.umu.se header.s=dkim header.b=nVRpdfpN; dmarc=pass (policy=none) header.from=cs.umu.se; spf=pass (relay.mimecast.com: domain of peklund@cs.umu.se designates 130.239.40.25 as permitted sender) smtp.mailfrom=peklund@cs.umu.se Received: from mail.cs.umu.se (mail.cs.umu.se [130.239.40.25]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id au-mta-40-WhF9viZxMaq5R_lZoDSnag-1; Mon, 05 Feb 2024 17:44:29 +1100 X-MC-Unique: WhF9viZxMaq5R_lZoDSnag-1 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cs.umu.se; s=dkim; t=1707115463; bh=q+LenLxPgUMuqCkp22Vd+h0PvH1hnAAZDRLzr1CapAY=; h=Date:From:To:Cc:Subject:In-Reply-To:References:From; b=CElKUYqkNKPuqnb9rykne3YpGoY81uxnzcvgLh5JBqLd07Vx+9cIbRy0Mh+sGfEGk QN4vdI1EnfqL2qdO4lHZ4C1gGkbaqjn6e2JLbUaBi3tsykepK2mfm9Zy69MT2Epz4H 0D521V0BkqjZWkPfAaUrFECD1ZGxxrbTP+OgfxfzBLhpZHDBtvlYdQepvXe0eOboSL 1Y5QoXdSCMmJK2OdMie7EjGT5L6YsvJQft75v5cSvoEPIiqCdW3yilCWXnzoaQgBrv OlezFuvbYN4ZbaznzT78DISUNBAjq0cOuL57OF6+jNQzbpXsfSGsE/UQc6eycz5SG0 y7KKSko40PV2Q== Received: from localhost (localhost [127.0.0.1]) by amavisd-new (Postfix) with ESMTP id 4TSxgW6ZYQz2l; Mon, 5 Feb 2024 07:44:23 +0100 (CET) X-Virus-Scanned: Debian amavis at cs.umu.se Received: from mail.cs.umu.se ([127.0.0.1]) by localhost (mail-vm2.cs.umu.se [127.0.0.1]) (amavis, port 10024) with LMTP id BowmuRbtsrRC; Mon, 5 Feb 2024 07:44:22 +0100 (CET) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cs.umu.se; s=dkim; t=1707115462; bh=q+LenLxPgUMuqCkp22Vd+h0PvH1hnAAZDRLzr1CapAY=; h=Date:From:To:Cc:Subject:In-Reply-To:References:From; b=nVRpdfpNtA6wtYSt5QhgL3znSbBgCUQi1gFpQGbhR8YqcOGsFEeBqjsL2HOyRZg08 P91enVOLgFJb4+/Wl9r2ycJ4kZyB0EarGgzuVluwtWVY5IuNA8n60iQZfq+Ww47lHd ZCVjvw8uX4qs39I/kpCPOwpmYl+y3bgq/8Q2QsSSKoJbXhJUYj7jMS/gPRS6IEgUlm /zPg2OKmuPgLcLRDLNQq5sP1wh/DqGhkc2yVxI6PHYRcwkm/AeB+Co4kZt9Xvgv2hv O9f4IwA0veeD9DEzLOXTX/bCV92dx2nGaINmlWtSAHrBnpMJzVDl9xP9wEr9Caf3q3 9XCZoQxfqHDyw== Received: from webmail.cs.umu.se (webmail-vm.cs.umu.se [IPv6:2001:6b0:e:4040::68]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (No client certificate requested) (Authenticated sender: peklund) by mail.cs.umu.se (Postfix) with ESMTPSA id 4TSxgT58gWz2k; Mon, 5 Feb 2024 07:44:21 +0100 (CET) Received: from VVMMkYRd7qKXn5DPMvW5ll1/lWiihQ8ZRhI3D2QrJws= (XJg0xUpUJ17IYnIBw9cvorWZsIxzBz2/) by webmail.cs.umu.se with HTTP (HTTP/1.1 POST); Mon, 05 Feb 2024 07:44:21 +0100 MIME-Version: 1.0 Date: Mon, 05 Feb 2024 08:44:21 +0200 From: Patrik Eklund To: Jonas Frey CC: David Yetter , categories@mq.edu.au Subject: Re: Monadicity questions In-Reply-To: References: Message-ID: <9e9cb7c9a56b7b0c01ea26ca622f8553@cs.umu.se> X-Sender: peklund@cs.umu.se Authentication-Results-Original: relay.mimecast.com; dkim=fail ("body hash did not verify") header.d=cs.umu.se header.s=dkim header.b=CElKUYqk; dkim=fail ("body hash did not verify") header.d=cs.umu.se header.s=dkim header.b=nVRpdfpN; dmarc=pass (policy=none) header.from=cs.umu.se; spf=pass (relay.mimecast.com: domain of peklund@cs.umu.se designates 130.239.40.25 as permitted sender) smtp.mailfrom=peklund@cs.umu.se X-Mimecast-Spam-Score: 0 X-Mimecast-Impersonation-Protect: Policy=MQ - Tag Header Only on Default Settings;Similar Internal Domain=false;Similar Monitored External Domain=false;Custom External Domain=false;Mimecast External Domain=false;Newly Observed Domain=false;Internal User Name=false;Custom Display Name List=false;Reply-to Address Mismatch=false;Targeted Threat Dictionary=false;Mimecast Threat Dictionary=false;Custom Threat Dictionary=false Content-Type: multipart/alternative; boundary="=_321b50fca6038d45142e1fbbe8004832" X-EOPAttributedMessage: 0 X-EOPTenantAttributedMessage: 82c514c1-a717-4087-be06-d40d2070ad52:0 X-MS-Exchange-SkipListedInternetSender: ip=[130.239.40.25];domain=mail.cs.umu.se X-MS-Exchange-ExternalOriginalInternetSender: ip=[130.239.40.25];domain=mail.cs.umu.se X-MS-PublicTrafficType: Email X-MS-TrafficTypeDiagnostic: SY4AUS01FT018:EE_|MEWPR01MB8783:EE_|SYBPR01MB7180:EE_|SYBPR01MB6064:EE_ X-MS-Office365-Filtering-Correlation-Id: 87546722-8b4a-4644-69ba-08dc2615eaa9 X-Moderation-Data: 2/5/2024 7:30:32 AM X-LD-Processed: 82c514c1-a717-4087-be06-d40d2070ad52,ExtAddr,ExtAddr X-MS-Exchange-AtpMessageProperties: SA X-MS-Exchange-SenderADCheck: 0 X-MS-Exchange-AntiSpam-Relay: 0 X-Microsoft-Antispam: BCL:0; X-Microsoft-Antispam-Message-Info: P06pwclVGFwHCE1xedT+/bBipYr3simvtLv3SZfWwrw9ycbaaGQabuRAmkloijRd+HvBnC+Jpuxl+OId1RqOGpjCQG0wfbKqgGZXz9MGtQBv+HiTxijjq9oBSMHqSq/Ty7vtBQHJ7UzlNIVZrYneaQr13fWxv+F8tAA7+nGZU2gCNcivD1nYwXr5bc052oyZqvsBP7gtnzmNG9cAD1f/iLNxCpKSNdCJFZ+2TqlOv09XY29u1Ick8TYbstITTAb0fZVzs1TNwOy8zUYzXqJvLkv+yGxdR99RZXs8eMH3c16yj9bt7zH+DwNVktPiBoL24+kbtMJXtYRzr9PmtC4l7Wuz/TZLzZ5U/+gFe36h/BgI717uy7hjnMQy25NBFVYZfAiiU7hFFcBTEPxDf48JdxQ0zwv9KQ/OUqDus/uRGJ7QvzzohkFWSlmtOWcSRnkddrD7s4ilNLz8ivJHVdjMrue87As2972+z0RMKXXBmKcSYVQ12a4Ej9CUNPqDGlpgCOE9x8PZ5SKfHV4QrRS1RKuYxbFL2m63phOnP9916PD+mAjiFr3ub7mHCJSCSMaHse5aMFlg0H0YJdwtxRCyItFM7WNh3hYIHlDt0uopX7MfgUX3sN7yDDaQ03HkChW8Z3sxpbFH9fyXuelKhYHJc+mPvD2cEnre+Uq5FtBtzVSeR7VGM2g8nLO2uYhE9KiUAtPh0RdumfTjXwEtmSoPR9I7jD7ChzQ6gLe9+4swHG1FeJfcKykIft9nCuu2NuCcuFdtP6oZ5HqszrPofhB9hdOGel6gEPwZjzIwn+Kv7tWMlEf/KvbK3HimPJjDbzU9FnZE7OS1G/huxsSo+xYYm5zUl7bkNi6Oxak1zGFTnY4= X-Forefront-Antispam-Report: CIP:103.96.22.101;CTRY:SE;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:mail.cs.umu.se;PTR:mail.cs.umu.se;CAT:NONE;SFS:(13230031)(4636009)(346002)(396003)(39860400002)(136003)(376002)(1800799012)(451199024)(8000799017)(82310400011)(64100799003)(48200799006)(40470700004)(3480700007)(32650700002)(2616005)(26005)(83380400001)(336012)(426003)(35950700001)(166002)(7596003)(82740400003)(66574015)(8676002)(6916009)(316002)(8936002)(7276002)(156005)(7406005)(32850700003)(786003)(68406010)(70586007)(4326008)(7366002)(7416002)(5660300002)(7336002)(2906002)(30864003)(7116003)(33964004)(53546011)(108616005)(498600001)(89122003)(88732003)(966005)(45080400002)(76576003)(24736004)(86362001)(36756003)(41300700001)(66899024)(40480700001)(40460700003)(41080700001);DIR:OUT;SFP:1102; X-Auto-Response-Suppress: DR, RN, NRN, OOF, AutoReply X-MS-Exchange-CrossTenant-Network-Message-Id: 87546722-8b4a-4644-69ba-08dc2615eaa9 X-MS-Exchange-CrossTenant-Id: 82c514c1-a717-4087-be06-d40d2070ad52 X-MS-Exchange-CrossTenant-AuthSource: SY4AUS01FT018.eop-AUS01.prod.protection.outlook.com X-MS-Exchange-CrossTenant-AuthAs: Anonymous X-MS-Exchange-CrossTenant-FromEntityHeader: Internet X-MS-Exchange-CrossTenant-OriginalArrivalTime: 05 Feb 2024 07:30:34.9330 (UTC) X-MS-Exchange-CrossTenant-MailboxType: HOSTED X-MS-Exchange-CrossTenant-UserPrincipalName: wuseWZJs8WCvaZ4Olqu/Mpya6ja2Z6o5gvuW8QxZj2m3/anQcb/Zle7TizXzMeRhe3CkT6WF4gcWpQuTSRWb1zeMNl1cz1ZssvQD/xPWg7L9RDJTtNGk8NXAWnojtwFiLSlLuRtd8iOpoOYZsF36GjTf+cf7alYDUYOo+tQ8UXYuABe5fMobqVFXtncGTHto X-MS-Exchange-Transport-CrossTenantHeadersStamped: SYBPR01MB6064 X-MS-Exchange-UnifiedGroup-DisplayName: Categories mailing list X-MS-Exchange-UnifiedGroup-Address: categories@mq.edu.au X-MS-Exchange-UnifiedGroup-MailboxGuid: 9c2f954e-92a7-451b-b723-a07075d7adb5 X-MS-Exchange-UnifiedGroup-CustomizedMessage: RedeemedBusinessGuests X-MS-Exchange-Parent-Message-Id: <9e9cb7c9a56b7b0c01ea26ca622f8553@cs.umu.se> Auto-Submitted: auto-generated X-MS-Exchange-Generated-Message-Source: Throttled Fork Delivery Agent X-MS-Exchange-AntiSpam-MessageData-ChunkCount: 1 X-MS-Exchange-AntiSpam-MessageData-0: =?utf-8?B?U1E2MzJjMXgrdGRyK25mTnBBSWFTa09XdmREMysvTlNWb1BTYlV2ek1FYms0?= =?utf-8?B?OG1HMXlMaEFQZHMvQmpTUTVyeFBvd1IwdmEwNmhUbG5rNEZ0U1cvTEZrL2NV?= =?utf-8?B?UHpxajdESHh2RFA3N3Q0cll6QktyQXNrVkpqN0cxTlltZ3NwV2c5Wi9GOGNX?= =?utf-8?B?YTdPbHl1YzhpY3ZySnNKN3E4WkpYOHB2akhCKzlXTm02Q2RFYXJaTXIyUnNw?= =?utf-8?B?TU5XNGRzbG1ZaHBtZlFNRlNuOVZGOHQzRHV6WFlXLytTK0NrZHVaQ3p2YXJL?= =?utf-8?B?T3lxa0U4OHgyQTFMcEswQWJneHVYOE5aU2pscDlGMk9jWndkdk40d00yYnRK?= =?utf-8?B?czVQU0M2WVpIR3htZGpkbWZSNGdKMmZscHpIQ1NmRjlRMlpkaFZ6dU1FeU9x?= =?utf-8?B?QWxxdXpwNE1JSXNLbCsvekQ2dVA2OUE1ZzlobU9aVW9DUGVGd3dKdFlReXEy?= =?utf-8?B?R2crcGxPbjFMZzlndjR2RWVrbmJyS09pR2FDM3pjdU9uZmhCMmwyNHA4WlVZ?= =?utf-8?B?ZmcxaXVjMFBDRENzWXJpVmtsUlZZVEFuanJjRjdjMDdnLzBTY0IvVXNENG9o?= =?utf-8?B?bkZDZE0xZFZtYnI2RmlaMzU1MmhVbnZ4SFMvaDhGb1dkanFKNmUwSk82TmlZ?= =?utf-8?B?MmVQNGJzaTVXOUlWMVVZSEM2Yk16UDR5WTRBdlIwYi8wTEs0WVdTUFJaSEFT?= =?utf-8?B?NlUzODdCaXV4RFRQYTMyUUFoWlNsZHVZTzYwTW9RaDhXeGVNbXNBN3h6enBY?= =?utf-8?B?d01HU2VDYUExY0Q1MGRjVzZhc2NPeWFLOGNzeHQzVGlMWHhkUnlZOERvdHl5?= =?utf-8?B?bG1yVmV6WjZSdk03dUs1b25UYVhRKzVZQzBpdm5lcUduUDdPQ2hMYnRGQlNh?= =?utf-8?B?Qk0yMzVZUGJrUWM3VU91cFBIWGlQbjArVXBqZUJ6V085MTdRU1Y0LzNKMmJa?= =?utf-8?B?Zkp5REpqQVJUU0M0NzZqcm16ZyttYmlYdy8xd2dRamtrRTJoYVJHQ3k1Mm9X?= =?utf-8?B?NHZPVG95OFl4RTBCUlN3dTRIZkpnZkQwMm9IU01kSWp6eW9JRUx5cUVQRllj?= =?utf-8?B?K0x6WUZNUG1ZZVBNVXdLR3BHb1RqdGEyUUlrdVZ1ekg2U2ZsbFFDUVQ0cUZp?= =?utf-8?B?OGtYUThKcGdNMTNRekdRenByUEFQRFdOOUNwaVdiL2ZHK1QvTUx6bUZ1MFJj?= =?utf-8?B?Qjd2Vjd6QlEyWmdqbVhCdnFqUG1jY2Y3cmExTW5NWnVkclBML3J2WFhQcjhz?= =?utf-8?B?cEV4dFN5MmVUZG9pRnFCQlByVEhZeVFzdWJHb3NvR2dCaFhtckgwS3EyVDN4?= =?utf-8?B?anNqdHVQOTh4aE9iU25RNU1pKzVxNUVCY1JkWFJsNVBydFVDUG40Y1dKME5s?= =?utf-8?B?dGd2WEluUlEyR0htQzVBRGtXNFhjdUFSSXpiZmR6QlFZMS9WS3RMbGsvSnN1?= =?utf-8?B?U1lmWUQ3cW1FUDgrYU4rc1NCWkxnR29kUkpzN2tmUVcrVHdlYXRkZmRQblYr?= =?utf-8?B?Visvdyt4eHNkQkxnZUE1UUQwZ3UyUTVRakR2c3JLRHpKUjdqaUNLZ3BxYWVF?= =?utf-8?B?NU51elgrYWEwdkMzbkZLT3ZFMGJqMHZSVDhIQ2ZtTFZOaHFldURVUG1CaTVQ?= =?utf-8?B?OHgwckxXWVF6VldpaFJJM3ZxV0s4cTdLV3lJV29qajlRaHVYRi94TGpNNnU0?= =?utf-8?B?Q1pIVEFXQk5hODhra3Y3cXF1ZFhvVnQ4bjh0VERFNUpCbHZUekpoUVpoeXhI?= =?utf-8?B?Q1NlL0ZSd0tvQmZId21VYkZ1enR0Si9vc3pXN09CNEl6ZU52SDZZMlp0YjRz?= =?utf-8?B?YUxYeHp1WkhONStETFUya3JwMU1JWUp6OVBsb0w3cklDU3hwb3g4bUdmYXdw?= =?utf-8?B?aHErTFdVZUo3TDZNN1FpZ3h0MGJDSzE5Y01Jdm9IK0lLa3ZkME1uMHpGeFZK?= =?utf-8?Q?Ct/WnWhjp50CLdhcvxTdqctq2770IFJC?= X-OriginatorOrg: mq.edu.au --=_321b50fca6038d45142e1fbbe8004832 Content-Type: text/plain; charset="utf-8"; format=flowed Content-Transfer-Encoding: quoted-printable These may provide some added ingredients: https://www.sciencedirect.com/science/article/pii/S0165011413000997 https://www.sciencedirect.com/science/article/pii/S0165011415003152?via%3Di= hub https://link.springer.com/book/10.1007/978-3-319-78948-4 The focus here is on (multi-sorted) term constructions and more generally o= ver monoidal closed categories. Other papers we've written build upon these= where term constructions are used in sentence (formula) constructions. Not clear to me what David precisely means by "no new", but in our case we = have been used to say "logic must be lative" in the sense that "first terms= , then sentences from terms" and no new terms from that, and "then entailme= nt constructions from sentences" so that no new sentences are constructed f= rom entailment. Here is where logic mixes "true" and "provable", and this i= s the very spot which allows G=C3=B6del to "prove" incompleteness using the= Liar and Richard's technique. Respecting this principle of lativity, G=C3=B6del's 1931 results are basica= lly non-sense. Grundlagen II =C2=A74-5 tries to deal with it, with some suc= cess, but not fully as GdM amd other work at that time, not just in G=C3=B6= ttingen, never properly dealt with the underlying multi-sortedness with sub= sequent term and sentence constructions. Maybe it's Russell's fault? Princi= pia said Peano had suggested that logic must be freed from algebra. Peano n= ever said that, but Principia did it, so "formula constructions" remained a= s a, as Peano said, "putting symbols one by one in sequence". That's not a= monadic approach to forming terms and sentences, is it? My point is this: Category could have been around already before 1917, as t= he set theory used in category theory basically is the set theory that was = available before Hilbert invited Bernays to G=C3=B6ttingen. Had they used c= ategories for foundations, G=C3=B6del's 1931 paper would probably never hav= e been written. I have always wondered what G=C3=B6del means by "isomorphic= image" (in his footnote 9) in his 1931 paper. Patrik On 2024-02-05 06:21, Jonas Frey wrote: Dear David, Yes, models of single-sorted algebraic theories are always monadic over Set= , and such theories correspond precisely to finitary, ie omega-filtered-col= imit-preserving monads on Set. If we take the correspondence between single= -sorted algebraic theories and Lawvere theories for granted, this is stated= eg in Hyland--Power [1], with further references there. More generally, mo= nads preserving alpha-filtered colimits for a higher regular cardinal alpha= correspond to algebraic theories with alpha-ary operations; unbounded mona= ds (such as the powerset monad) can be viewed as corresponding to "large th= eories" with no bound on their arities. The theory corresponding to the pow= erset monad, eg, is the theory of sup-lattices, ie posets with arbitrary sm= all joins, which is not expressible with operations of bounded arities. Reg= arding references on these generalizations, I would also be curious. Concerning your questions on extensions of theories, and more general kinds= of theories and base categories, there recently was a long thread on the c= ategory theory zulip server [2], which I'll try to summarize: extensions of= single-sorted theories by new operations and/or equations are always monad= ic (regardless of arities); this follows from the fact that monadic functor= s have the left cancellation property (Proposition 3.3 in [3]). Extensions = by new sorts are typically not monadic, eg Set x Set is not monadic over Se= t. The models of many-sorted theories are monadic over powers of Set, and e= xtensions of many-sorted theories by operations and axioms are also monadic= , again by cancellation. Things become more complicated in the generalized/= essential algebraic case, since (in the generalized algebraic, ie dependent= ly typed case), adding new operations can create new sorts by substitution,= which can lead to successive monadic extensions which are not composable, = as Tom Hirschowitz, James Deikun, and possibly others pointed out. In gener= al there's a lot of ongoing work on the dependently typed, ie generalized a= lgebraic case, such as eg Chaitanya Leena Subramaniam's recent PhD thesis r= epresenting dependent algebraic theories by finitary monads on presheaf cat= egories over direct categories [4]. [1] https://www.dpmms.cam.ac.uk/~martin/Research/Publications/2007/hp07.pdf= [2] https://categorytheory.zulipchat.com/#narrow/stream/229199-learning.3A-= questions/topic/distributive.20laws.20and.20monadic.20functors [3] https://ncatlab.org/nlab/show/monadic+functor [4] https://arxiv.org/abs/2110.02804 On Sun, 4 Feb 2024 at 21:00, David Yetter > wrote: We are all, of course, familiar with Beck's Theorem. I'm rather hoping tha= t there are results in the literature that will save me from having to prov= e that the underlying functor U creates coequalizers for U-split pairs in t= he context of two quite different projects I'm working on. Thus, I have tw= o questions for the community: 1. It seems obvious to me that for the same reason categories of models of fin= itary algebraic (equational) theories are monadic over Set, if one has (I t= hink I'm using the term correctly here) a conservative extension of an equa= tional theory (by which I mean, add operations and equations in such a way = that no new equations are imposed on the operations of the original theory)= , then the category of models of the extension is monadic over the category= of models of the original theory. Surely this is either explicitly stated= and proved somewhere, or follows easily from some result I simply have not= encountered. Citations? 2. What is the most general sort of theory whose models are monadic ove= r Set? Or if that is not known, what sorts of theories have monadic categor= ies of models over Set? Are there multisorted generalizations of any resu= lts of that sort, ideally not just to Set^\alpha, where \alpha is the cardi= nality of a set of sorts, but to things like Graph? Again some citations w= ould be much appreciated. Best Thoughts, David Yetter University Distinguished Professor Department of Mathematics Kansas State University (That is the first and last time I'll use that signature block in writing t= o the list, but I thought I'd do it once since I thought the community woul= d be gratified that a categorist was so honored. After this it's back to D= avid Y. or D.Y.) You're receiving this message because you're a member of the Categories mai= ling list group from Macquarie University. To take part in this conversatio= n, reply all to this message. View group files | Leave group | Learn = more about Microsoft 365 Groups You're receiving this message because you're a member of the Categories mai= ling list group from Macquarie University. To take part in this conversatio= n, reply all to this message. View group files | Leave group | Learn = more about Microsoft 365 Groups You're receiving this message because you're a member of the Categories mai= ling list group from Macquarie University. To take part in this conversatio= n, reply all to this message. View group files | Leave group | = Learn more about Microsoft 365 Groups --=_321b50fca6038d45142e1fbbe8004832 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=UTF-8

These may provide some added ingredients:

https://www.sciencedirect.com/science/article/pii/S= 0165011413000997

https://www.sciencedirect.com/science/article/pii/S= 0165011415003152?via%3Dihub

https://link.springer.com/book/10.1007/978-3-319-78= 948-4

The focus here is on (multi-sorted) term constructions and more generall= y over monoidal closed categories. Other papers we've written build upon th= ese where term constructions are used in sentence (formula) constructions.<= /p>

Not clear to me what David precisely means by "no new", but in our case we = have been used to say "logic must be lative" in the sense that "first terms, then sentences from terms" and n= o new terms from that, and "then entailment constructions from sentenc= es" so that no new sentences are constructed from entailment. Here is = where logic mixes "true" and "provable", and this is the very spot which allows G=C3=B6del to "prove" incompleteness = using the Liar and Richard's technique. 

Respecting= this principle of lativity, G=C3=B6del's 1931 results are basically non-se= nse. Grundlagen II =C2=A74-5 tries to deal with it, with some success, but not fully as GdM amd other work at that time, n= ot just in G=C3=B6ttingen, never properly dealt with the underlying multi-s= ortedness with subsequent term and sentence constructions. Maybe it's Russe= ll's fault? Principia said Peano had suggested that logic must be freed from algebra. Peano never said that, bu= t Principia did it, so "formula constructions" remained as a, as = Peano said,  "putting symbols one by one in sequence". That'= s not a monadic approach to forming terms and sentences, is it?

My point i= s this: Category could have been around already before 1917, as the set the= ory used in category theory basically is the set theory that was available before Hilbert invited Bernays to G= =C3=B6ttingen. Had they used categories for foundations, G=C3=B6del's 1931 = paper would probably never have been written. I have always wondered what G= =C3=B6del means by "isomorphic image" (in his footnote 9) in his 1931 paper. 

Patrik


On 2024-02-05 06:21, Jonas Frey wrote:

Dear David,
 
Yes, models of s= ingle-sorted algebraic theories are always monadic over Set, and such theor= ies correspond precisely to finitary, ie omega-filtered-colimit-preserving = monads on Set. If we take the correspondence between single-sorted algebraic theories and Lawvere theories for granted,= this is stated eg in Hyland--Power [1], with further references there. Mor= e generally, monads preserving alpha-filtered colimits for a higher regular= cardinal alpha correspond to algebraic theories with alpha-ary operations; unbounded monads (such as the powerset= monad) can be viewed as corresponding to "large theories" with n= o bound on their arities. The theory corresponding to the powerset monad, e= g, is the theory of sup-lattices, ie posets with arbitrary small joins, which is not expressible with operations of bo= unded arities. Regarding references on these generalizations, I would also = be curious.
 
Concerning your = questions on extensions of theories, and more general kinds of theories and= base categories, there recently was a long thread on the category theory z= ulip server [2], which I'll try to summarize: extensions of single-sorted theories by new operations and/or equations ar= e always monadic (regardless of arities); this follows from the fact that m= onadic functors have the left cancellation property (Proposition 3.3 in [3]= ). Extensions by new sorts are typically not monadic, eg Set x Set is not monadic over Set. The models of many-sort= ed theories are monadic over powers of Set, and extensions of many-sorted t= heories by operations and axioms are also monadic, again by cancellation. T= hings become more complicated in the generalized/essential algebraic case, since (in the generalized algebr= aic, ie dependently typed case), adding new operations can create new sorts= by substitution, which can lead to successive monadic extensions which are= not composable, as Tom Hirschowitz, James Deikun, and possibly others pointed out. In general there's a lot of= ongoing work on the dependently typed, ie generalized algebraic case, such= as eg Chaitanya Leena Subramaniam's recent PhD thesis representing depende= nt algebraic theories by finitary monads on presheaf categories over direct categories [4].
 
[1] https://www.dpmms= .cam.ac.uk/~martin/Research/Publications/2007/hp07.pdf
[2] http= s://categorytheory.zulipchat.com/#narrow/stream/229199-learning.3A-question= s/topic/distributive.20laws.20and.20monadic.20functors
[3] https://ncatlab.org/nlab/show/monadic+functor
[4] https://arxiv.org/abs/2= 110.02804

On Sun, 4 Feb 2024 at 21:00, David = Yetter <dyetter@ks= u.edu> wrote:
We are all, of course, familiar with Beck's Theorem.  I'm rather hopin= g that there are results in the literature that will save me from having to= prove that the underlying functor U creates coequalizers for U-split pairs= in the context of two quite different projects I'm working on.  Thus, I have two questions for the communit= y:
 
  1. It seems= obvious to me that for the same reason categories of models of finitary al= gebraic (equational) theories are monadic over Set, if one has (I think I'm using the term correctly here)&n= bsp;a conservative extension of an equational theory (by which I mean, add = operations and equations in such a way that no new equations are imposed on= the operations of the original theory), then the category of models of the extension is monadic over the category = of models of the original theory.  Surely this is either explicitly st= ated and proved somewhere, or follows easily from some result I simply have= not encountered.   Citations?
     =
  2.  What is= the most general sort of theory whose models are monadic over Set? Or if t= hat is not known, what sorts of theories have monadic categories of models over Set?   Are there multisor= ted generalizations of any results of that sort, ideally not just to Set^\a= lpha, where \alpha is the cardinality of a set of sorts, but to things like= Graph?  Again some citations would be much appreciated.
 
Best Tho= ughts,
David Ye= tter
Universi= ty Distinguished Professor
Departme= nt of Mathematics
Kansas S= tate University
 
(That is= the first and last time I'll use that signature block in writing to the li= st, but I thought I'd do it once since I thought the community would be gratified that a categorist was so honore= d.  After this it's back to David Y. or D.Y.)
 
 
 
You're receiving this message because you're a member of the Categories mai= ling list group from Macquarie University. To take part in this conversatio= n, reply all to this message.
 
Vi= ew group files &n= bsp; |   = Leave group   |   Learn more about Microsoft 365 Groups
 
 
 
You're receiving this message because you're a member of the Categories mai= ling list group from Macquarie University. To take part in this conversatio= n, reply all to this message.
 
Vi= ew group files &n= bsp; |   = Leave group  = ; |   Learn more about Microsoft 365 Groups
 
 
 
You're receiving this message because you're a member of the Categories mai= ling list group from Macquarie University. To take part in this conversatio= n, reply all to this message.
 
View group files   |   Leav= e group   |&n= bsp;  Learn more about Microsoft 365 Groups
 
--=_321b50fca6038d45142e1fbbe8004832--