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 7911 invoked from network); 18 Nov 2022 14:22:17 -0000 Received: from mail-pl1-x63e.google.com (2607:f8b0:4864:20::63e) by inbox.vuxu.org with ESMTPUTF8; 18 Nov 2022 14:22:17 -0000 Received: by mail-pl1-x63e.google.com with SMTP id q10-20020a170902f34a00b00186c5448b01sf3961001ple.4 for ; Fri, 18 Nov 2022 06:22:17 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1668781335; cv=pass; d=google.com; s=arc-20160816; b=GlT36IXa3dVd5t3mtnm78JLGA8BZkDyw5CbI1UDz0ucjmrS2Ql+a+4zL6u4SmDoTTf MlOPZFtGR0UD+rV2t9wVjfCyRKyehp3F0W5jUgKlHHAl+qTSE1w6E9F8ZClyMxTW4frC mDa+L/i0YJRfh8uM2/0YnaiixPCjCpurPWpNO4wwbcb+yu1zlz8MTl/iW1CF2OnQt8Sj Rzbx86l02i0bmR35Qalt9R3uF+g1tM3O2Mamzz8vfb2y3/k8mxrhmmrlt31VBcbvFtSZ 0us7FuKc/lQkuBnqn37iBEOJEmFtB3kRKJs2weNLE4VbYuODhQ3oDVIWvfksi5sklWW1 izKg== 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:from:sender:dkim-signature; bh=07N2f8QYOdegsG3W/HYOrJg/XM9x1cKk4iSgVe15YJQ=; b=zYIzCoKErutQNwwpHVAxQBcqcsKw87e1x1q6A2qRLF4EBRsmBg40wmcjJ4OeIpaG3V ek1KrzJaYguVSzdTXPBvXtHHHaSPY3w4XZyb/QIKHHu15qkdYc5sbM+mMyZPzdMWYZ7x bq5+kYi1MMi6U9CV77HRXmuUkgIRQaAwP6x+FlcSmTLRIzaqrFOLQ4ylVPveRMs6xhVV acLZhYZOsQZzzXqdB+PF5Fr8X/ggoPU0vxTa/QoknJfsqLxWrwIRQw5Lup8L/6TQ/56s pICAJ45ZtniSKWyMQh3MN5wrJnRtLvLVA1Wv1S6TR0RJSnZsJ7QuiBGtPqn0sHHYlyqV O79Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@andrej.com header.s=sig1 header.b=aWPnVRrl; spf=pass (google.com: domain of andrej.bauer@andrej.com designates 17.57.155.4 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:from:sender:from:to:cc:subject:date:message-id :reply-to; bh=07N2f8QYOdegsG3W/HYOrJg/XM9x1cKk4iSgVe15YJQ=; b=ffWik0gqnJ8XEZYoy12JU1OD915sjGkMjaGBWUQYJFI7Pp4zR77sEcF3/fa+8FhNkS KCvAMY2A9h6Vx2JRehHEiaXwN7qn5b/USYcwrlrG615eq9n7DwQSf5gf7SJb7Jux9o0D XHi5XvcFB/R6Kuls7PhzNwePpL4G/8J4Eq7oVXCgh9mMi4pI0tk+Tg4Q4muDval0fQGQ bMJbl0HeOuczjn7S/TRHaR283CDPhCC0yCkrRki6m+xGCkTt8HyjLpDvlaK/BlExV6Fl xP1XCE+5xKY2VAsiI0rzIfshaGgQGdX2F+xF/PB+EeYHdbxkkWa+NEX9f3/DWm7BT/XY MkbQ== 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:from :x-gm-message-state:sender:from:to:cc:subject:date:message-id :reply-to; bh=07N2f8QYOdegsG3W/HYOrJg/XM9x1cKk4iSgVe15YJQ=; b=vytiNJKSHecjTgHIw0CkJU2T4+UYYwF/+7TwlQs/FYXzuZ69JCSvBt0p7PWZlIP4Cb JNO0YQOuc1v9DrSQAnuaGnenlJLUkWFhVIEhg2hEdhEE800F+gbiPXWuDPRZWrewMEdN SclSt6c7W3ZiPBOqJJ2TBHRTd0tX/zx8J2fK6w2saAPQCJI1o4Kst8jkAtiw+x74uO9+ C7ujX0fU1ZvZXg8RUIAy09XWfD8//EfakvhBDQ1Rp2S3zKojWCmJGx1l7clsQx9Mrrgj emMBFMZlLQUDr4H+5P6hPaQnF39DfPFf6dHtqD2pt1I8lGTgYlLw9O8pbYWpEc6QgdDr BzWg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5pkx6aW3O72j35krkOWEMGY9hjBqLcggkNRmRNg19hEG1iaQGPrx VO1ITQrcx1lr7AIuRYL35iU= X-Google-Smtp-Source: AA0mqf5E1d60o3J/v3bZmcHWjeqBLb0hVh4MRQoSNdyp9x4Z7U0WyYh7wBAzCAVYqDQuT2rvUcovLg== X-Received: by 2002:a17:90b:128b:b0:20a:f469:7307 with SMTP id fw11-20020a17090b128b00b0020af4697307mr14130893pjb.213.1668781335422; Fri, 18 Nov 2022 06:22:15 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:1c06:0:b0:561:e77b:c7c2 with SMTP id c6-20020a621c06000000b00561e77bc7c2ls2635775pfc.4.-pod-prod-gmail; Fri, 18 Nov 2022 06:22:13 -0800 (PST) X-Received: by 2002:a63:5641:0:b0:470:48c2:3aa1 with SMTP id g1-20020a635641000000b0047048c23aa1mr6801265pgm.45.1668781333592; Fri, 18 Nov 2022 06:22:13 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1668781333; cv=none; d=google.com; s=arc-20160816; b=JFFeRYBIDBQLAYe14ugwBleVWq7bP17+aHYZUbPJy3eagLO9Yk/Qqh1nUe3QdOzMD6 D592ldMvu652bf/ulS5ZAKwNUXC3Sj0xT+5hpQQrhr41y3pTHWRqMEYUd6OWeN5cgpQn YydxzeyIXaet0/3ppzkzgFbn3JNmrzeqBn1F6BW/toXLD1YTMfSRXWWMrKqsPyHJ82zH 4Hb038IbOMThc9cASdYyhKHfK6UZUorSEEQg+5v2U2LjJMwp4Kd294RCWD0/JxOxb+VG 4jEI8dLH9GXOkcK6g5R6jFGzzKRRdAUxCAyfj1MiO7+rJPotI3MFa8/H9eJa7rIB7BSN AQ0g== 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=g29HxTejgE5K+qCBrhHj3xN17U/PlN5gJxu8tV/N3ns=; b=yyDwkC89gQ3FL2YZ62pYonqzYHkxc0c277Hy5I4ZbpxdqjTwIRZy9VRh+ORrqcGvWq lnMTMCLJhd5RMsglxtB7GT8NvzgKD/2KfQ/pFxsydnNXulrMTtY3sz0xLV06f7LoQg/n Pro+1qZVq+w3Ltdvc5rcscpGW24//1nqBp2Uv1A5flvf65FPSSUh5mOxzcIV1CvCN3uV NQ/m+Y+GawgPtVFB2aIIfBsSe14GuhpkPrZwIx51NQslb7/ev+u7hL1hHCw27ZdaPX22 Y3WKEHHPaOEAx5MGE3amnGUmRx0TULYLWvq1VicpA3l13AowHi25pyYkgj0JP+MvUyho 5qHw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@andrej.com header.s=sig1 header.b=aWPnVRrl; spf=pass (google.com: domain of andrej.bauer@andrej.com designates 17.57.155.4 as permitted sender) smtp.mailfrom=andrej.bauer@andrej.com Received: from qs51p00im-qukt01071501.me.com (qs51p00im-qukt01071501.me.com. [17.57.155.4]) by gmr-mx.google.com with ESMTPS id l187-20020a6225c4000000b0056bb72479bdsi223268pfl.0.2022.11.18.06.22.13 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 18 Nov 2022 06:22:13 -0800 (PST) Received-SPF: pass (google.com: domain of andrej.bauer@andrej.com designates 17.57.155.4 as permitted sender) client-ip=17.57.155.4; Received: from kylie.fmf.uni-lj.si (qs51p00im-dlb-asmtp-mailmevip.me.com [17.57.155.28]) by qs51p00im-qukt01071501.me.com (Postfix) with ESMTPSA id 7EC2A1C405AF for ; Fri, 18 Nov 2022 14:22:11 +0000 (UTC) From: andrej.bauer@andrej.com Content-Type: text/plain; charset="UTF-8" Mime-Version: 1.0 (Mac OS X Mail 13.4 \(3608.120.23.2.7\)) Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory Date: Fri, 18 Nov 2022 15:21:59 +0100 References: <96f15467-49c9-43cc-8868-40b1bdf2162dn@googlegroups.com> To: Homotopy Type Theory In-Reply-To: Message-Id: <13907424-5B03-4804-AC89-33DC5466F497@andrej.com> X-Mailer: Apple Mail (2.3608.120.23.2.7) X-Proofpoint-ORIG-GUID: 8xoIBn6pkuJ7986Esa-Z5a6qCgkUF5Up X-Proofpoint-GUID: 8xoIBn6pkuJ7986Esa-Z5a6qCgkUF5Up X-Proofpoint-Virus-Version: =?UTF-8?Q?vendor=3Dfsecure_engine=3D1.1.170-22c6f66c430a71ce266a39bfe25bc?= =?UTF-8?Q?2903e8d5c8f:6.0.138,18.0.790,17.11.62.513.0000000_definitions?= =?UTF-8?Q?=3D2022-01-12=5F02:2020-02-14=5F02,2022-01-12=5F02,2021-12-02?= =?UTF-8?Q?=5F01_signatures=3D0?= X-Proofpoint-Spam-Details: rule=notspam policy=default score=0 adultscore=0 clxscore=1030 mlxlogscore=346 spamscore=0 suspectscore=0 mlxscore=0 bulkscore=0 malwarescore=0 phishscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.12.0-2209130000 definitions=main-2211180083 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=aWPnVRrl; spf=pass (google.com: domain of andrej.bauer@andrej.com designates 17.57.155.4 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: , I am sorry I started such a long conversation about so little. Of course one needs to distinguish structures from presentations of structures, which can be done without promoting one's personal preferences as value judgements about the 20th century type theories. Mike already explained why presentations are important. Thank you. With kind regards, Andrej -- 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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/13907424-5B03-4804-AC89-33DC5466F497%40andrej.com.