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.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 20259 invoked from network); 14 Apr 2022 09:25:24 -0000 Received: from mail-lf1-x138.google.com (2a00:1450:4864:20::138) by inbox.vuxu.org with ESMTPUTF8; 14 Apr 2022 09:25:24 -0000 Received: by mail-lf1-x138.google.com with SMTP id n1-20020a196f41000000b0046d14d9067asf427817lfk.18 for ; Thu, 14 Apr 2022 02:25:23 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1649928322; cv=pass; d=google.com; s=arc-20160816; b=EtmtS+IfPb1gkPPFN4RbHPTHvauJNxwFxM+BPdUdjTIfT4Xv3OCLB6u2XGdj5iKfUC ofl36nUok+vw98sv/MDn2T/N9NKWiAm/fpLmJMAyR8MzMRMW98s9P3UgS0WHMVvpXeR0 kRfJhRiVNwkIIxfUawKzKVeqaRrSiMJyQRk4hEYkVwU04fsV08Ckas5V1IChYMrl5+4w JU41BJPyXr4uodaNQ5G8RMJTKV0SIYQDXICly+D4XYi22qfCcomOtZJ6pWY9qgOLVu+H V8Glbbb99nDHMysKi04+MTuWtuNCFoPBbVT3+WrxeMKAAYtRBfhgqpqjfTeGMxhiZjnc qDig== 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:reply-to:content-transfer-encoding :cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=VQLwVlqOQT690SF9ZM/eHFOv3I5Eyl5dVBdrh9FYJ+4=; b=LmAPLaUSRh0TeSu58b5ikh9aqzHv45KHMNirifkQnmItzkpBvg1tvp6/dTMW3tCca+ Mn9mA8vaMsjzCXGqcNxaoQsYp6a5aX1P9JDiKB+1ajRz3fMvrHXTfpMK66otBnnyfdu3 y/IMNvOoVQ5JZABbwGhAxEVBWOAVMnk/6azRPth2Y9S0VEIZD95nCGuywJgMuw1IbD+t UtRt3Lhn+UFD6km0jdQuLB2L5vfMATmYtRBsvkIO6byIVnQI4svl7cD494MY5hmKAjrM RSNEuuo0S3bOV+Nf1RzUDxtNbIK1q86fVmKgfAyT4jAcciLgK38goFHFTbDQz4lRgNa7 ypDg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@googlemail.com header.s=20210112 header.b="l/heEnmu"; spf=pass (google.com: domain of urs.schreiber@googlemail.com designates 2a00:1450:4864:20::430 as permitted sender) smtp.mailfrom=urs.schreiber@googlemail.com; dmarc=pass (p=QUARANTINE sp=QUARANTINE dis=NONE) header.from=googlemail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:reply-to:precedence:mailing-list :list-id:list-post:list-help:list-archive:list-subscribe :list-unsubscribe; bh=VQLwVlqOQT690SF9ZM/eHFOv3I5Eyl5dVBdrh9FYJ+4=; b=MT6mcFcdjHDhM930a/Ev5bDTMN8xtnxIN2HdJWj9TmYLzBdl2Ky60phhRrIXSnPFT4 93OfW0O7/fBkyBHhWB80U8d6kq7Za7fL3yoNOSj1DINBCnScHHlOZmWsX9toKd8NLcmP N13GdpEiQ+Em8BZppdqRkR0dqe21efsP0/2vsoV9MBiga2GEit/lakPTEe3E4ooOl4kp nQkY3Usf52BFvgNr+rYgUsGScrPbnVBwawZ0r2tssR54IcxmvyvqY9uryzdpfsD+Xg38 VvQ9hVhYleUaf3WXG8EO4pY4jdKEv5sJAKmnHriqEsZE3mRTIRZqIdwDu3OoAxBzdJE8 8tKw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc:content-transfer-encoding :x-original-sender:x-original-authentication-results:reply-to :precedence:mailing-list:list-id:x-spam-checked-in-group:list-post :list-help:list-archive:list-subscribe:list-unsubscribe; bh=VQLwVlqOQT690SF9ZM/eHFOv3I5Eyl5dVBdrh9FYJ+4=; b=gI1vR74pptsJEBtyd2kLD4p2BCqT6II5U/i2MU9rT2ksUbb67tdYLO5qa8FOjlnNtq gGrKxPoM3ZSe4owkLSvKex/0jbrKFGRh98yKN6V7I25U+D0oxGXyx1u3uFMw457syGe5 OWVKtmsb6P4GW8eHLxUur+OXbheTe+r746xProFUHrLUOtpMFJcQV/M8Da5XWjmNVlkb mFpf5G0QVTA/rCNKU1niDuavqhEGxBBnlrj272Jrb9Yo9IsolCLzeSZ6ABevF4sLhFc6 XobZcKdmDIYPDn0G9OXXNncHOCV/6H5YsLUkObPlRR7y+U8KYNHw2bAYZPN2e8rq+FeN m+kA== X-Gm-Message-State: AOAM530gaElKA2qc9HldftOPeQy9PlsX/sVKFcv1/h7yqvfmE4MqJwmt E0lP4KdPpxb7RzjPQ4+NbEk= X-Google-Smtp-Source: ABdhPJzDf8f2uoAMEJac5Pp5D72VGdJt4Uq2WxcSxLPvfVBc4kk0UPUqmuoyY45kdZGKiE6Zjk/aRA== X-Received: by 2002:a05:6512:32c2:b0:46d:12ba:e065 with SMTP id f2-20020a05651232c200b0046d12bae065mr1456333lfg.374.1649928322499; Thu, 14 Apr 2022 02:25:22 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6512:1693:b0:448:3742:2320 with SMTP id bu19-20020a056512169300b0044837422320ls4037791lfb.1.gmail; Thu, 14 Apr 2022 02:25:20 -0700 (PDT) X-Received: by 2002:a19:5f0e:0:b0:44b:111:1622 with SMTP id t14-20020a195f0e000000b0044b01111622mr1342364lfb.161.1649928320312; Thu, 14 Apr 2022 02:25:20 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1649928320; cv=none; d=google.com; s=arc-20160816; b=PrdotTyOiuMfGYXMTBry77YhtFZDrx7+XTSkBLizCmLAFxHcMusX5rEig7SXcENbTY O6m7McjbU+KItnchAT8DmxBx5nR6I5CCfmJ1ooy8NfGpDgf3KTiOXrdYH0TuGK5uxlfL 8TrDIyDfpO4m/ZvHEa2ISEP9q8t6o/DexgrS3a8lyIBiF+3ZuHCK0vtTkwQdVS6UmZdj VCzLsxoFPjKrAQLTpdSmOohoX+4J2Muf7nmydJ5GO3xerfwm3x3fLjR/nBsiLmJjF17t xQZje4CL5qBpNxI559wnFrkdREhUrekMtrQqDXyLKKJBMIDeTyGizs1Ye4gsVKRKfAZh YcBA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=BiTlcK53O8i0JzKB272Eqa70V9h0kv1swMRmLPJkZ7w=; b=0169SLxBgykZRw2mFBNRtDmUr5b8WV5LiIvLKveG3zrYKO7L/y8NBzENScoazW6nfi uLBxDYKX+4TgIbFDzeexiIFxoCAv0BDYKsRnUAHxqDYeNunJzC7PksqOPeqFhpyNXEMB VUhG6/mzmw1D5LFwSnaMQfwdUM+f/GhXSUwVY/l56xusSsMywXUPKPJ+MLdyLzXkWTT4 EYaAE8XSh2KoLtYpfB12+akVUpSx1Ybq9u3E9jU+F0NpWcC6hfWgQMp0x+30K+X2I/DT weE1ljbIz//T1K13VA7eZlvnXfUwOETqb4eoSb80sujg3MGHLSpqYggt9roeOXwp9M3k ut0g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@googlemail.com header.s=20210112 header.b="l/heEnmu"; spf=pass (google.com: domain of urs.schreiber@googlemail.com designates 2a00:1450:4864:20::430 as permitted sender) smtp.mailfrom=urs.schreiber@googlemail.com; dmarc=pass (p=QUARANTINE sp=QUARANTINE dis=NONE) header.from=googlemail.com Received: from mail-wr1-x430.google.com (mail-wr1-x430.google.com. [2a00:1450:4864:20::430]) by gmr-mx.google.com with ESMTPS id w1-20020a2e3001000000b002499fdca3e4si988843ljw.3.2022.04.14.02.25.20 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 14 Apr 2022 02:25:20 -0700 (PDT) Received-SPF: pass (google.com: domain of urs.schreiber@googlemail.com designates 2a00:1450:4864:20::430 as permitted sender) client-ip=2a00:1450:4864:20::430; Received: by mail-wr1-x430.google.com with SMTP id c7so6120787wrd.0; Thu, 14 Apr 2022 02:25:20 -0700 (PDT) X-Received: by 2002:a05:6000:1d89:b0:205:e6d5:c571 with SMTP id bk9-20020a0560001d8900b00205e6d5c571mr1360755wrb.594.1649928319948; Thu, 14 Apr 2022 02:25:19 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: "'Urs Schreiber' via Homotopy Type Theory" Date: Thu, 14 Apr 2022 13:25:09 +0400 Message-ID: Subject: Re: [HoTT] Re: M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series To: Chris Kapulkin Cc: HoTT Electronic Seminar Talks , Homotopy Type Theory , categories Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: urs.schreiber@googlemail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@googlemail.com header.s=20210112 header.b="l/heEnmu"; spf=pass (google.com: domain of urs.schreiber@googlemail.com designates 2a00:1450:4864:20::430 as permitted sender) smtp.mailfrom=urs.schreiber@googlemail.com; dmarc=pass (p=QUARANTINE sp=QUARANTINE dis=NONE) header.from=googlemail.com X-Original-From: Urs Schreiber Reply-To: Urs Schreiber 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 Thu, Apr 14, 2022 at 5:28 AM Chris Kapulkin wrote= : > We believe the speaker=E2=80=99s recent statements in the context of the = HoTT > Book stand in opposition to these values Scrolling up this thread for context, one gathers you must be referring to this statement: "In Book HoTT, identity is defined uniformly [...] many desired equalities are not definitional". While possibly scandalous, I am tolerant and was looking forward to seeing the arguments, if not for moral but for intellectual edification. Is there a draft or preprint available of the announced work by Altenkirch, Shulman & Kaposi? It sounds intriguing. --=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/CA%2BKbugem61xD06bxhHvd5vuUJdHrt%2BCJu0%2BYoJvNBM57jCxJC= A%40mail.gmail.com.