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.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_DKIMWL_WL_MED autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ed1-x540.google.com (mail-ed1-x540.google.com [IPv6:2a00:1450:4864:20::540]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 70003b35 for ; Tue, 28 May 2019 10:13:18 +0000 (UTC) Received: by mail-ed1-x540.google.com with SMTP id k22sf1349660ede.0 for ; Tue, 28 May 2019 03:13:18 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1559038398; cv=pass; d=google.com; s=arc-20160816; b=pQmo8alGko+EGRTMmeITpVyw8TdeZLGxZtGHZeExQhosqYDAISDXGWGINB3nkMU8Pe zB/NFmOmX00/GjNID5oR9Sz0+X93se2AwkOsd0KghiSSZSaK4Hqmj0q+cSnoBNm+zycJ Eh/kwyxQ2LaVhRtbRM0tnA+OASgtsblZBVixXT1bCk1E2FlOHbaRfFeKkIr+1LLIVqLs AmBLL+jyFDhDztq5KpDlqXgZy3UDu4YTfMvVFWMOUEA1xuv2oR6ogywxQsVzxRXk7l7S 5+8LyNFD/X4VxLF1Q9Ka1jFmo9jT+TDHCeCftZCC1t++DadkQJIRp0NJrxxgM9lZOhbC wfaw== 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:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject:sender :dkim-signature; bh=exffetDaHQ2b/jSzO7hGWooOPOPsC4Vj7P/w4tGy09s=; b=fe+l6GCXy7Br7h7i+2ZVVJ4E9Wr2kMeMtGDnpifGsyg/UFgRA0fJKFqDWkWbl1xbY0 1gLclQBw+za+qDRKabaE/L6H+DLjED8vcXT3hWgEZLVwirIO+tqvO8THbNM3GkIRP5yt 37Prs4GA44tWfaFICKrgagpkDPYdgcXZCQAHDrG0dqlQarI7jO6uI436WQeCmcCncX/u yighSAuQAH9TRNnSHpPmTwlS4VV8kaTmBuNcwdqT6WVjAxK4ZWUF9Oi6GP00ffDfMbKG JIxz0a2DL8zsgS0DH2fKklGNont1KwFi6iAEM4Dz8C3jdEW0Dmw0nGoyJg5gp0Hpwkwo PQ8A== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of nad@cse.gu.se designates 129.16.226.131 as permitted sender) smtp.mailfrom=nad@cse.gu.se DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:subject:to:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=exffetDaHQ2b/jSzO7hGWooOPOPsC4Vj7P/w4tGy09s=; b=WYgYuhwkJtM72/vRWNco9EWHAZoLGuU4sJliJEj/1fvi12QxOd0FWEv7dRwILExsuJ cq/9M9xnOhTdpmg29J5QAV/p6j3l2vgbVBrIiFzHhDV062ruGlDQo8bo6/bhAAKFm+v5 ftpvL/uEh/gHqCHiZId06ItGW80MKfzvf0tttYATPTLnt7vauxky6pX9TKjnzU1wm7JS 1ztnaBcHkcflmernrV+DIrIuaLJSf1p+o3tE83i+xdYvoKUUF/MrGDjqgCEdme4F++/I u79on5ZzcF/JgfKRs5TOJNbq9BjN6nPyF+1LBUKNfhS3CyMzDHw3g5iRgxR8ykAuv4/b HYeQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:subject:to:references:from:message-id :date:user-agent:mime-version:in-reply-to: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=exffetDaHQ2b/jSzO7hGWooOPOPsC4Vj7P/w4tGy09s=; b=pr9tScelKEPPaKN5kvUCJfSWvTYqLFqYekhXoD3DCB+7C2GwaHpGcY/ntTpg59EjYk Vr1nDGpmcGIRXU70kz5C9oLBVIbvSHfL+6SV/BwOVjJT5ZSN4dbJ4mthLTke5Y2oy3oH owLgZx+SWFv7DMRrqgZK7wBeFquAhAMQjl/8mOB0yULbHN2etZz8mfgCIYKYMlHjkF+h gsUFFf3GEn5XteFJ1nS7KmQ3xIumRlVvyLW5F0xoq7rZP6EKiho2v4tK2w9XYK5+JycJ GE35s9bivFBLAjpTrOxXofpAgXsuLIf+qQcRSRVfltExd/mdR6WBxr1QuFVODb7m1Hxy ablQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUbDHkCTBD5MvnECsGe6gcJoXamLaAn+TV48jXHUpNIVSoX0jQ8 ig4rsyYkhxRBdw+20StuVFU= X-Google-Smtp-Source: APXvYqyyQ01tPqMVpsyvkXzxU6VJUXFR6SBkBFgOc6fz7i0L3oyOYudCp+BW3JSGvpFA0xlFvbypYQ== X-Received: by 2002:a50:d717:: with SMTP id t23mr71185794edi.248.1559038398290; Tue, 28 May 2019 03:13:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:4a19:: with SMTP id w25ls4487696eju.14.gmail; Tue, 28 May 2019 03:13:17 -0700 (PDT) X-Received: by 2002:a17:906:61c3:: with SMTP id t3mr83428947ejl.273.1559038397863; Tue, 28 May 2019 03:13:17 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1559038397; cv=none; d=google.com; s=arc-20160816; b=M5iIDMQoZy9zp75rkA5AOy1o6n8kexwZVSz+5ZGnZLYSuxE5x8Q6soCFD3zgsb1UEO kWuc6U9yulIGi4z8FHRGqdD57yv6nwU9oA+05Df2cguOxtKke3kUhM0FarWiPWDvmxpi z9af27/fjMr3TgtcxSmINnPVnqKvD9t1MFegT5uJynXmHn8bqarhFah0SL9G4PXFl50d fXz5Gh6NellAegAN6iL6H9lXooDGP7vakb/Eb3ep13ohorVv59FJcPO/uDM15qqXELxc XpKYGKav8UCRf5JO+JlZXHZcHZA/N5WNi8UGWp56+cVRfhiz5diAMJ0h/bFE6RieX3mP He1g== 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=1JjLnp0HxoSqTxiwYz1yo1yEoaVikRgzbiz+gPlMkZg=; b=GI1VQBUZ//R0mc+NkJbsBBfJYV0hiTmvipAh1d/T+jD0Y4im2Bh6yfzbZCeRyLGCxt VZdQvsxd1Nn9X/xDUxu95NLCQpDJMEHhv0HKJ8R1rWoPEE1+hzR5nxhlzpApg9h18Y0D Qr5Y5xFAiXx4XSnEs6nWzHxBIMZnMnMBX4Mv9ikFr1E4RxjHa18YOjMLPK/doXwshsDa gmSwMuhsUtaRGOlB9njrHrrGColuCqDvmkuuC1+dgPSWnL8xCiwBER931OJXaujaQwS+ EdDnCPG2jhCJ/HZ3ABYrJZ3CMSlXMGWf/TAuwQHyFszpqkZveWSSI6QVPh/wus07dCt4 q/6g== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of nad@cse.gu.se designates 129.16.226.131 as permitted sender) smtp.mailfrom=nad@cse.gu.se Received: from stark.ita.chalmers.se (stark.ita.chalmers.se. [129.16.226.131]) by gmr-mx.google.com with ESMTPS id h25si464322ejz.1.2019.05.28.03.13.17 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Tue, 28 May 2019 03:13:17 -0700 (PDT) Received-SPF: pass (google.com: domain of nad@cse.gu.se designates 129.16.226.131 as permitted sender) client-ip=129.16.226.131; Received: from [129.16.22.134] (129.16.10.245) by stark.ita.chalmers.se (129.16.226.131) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384_P256) id 15.1.1713.5; Tue, 28 May 2019 12:13:17 +0200 Subject: Re: [HoTT] doing "all of pure mathematics" in type theory To: Homotopy Type Theory References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> <3f6331a7-688e-570b-01d8-d02a81eac96b@inria.fr> From: Nils Anders Danielsson Message-ID: <9232f85a-6d64-84dc-a2d0-290c0fc6e760@cse.gu.se> Date: Tue, 28 May 2019 12:13:17 +0200 User-Agent: Mozilla/5.0 (X11; Linux i686; rv:60.0) Gecko/20100101 Thunderbird/60.6.1 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: en-US X-Originating-IP: [129.16.10.245] X-ClientProxiedBy: arryn.ita.chalmers.se (129.16.226.138) To stark.ita.chalmers.se (129.16.226.131) X-Original-Sender: nad@cse.gu.se X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of nad@cse.gu.se designates 129.16.226.131 as permitted sender) smtp.mailfrom=nad@cse.gu.se 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 28/05/2019 11.50, Michael Shulman wrote: > More modern homotopy type theories, which are generally based on > cubical structures, allow univalence to be "executed" by the system. > However, these systems lack (so far) all the intended categorical > semantics (see below), and haven't yet been implemented in "real > world" proof assistants (though there are prototypes now in use and > development). The latest release of Agda can be used in cubical mode, and supports both univalence and higher inductive types. (As well as things like higher inductive-coinductive-recursive types that may not have a proper explanation.) -- /NAD -- 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/9232f85a-6d64-84dc-a2d0-290c0fc6e760%40cse.gu.se. For more options, visit https://groups.google.com/d/optout.