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-wr1-x43e.google.com (mail-wr1-x43e.google.com [IPv6:2a00:1450:4864:20::43e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id bcb7c6f0 for ; Mon, 27 May 2019 08:41:31 +0000 (UTC) Received: by mail-wr1-x43e.google.com with SMTP id g1sf7898918wrw.20 for ; Mon, 27 May 2019 01:41:31 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558946491; cv=pass; d=google.com; s=arc-20160816; b=px+KUWVDhwBC0jYkMwkgw8aMKUfvOdoizk6MhFcpXwtx0nBqmobYE1M0R7nK/9oJnY cBm78Ddx5MPR881sfm/SalLM0wPvLAU7J1DbHNqWcV9h7FZPPxNlbH/FUnBARVaq+Ol3 UyGQz6UA6GVBYbk0nij0othDp+QUwVllFEGfLn5r6/Von/sJhe3pqK67ZSJoyAwrfBiJ vgESB0KgYlj37riGM07biXbzh6vgT4nn7Jwa1mNqhgbYD7axFU+9v3jbpIMcBqBoNB0e L1ypTjO4nJr3QWaP4XLwyk7H3YxA/pbhhep9lKo2MI1wQZ/ntEZXlbFbxFDmVPWw58Cq wl3A== 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-transfer-encoding:content-language :in-reply-to:mime-version:user-agent:date:message-id:from:references :to:subject:sender:dkim-signature; bh=VCSIgTQ2jBvEgN2PBZBUHtOmII8uRMbwM98OvAINmK0=; b=ec78CQUGmOCVueFmwP7LXt8NkkZxk/jA2jPP4p1gKetmvoXNJA3bPXDVu2NcA6oPZC muDRcglNxQ6uvpUpBScbr17vze48SDE5TvQDjFoHBfWZzQodzaBBaKP9VYSrHbZEwJtJ FONHobjtZNcrsjrvJbWzu0mYZ9Zin45ccXcOlLBx7pdhmAMnEpMxAWs3tCxg4ws6H/IR rKnxOfdMgnu0ioJFh9YlGP+gqNLnefk4krE41/XuUnr9IwknvACSfrDM1gsWiGeerE3m 5RcuEZXgneyuXdX8xYHYp6eAqo8afu2IvukSDf1vJfFp9rbiD/Wko0fNDp0sTQepGNgq ssXA== 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:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=VCSIgTQ2jBvEgN2PBZBUHtOmII8uRMbwM98OvAINmK0=; b=nk+q+KWdjKLJofFJs8Z9H5JI52ssI8Mt9ZbSfbhFSR7iXH5Hl/MgRXDWa4gGWTmQ90 Mqk5lOydUL1iKnSf4UaXKqoowlnPkSivybFbgjt2VJFC0X4oaZ7ExFxzi+HM3PhzUYYc Qnj8eM1gaGtao/yvqa8HCnu1OTy0RlAHhcdwrK6YxJqTmNhFmMJXehPxNSsm3t6ZdAmY wqA/38108mOPX7xfmPNJlbLBJv7j+0gTj8O2utotJ3ksxImGmeK/vQYx+JicnaBCKeTc 5mEyLZ234B5Gb+OyMemyewxnDMq47qhu42vJxl5c0GzWajy1DgLPfsd9mewIQv79ZrdJ l1lQ== 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 :content-transfer-encoding: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=VCSIgTQ2jBvEgN2PBZBUHtOmII8uRMbwM98OvAINmK0=; b=VzP/E3q/1bBbN20iQ5cJUrFFi3tdggxpHP8mL1fJZoRdq50j7mcHO4YziiM8Vagxzo zVIe27I67tonjhdXfL4ghVjn0kWefOZvXguXPi7+FvUTyiO0QfxH43LNwN05fBkRQhsu oxG17haoSW2ekvdF6FsM7AB7Nzh9OQeAIAt/3k9nUuY3lG6UxJu1CVd1vzvKUxcEbn2V WmGyNyNuIEOxdMZGuGV+CsnjowIOK/ErAerVk1VGDcCY5IwiT+wT6bWp2MQnOh/S9cmR V8T3bkqIMTPlUWEyydfOAfGkd+4NMfXZF8Mke3H83soIVQUy+T7xmuPgsmkSR/4lIBzX hajw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUkK/Jc3sc2tCvNHsAsUziIxyvYCOw1fECvAkb4aFDAl25rSjZR KZli7PFiJ2VvpcVNNN8bCX8= X-Google-Smtp-Source: APXvYqwEKxPu9y/S47xtcKV9k5W3uoyX0/0BD4ZJfn4GwKvFJcp5Gm0Hw8bt4kG1sOXuEgvE8Xlj0w== X-Received: by 2002:a05:600c:2058:: with SMTP id p24mr24343659wmg.42.1558946490950; Mon, 27 May 2019 01:41:30 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:6342:: with SMTP id x63ls4701439wmb.0.canary-gmail; Mon, 27 May 2019 01:41:30 -0700 (PDT) X-Received: by 2002:a1c:2e0a:: with SMTP id u10mr8094216wmu.92.1558946490077; Mon, 27 May 2019 01:41:30 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558946490; cv=none; d=google.com; s=arc-20160816; b=IjJwkAF0hqhfeqE2ZKe3J1f7sQNj5i+NSiVDy/Its6N6swBIQ/WJXudHYALeEcQXZ8 TSeWvI3D2rdGwlM5M5UbxuDJXI6VMi+aFhCT4ogF4aVTC1MhyHG5+wkbdcrTKnfqWDxp a52QgyjTc4gJlZhRlIkMHo0snt52OCFW1JL1os2vPrsFQHhNr/XF+SEFVoCE+5aWfvPJ eKcvUKL8wpjjNIn91yoMRxNY6b2MOEip7mmeTJ5fndMcDxCNokcRNRS83Ckv8Recwl/y B8WBGg8eHkyqF1COoqnecAoBDSeniqo9PvmAHaN6jIJv0WHNnjYkbrxN9SYjWssaxT+a XCrQ== 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=+/KaZu/psgfnkCcUIK8+kwZxpCWl8dmc7yC4LS+pStc=; b=HhygxHsGGml42UWJcHHgYGV04XjjzJ6WZQXT+CsA1smJ/1etJvNlIL2OHtRd3Cmkgs b3/1UhOpAVcLPhjvvda73zm755XoHtHMiTE7/5XbDUVdWThWgXlEZP8uosQfOc6+DtCk 9hD+6mU+YzXA5MQYEzs4K4vXti1Wai4yQ9aTnc/fxnot1gz2/G6c/NYX+PiOqcW8uvge zDoyje3n0rB2SC4xal8j3HySK0ookuzxydUemKick0FbPAJqVeWn7XSBwoBjCokwd/9m cvvlHttSTRJwqa4+kdJzZWRIlguc9Z22J1Ng7WqNKWA16wCkL9n5nzd4z3qtyxaVIo2+ pebQ== 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 j18si482039wrc.1.2019.05.27.01.41.30 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Mon, 27 May 2019 01:41:30 -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; Mon, 27 May 2019 10:41:29 +0200 Subject: Re: [HoTT] doing "all of pure mathematics" in type theory To: Homotopy Type Theory References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> From: Nils Anders Danielsson Message-ID: <0e51ad31-29cb-d054-5e96-1544732f47eb@cse.gu.se> Date: Mon, 27 May 2019 10:41:29 +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 Content-Transfer-Encoding: quoted-printable X-Originating-IP: [129.16.10.245] X-ClientProxiedBy: stark.ita.chalmers.se (129.16.226.131) 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 25/05/2019 18.41, Noah Snyder wrote: > (When I was using Agda the situation was even worse, things like > pattern matching secretly assumed k even if you used the without-k > option, and HITs were put in by a hack that wasn't totally clear if it > worked, etc.) Things are a bit better now. Jesper Cockx and others have worked out a better story for --without-K, and Anders M=C3=B6rtberg, Andrea Vezzosi and others have implemented --cubical, with direct support for HITs. --=20 /NAD --=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/0e51ad31-29cb-d054-5e96-1544732f47eb%40cse.gu.se. For more options, visit https://groups.google.com/d/optout.