From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.2 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,DKIM_VALID_EF,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ed1-x538.google.com (mail-ed1-x538.google.com [IPv6:2a00:1450:4864:20::538]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 8370c721 for ; Wed, 17 Apr 2019 22:59:41 +0000 (UTC) Received: by mail-ed1-x538.google.com with SMTP id f42sf266622edd.0 for ; Wed, 17 Apr 2019 15:59:41 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1555541980; cv=pass; d=google.com; s=arc-20160816; b=gPrtrZez1NnIFzeWMjdf+TT3qhsvjeEfhzrDx8E6Rat2mceJaTx6wXA0gHygFWHun5 IZ/tmxSm2PD9Gj/cd3nfeaL4mjSaWNIvx9phgPaydEkp0aEww+THAa/n5JCiCHvJGdmb PivOTaBpQsv4XhNEgQw8jRy7qkcrVSryH0cUPjreqdGEhR2SPXiEapDHYnVjYypZJYFY NdbZ0IOHljoJjuVQU7CMy9puPjXun5yq/FYGdcZbJccsfoO6rzrn5m4HsHGSXe1c0VSc 6SrZYRRKtH9Hm6hGC8HXQd7XbhUxzna/4H4tx4dgt+jFJDK7Koa5F/vAYBflM64kaTnX 86VA== 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:reply-to:content-transfer-encoding :content-language:in-reply-to:mime-version:user-agent:date :message-id:from:references:to:subject:dkim-signature; bh=3pAGvlT4MuVWZoF1mr/QebZ5pxGEMvaA51XykIFFKXE=; b=o1GJACzLuMeKz09OrfEuCymD9K3S+NDPsInuzSGnMp/8ektWgKqgcVoJTZvxOA8TvU aXlGTjBCItWdgTlG0YBoIxM7xmlq/aWd3YwLB74dCrqtw0aS4a3sZVuV0UuL4o9HPPLe 40lXuN5lC1V7TrhP/Xsgr7VzdpbZJon7Mz0CzCw4DB9DcgZF/zDee1UwH1g7dlz5WGjq DQq3kXqY8kjxuRNNrhRZAIxeEFOUjNpK/5fEQNRx4L/SVoIO9YurSjwb5kmmFWdDKGO3 JJQjVui3CU7FsekDvJQj10B0bayJehRLKGX4gEZV08q35hzyHS/TVQGnEs88qpRKKowM +lXg== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo.martin@googlemail.com does not designate 147.188.128.137 as permitted sender) smtp.mailfrom=escardo.martin@googlemail.com; dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=subject:to:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-language:content-transfer-encoding :x-original-sender:x-original-authentication-results:reply-to :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=3pAGvlT4MuVWZoF1mr/QebZ5pxGEMvaA51XykIFFKXE=; b=L41r7je957I5I0xi7BUO6WKZQ4ZvACAUDXjEivsl08fGyKLF8czFzAB0EHVOGBLMKq atqwRcp8kG8isOMIfz35m98tPuFrGnYV7K1SSAnvlhrrAsQQFpzCQZqb70JQZuWyg2UO ePZVodGEWbeUB5ezL2ggGb7OmiDgWx/Dnpf/YUsOnXwbAcZndD6L9GSdw4NBBlwYdZFY +ohKGRG4j+yhMOka+GNVNGripa/v7rXuv4PNGoVCOkwGZ82ldpGpHLPkTGTAw2eC1dgn A+jtGmEMB5i578valx3Jz4+3nAJ31RdvyD/IYetjH8Mfe740+RB/p7zVSX6G0eyOJKr8 DvdQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:subject:to:references:from:message-id:date :user-agent:mime-version:in-reply-to:content-language :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-unsubscribe; bh=3pAGvlT4MuVWZoF1mr/QebZ5pxGEMvaA51XykIFFKXE=; b=JbcpwJHh0fli1K2u7WDCjUytbKmiORVC3eWzICY+JjxkY13wHIjyu2wF0/hSP8frXC vdCRZogmb/VlPvYX80umg880zPeAy2VxiUlgwICf6lZTgtovP3yavniGDzwQDpOlf5oI VuIekVwcrwxSwKs7UEMLfkVacBMc+i4ACafYj3LD1PaLQsBdwG/kY7zrkMid38Wc9R2t sSGm0QdoWtv4Iq8/QnBz4F8FGj4RY9HBE/XLLSZtsteKoy7paotxTo058FEa1pANGDCu o9sSzfSCKkRHuZI+ofZLKZg7JGbCCs8usxi74ifKsmAcJsZ2o5W0+YolebZATl6ooWDz r8MA== X-Gm-Message-State: APjAAAUsM7pjyLAKpJOSTsv6z4IV6+ZzmlI+V+VDv25u14kvus8UmRHK 4bUvrQkhK/7AHBw57ZNIOBA= X-Google-Smtp-Source: APXvYqxkz3jnTDKmi/znOiHz85YJSfNVVoYS0EzDPwVtFpoTiVCpiFiMJKM54ock9GsuIGZT1EpbRQ== X-Received: by 2002:a17:906:1c8c:: with SMTP id g12mr49526978ejh.97.1555541980478; Wed, 17 Apr 2019 15:59:40 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:bc06:: with SMTP id j6ls37784edh.8.gmail; Wed, 17 Apr 2019 15:59:39 -0700 (PDT) X-Received: by 2002:a05:6402:64d:: with SMTP id u13mr13575879edx.218.1555541979784; Wed, 17 Apr 2019 15:59:39 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1555541979; cv=none; d=google.com; s=arc-20160816; b=B8FvbsZ9seJPTYsh883wMlDmz2pbFOI0op6UKLkDsSoHsoXbBGRysNB4JNkYsiZsv/ 8xuwi4Ec4e/AM5V/JfQucpryMHjSijkfyMG/dM26kmv1uVBCw2iza33iGniketQtaXBN SwrtYZVCLBYb6V/2DFcLNl9pkygWDfmYBXYx2/h3nbMLGzl3DvggG32NXQepC5/38YVQ wb3IjrqVsbvfOc1rnqAjV2i9fEOkAsODYWJsMaki2p9Ir8XWijJr3gsJHqo4t3KAzAbO 5C1Ia5tWptk9AeczLjLJ/NW4B6rUwm6GxoM4zsD264uXfz2a2pn9j8kYX292fWXdoY+h vh2A== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject; bh=OfV0VyAkk+tuvQAM8cDmFmX+SCucnL3h/KE9iw89NeE=; b=FwmVlmBakczdvh6/lBAVeNF23BqBL4/Sz0BqMHFdHpq6Nhq8wHHyiX4uhxzbFJJaRk nrZ6ldDLEHDHE4Kojs5JJ74s8JROAt6ACnzHudbq/oJhoqF789HYtxw7gEHa58+Ns5Yj ACRabm0h+9V995ye2HNtGThOugt9CRH7m8Oy+gRkSVT4b8qEYh6yvMDGV/2w2aCWwcbq LLiSb7ZN+NJJWw0CL6rzxUgVjy7VvNoKIkceVJP1chchXtykyqq+E2RiZvpLRrreJ9Rk r1pne0TRJ3Nsi8Yp72xY6vg3/qMFrqSHLgUSmmbjMWsm1e4Ws0i76hxT4L5BKvwmWbiK BBxA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo.martin@googlemail.com does not designate 147.188.128.137 as permitted sender) smtp.mailfrom=escardo.martin@googlemail.com; dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Received: from sun60.bham.ac.uk (sun60.bham.ac.uk. [147.188.128.137]) by gmr-mx.google.com with ESMTPS id a38si28070edd.0.2019.04.17.15.59.39 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 17 Apr 2019 15:59:39 -0700 (PDT) Received-SPF: softfail (google.com: domain of transitioning escardo.martin@googlemail.com does not designate 147.188.128.137 as permitted sender) client-ip=147.188.128.137; Received: from [147.188.128.54] (helo=mailer3) by sun60.bham.ac.uk with esmtps (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256) (Exim 4.90_1) (envelope-from ) id 1hGtWl-0004bl-O2; Wed, 17 Apr 2019 23:59:39 +0100 Received: from [31.185.238.44] (helo=[192.168.1.93]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:ECDHE-RSA-AES128-GCM-SHA256:128) (Exim 4.90_1) id 1hGtWl-0000y0-Dx using interface auth-smtp.bham.ac.uk; Wed, 17 Apr 2019 23:59:39 +0100 Subject: =?UTF-8?Q?Re=3A_=5BHoTT=5D_All_=28=E2=88=9E=2C1=29=2Dtoposes_have_strict_univalent?= =?UTF-8?Q?_universes?= To: Ali Caglayan , Homotopy Type Theory References: <655fcacc-0d88-47f7-bcf6-3a0e27ea10fd@googlegroups.com> From: "'Martin Escardo' via Homotopy Type Theory" Message-ID: <7724b923-fc14-0bd2-57b6-ba341f5641bd@googlemail.com> Date: Wed, 17 Apr 2019 23:59:38 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.6.1 MIME-Version: 1.0 In-Reply-To: <655fcacc-0d88-47f7-bcf6-3a0e27ea10fd@googlegroups.com> Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: en-US Content-Transfer-Encoding: quoted-printable X-BHAM-SendViaRouter: yes X-BHAM-AUTH-data: TLSv1.2:ECDHE-RSA-AES128-GCM-SHA256:128 via 147.188.128.21:465 (escardom) X-Original-Sender: escardo.martin@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo.martin@googlemail.com does not designate 147.188.128.137 as permitted sender) smtp.mailfrom=escardo.martin@googlemail.com; dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com X-Original-From: Martin Escardo Reply-To: Martin Escardo 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: , On 16/04/2019 13:06, Ali Caglayan wrote: > Mike has released this new preprint on the arXiv: >=20 > All (=E2=88=9E,1)-toposes have strict univalent universes=20 > >=20 > Quoting the abstract: >=20 > Thus, homotopy type theory can be used as a formal language for=20 > reasoning internally to (=E2=88=9E, 1)-toposes, just as higher-order logi= c is=20 > used for 1-toposes. This is awesome. Perhaps it deserves a short explanation (or at least listing) of the=20 crucial steps gere in this list. Best, Martin --=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. For more options, visit https://groups.google.com/d/optout.