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=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 21290 invoked from network); 24 Feb 2021 14:50:26 -0000 Received: from mail-lj1-x23c.google.com (2a00:1450:4864:20::23c) by inbox.vuxu.org with ESMTPUTF8; 24 Feb 2021 14:50:26 -0000 Received: by mail-lj1-x23c.google.com with SMTP id t8sf628432lji.1 for ; Wed, 24 Feb 2021 06:50:26 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1614178225; cv=pass; d=google.com; s=arc-20160816; b=lVm/f+9Skz3+RfWKKe1H4dmlS5K7apcH0/1tjt+UNVcHhdB6zNUbl8b+yOWwUfeTZN UbtYNnyMtBnYsTJ/xEi20+vuqsDYjIFOOim+BaiFileWuFqKiEx/ZfLuhXx7dl3+hWHV cqQhOXsAfJvM29KJoh0OvaDuBqM/onCqi0bSR1ip5yzhrWXAkllcILJte8lJx4c0yHMz tkUyr44MTcTnszHPbE8Hu1CWtqpssd2n3d27INeW4PpneOdaH4l0hGxnwXtqcxscg1f8 Gbsj1X2zbJNfYBgNO+xUSx8vloWf3y9zzcAZu8bpnuezj05FJt3cTYV33R/8gxhnjR62 wtpg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:content-language:mime-version:user-agent :date:message-id:subject:from:to:sender:dkim-signature :dkim-signature; bh=/QPwXQo/8erxUmN9oCP6+zOXceZ/WZBYHTI8QXMIii0=; b=OykOAu85xCNzp4FfmI+lD729PeA0hjeGFnyoYpsY29TwaXTDHWDDlEVft4YwT44lZd zMzZcAeJxaFj8bpuPbcyc8sK6WCLeRIqEwaIGc+3gURKfXhiY8Wjh7TT0zttT0hb9CPR lgTe4N9g6A89aNAl9lsqyWwVHaDOvK/BQTwJALA1D6JWDw6wtdv3Uou1jsrMYlK+a72j dldP5QS1kLhnAcAZhZYtfL7u1DoNXFk3Fv5simCAsSyFB1nIWy3jshdqq7z1jB7CdWnI Nan2kpqCylUKHYJ4qxq0fgtmOEnt0HjuRbN/xlOTFOA4TL/rtVKUKw7enx8/bb6gaUmu K0Ow== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=h2S7aC9l; spf=pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::42a as permitted sender) smtp.mailfrom=escardo.martin@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:to:from:subject:message-id:date:user-agent:mime-version :content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=/QPwXQo/8erxUmN9oCP6+zOXceZ/WZBYHTI8QXMIii0=; b=qTfL/YeKmQxd/cuBeyEsT50J7lQOx5/w/+lF0tq0ZH0kW4ZOd6iw9q93aSWt5MU1o/ whY+BT3IWi1wFt9QbgLshPV4TRyWuc6y7ihG2UieJ+NFn70BdhhJ1cGh2/Fh0E5WpyN6 0QDYPYP+oq+qmulkSZIZJrpquM0fDGFbMBlcZ1V+u5isPOUF+hXXccYsEEKyqxC+fvw5 OkiozhOZQV0kTu0jw1GQztnVKnZqXKg/SM2ggqVFDF8NveTX6y+rHLrUKViYdFvYpNBh SHbHMHc6h4PfRzPbAtfbqj/YgniQGtKprjeg0jlm4m0ik+eTDIhQotqOVAo7Shj3+xJB bjxA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=to:from:subject:message-id:date:user-agent:mime-version :content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=/QPwXQo/8erxUmN9oCP6+zOXceZ/WZBYHTI8QXMIii0=; b=qQ2W7uXBhKI6l8/2jLReVu5d+QFOk6O6h3q9EDYxGIztJ6MvuUaXC94vSfBF7bRAHz Namn+mEjS3FUPrPXt1Qq+K2BDPWfBUCDJxG3C1K4z9nC73d8nZYH5vs7YVRLUqfMiUGt NP+oz5Cf2DXm00DZ3db8mjO5qrgHZFiV3PdNTz4Lr5At3Gi7ZnZmqX9t0ZeVmI1s1B65 navyV2k8oKdOkO+22yhVMgZL+7XKy6zsv+tkBkvwNeL7okH0JvfQBUZ4+X7XxxtuYuMt ozAuDuTmnky1okjKD7suQZNcIqU3+nK0SDwHj9//o5NF6+BLbBaTuMbgPOK0fCiYOQEO ykZQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:to:from:subject:message-id:date :user-agent:mime-version:content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=/QPwXQo/8erxUmN9oCP6+zOXceZ/WZBYHTI8QXMIii0=; b=gRiXIV9C7H7n/hhp2wTtNrsKtHhqlktxnvxfGm3p5p8meBCITtenQcvJNe+T0lRk86 JKsL1fnb5s+q+wEgdWNvqhUw/QGgD98yN0xthxUYs0DEtYe9tTTMu7OsCs5D4F67SOKE N4r2E+yeUbfwG4tPL1v/I33lfCEReSvEiL77KjdPUFUa1e68vSzZbysdTWV82gQW0yHO Fkz68W9tdPfhnfYchbcZz1LU6B/+7MJpSuAC1ruW3DRDj5edvgEkbWqlXc4Ow87TiiD0 loOk37gzMqco6lhHCkYLgFxvstzEgHmxETSZqIhqoKGhM51xUkaXTNDRRaNUQctDBiPp benw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM530GeOoao8yB9nQp97im6cm+Tf+OBzxvaEbkMbxD+Z2cmn6ccmlC fRHv2c5fyPy1rMXK+vDm1U8= X-Google-Smtp-Source: ABdhPJw5at1DqvQ2dEatdh069scKVEiLalMvCrjVXD6ZDsvBgVBLyYNxE9vTigE6ljFw/QkwXtoZZw== X-Received: by 2002:a2e:968c:: with SMTP id q12mr3452906lji.317.1614178225569; Wed, 24 Feb 2021 06:50:25 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a19:e86:: with SMTP id 128ls1534172lfo.0.gmail; Wed, 24 Feb 2021 06:50:24 -0800 (PST) X-Received: by 2002:a05:6512:14e:: with SMTP id m14mr20771620lfo.503.1614178224261; Wed, 24 Feb 2021 06:50:24 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1614178224; cv=none; d=google.com; s=arc-20160816; b=QvS2Uh3NhKtqV4EZkjNH9fDpb2Fl3sewT9naVpZ/JphbuDIMri6KXdT28zP46nUneJ JRUBOWLkq/H1+/SH8zE7QUsRTERQPNkurD96gw4MYvzfm68JkC9fNpSW52m6KKJyfXlQ a+kSVGMBjZoz6w/C5dYTOq6aIRoz8fphYdBfLUkA8M8NI/DNymzGOz6n0lqc2mnvQwl5 ZlivHMDj12XK33B1YwypZrUmLgudsBsKfZDjrli0j8YmWzjPW7z2B6Act0RDB4tSer05 GhQ2ulXw4cPta3HBQXwye5q/cpt/XtaBDa9A2Qfib4tCbJBrZYDW8nnazlA1Lxl9Vw64 0oHw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:mime-version:user-agent :date:message-id:subject:from:to:dkim-signature; bh=Zap9r/H7mdqMwFVsig7q3bJjtTEG8goXZasWnD0NkP0=; b=xZImmKvi7gvV2maNexzQ+mmy+cZnSdhZuAYYM7oZyu2YUa+1pi4iWvzJbAAV+lSZO3 jndGb1gOBTmjA7YtkwnlJivoNhlPUSSnOLWFRwq+VLTYJigqJVp0qJwXFrIxNZ3KGcLb GNJXWDOn0DlJkuWXU0UfmqhuzmIcKK1ABsKJp9o1J6A1z2Mu2F9SS4N8q+X2P0cflrnb fhUfT9enW8ydXg18qiFXMmRlmpF91ic29nH4pQoB7JFRX7p/qb10cKElF8RSPm0SGL8T 6hfv7DAJXPxsvYe1EbjLlmaqRuFZ0VbQCBJeCaB1Hp5uQgHkQ4Z8UbYUgizt7O0+7H1n yCdA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=h2S7aC9l; spf=pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::42a as permitted sender) smtp.mailfrom=escardo.martin@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wr1-x42a.google.com (mail-wr1-x42a.google.com. [2a00:1450:4864:20::42a]) by gmr-mx.google.com with ESMTPS id a26si123277lff.2.2021.02.24.06.50.24 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 24 Feb 2021 06:50:24 -0800 (PST) Received-SPF: pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::42a as permitted sender) client-ip=2a00:1450:4864:20::42a; Received: by mail-wr1-x42a.google.com with SMTP id b3so2157079wrj.5 for ; Wed, 24 Feb 2021 06:50:24 -0800 (PST) X-Received: by 2002:a5d:47af:: with SMTP id 15mr32176228wrb.205.1614178223557; Wed, 24 Feb 2021 06:50:23 -0800 (PST) Received: from [192.168.0.14] (cpc1-king14-2-0-cust212.19-1.cable.virginm.net. [77.101.206.213]) by smtp.gmail.com with ESMTPSA id l22sm4206808wrb.4.2021.02.24.06.50.22 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 24 Feb 2021 06:50:23 -0800 (PST) To: "HomotopyTypeTheory@googlegroups.com" From: Martin Escardo Subject: [HoTT] Burali-Forti in HoTT/UF Message-ID: <0641316a-a1f3-856a-1579-2f244e5f80ac@gmail.com> Date: Wed, 24 Feb 2021 14:50:22 +0000 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.10.0 MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Language: en-US X-Original-Sender: escardo.martin@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=h2S7aC9l; spf=pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::42a as permitted sender) smtp.mailfrom=escardo.martin@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.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: , I've written a post about Burali-Forti in HoTT/UF in Andrej Bauer's Mathematics and Computation blog, which I'd like to advertise here: http://math.andrej.com/2021/02/22/burali-forti-in-hott-uf/ This is joint work with Marc Bezem, Thierry Coquand and Peter Dybjer. -- 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/0641316a-a1f3-856a-1579-2f244e5f80ac%40gmail.com.