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=-0.9 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-vs1-xe3d.google.com (mail-vs1-xe3d.google.com [IPv6:2607:f8b0:4864:20::e3d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 309247f5 for ; Mon, 12 Aug 2019 17:33:00 +0000 (UTC) Received: by mail-vs1-xe3d.google.com with SMTP id 66sf22757481vsp.2 for ; Mon, 12 Aug 2019 10:32:59 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1565631179; cv=pass; d=google.com; s=arc-20160816; b=OHCDSX5TRFSZJN1zlt5TrOncDZIe8252wKN72+dayF+kK2cuXQplQxvXIXu5vp3VtR fC8c/UEkdtmZZVNbibw4XkeRFFF8lnJCOtvXQpKpp5QODoRIDSRTrL7cFvT0BRTXQXXq Z63Vagcduk9xuPeRImSKAAEDdFpnDE0Kv5yQMgWWPdXU0wtH2cKzLy6yoe9Uyv4gtu8w feTAiHHTxpGd2JVslop0uhvATqT0C8i3ph+3sRCoDUUoVBy6dOPvRQKwxtztf2kbe96Y 3j311NLRh2swNSx75UWHH8BGlbdqudxIjtVy0FSgTO0bX7Q71OhhESc6GcJtHr4G9jlo AOjA== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature; bh=Dpn5Y7kagI+FIwg/FY4dAl2VbZaFi0b0dtNpA2eOP18=; b=wputPEJbwhtlbwlWuilcaDw3HMwEHZqNjTXTOEkUR0P8aZPJmen5OnYgG6X2XT3RFG Y0w/mAYfJhYxryJ9A5ETALHyOgIWBa78DHRxyKNQyp/pQP5DQUVgqNzs9LYcIJyGXiiv 2AOqIn8X5JeyDQZ44ldoBEpOXtc1h4APq5ffm8kpf4dmKv/h2hLQN/n4eXs0rVTqto4M BDUrUsAeazWFsBORclCb133Bx3ON0kkuHRmVlRpe8AYO2W7nDoP4eZRixfHPZOO5JBFj H8G0ITpBJcpUxZj/1VrJD51YWavww/KCIMzqYDx4mcUgZcB6KZOE9rwpPLe8x3bg+1Ly Uy5Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=kXZcXt8L; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2d as permitted sender) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=Dpn5Y7kagI+FIwg/FY4dAl2VbZaFi0b0dtNpA2eOP18=; b=deAKOGdQu+x0VoIpczh1FuebnNP7wiaILtw3UR8hXFJ+5YMN4FJIqO0fvcBFoDY3wA Nog4wwBmLuK+zP+NxoEgQ3v72IU3s74yVzbcyxc4knNgg6UlrYJ4/6Y+m3kFH/+LJooB nAInIDG2IedxuWGoH1pYrQlpCw9PApGOYr4YInEKdtsmd/mBzRnajae4m+Mvv7GRtav+ 3vsl+9fy1SbNhuLLIn7m2/V0jneNpc09EPyelthEB1QqiMKy1xAEf35PIt2jIW80QDMb eq1gjy1zT8KYk4Pyho0826U+fHVoGH9uE3gKIG7DXMB86XizTAG5CfECJeef0JdqkAVw eGnQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc: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=Dpn5Y7kagI+FIwg/FY4dAl2VbZaFi0b0dtNpA2eOP18=; b=udIdF3Qd1hEQz9SjqJ7d+ICEaY2WzP0OjKyO2BKdm5bqZsq5Nj20mz+Eq9swiVpZ7r ECILZcjdrY/2spKwS07S9BD9eSFHPOeIQNH8LJqiStICUyZS9h7s0WNNW5BD3FLLF7Ey q3MTChBzCQWqsBXxICvUld+5fpmzl5h8PAN5JOfzSxCle9QDgF98RldPvGQH6JWoHRYC KbiLGJuVziO/oH40Q35wzm3mTWhlBLwp6EFH1MKON3lYUXfAI3b82A+1AvKqzj66cnzS LWTUKAC7c04gSzxwy82/o37Q7Gfuv9vFsmvwfDkuwnq4RwXDN2iHS8WX7azh6QMdDjR+ YKEw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAX+0BKTyqOcY7xUmkWpnM7NFRe7rVP1c1sP+YWnmRV7ULA+kwE5 iad+JEPUxDlq5chZAZ5Q6y8= X-Google-Smtp-Source: APXvYqzYAWsUbwR3WwZyGClFqeKLq7PYnhaqIrTjZRE3bXLm96SJ8IzmyZLTgl67Tds6IqNDfYsLkw== X-Received: by 2002:ab0:240c:: with SMTP id f12mr2902176uan.97.1565631178861; Mon, 12 Aug 2019 10:32:58 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a67:8cc8:: with SMTP id o191ls13040643vsd.15.gmail; Mon, 12 Aug 2019 10:32:58 -0700 (PDT) X-Received: by 2002:a67:fb58:: with SMTP id e24mr9503807vsr.141.1565631178567; Mon, 12 Aug 2019 10:32:58 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1565631178; cv=none; d=google.com; s=arc-20160816; b=ZOF/AaCCvGxZpBDiKq1UAav7WHM1AkzM5XgyGtTTcvvmSrNA8KudCMy46Q7ulwki4F cRbdDIOr92CO+BMOSI6yhy/BIOqQYoBS50bClrHQR2KdP/CIVXm5BjhKNWaUbHTMMPBr qQj010aJh5zmZzvbKhbTL9o7ieaCrmTr2zRENN7PpgQuYvJsP1GX/iVuYFj/DzGTg1cW 5akNnHAgxGlHuCu+PtY8kSQi7Ku391RChMpnHVHh/61FZX/yN97vK9zk98jbbhThEJjx KF/7BKp9CI+jKqw9R6+y2j1o2X/UIoAja3y5wHr/yGz7LAimD6nOHfbEOb6wzNnez6Du 5/cw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=4VUtjQEA/62eCWYJ2sDcuojRUTGCp5ihkXmV/S8F1YQ=; b=WixY4oYSMyviYvbxJKvSkT2APw9POSjOLj0xZLsnFXhq9umK+v81+tSQ00Rqhyip0i qvqNRLt682Ai4hlVx1TKMTFxZh+Bp2uOUihypSrKcfQWVj4oKPRfAcwZLFMjRk5gmL2d RYEZ+fEK32fHDv14fE0Zps4pSsKSspCfOKtw0yKWvTlCPWw7ceMn4S1eghKouRZ+TCSN ML6HqZhdZMkN7YB91ZzCiPkCBY2Pqq5tXKh/2lkre7fCt2PwSbTvh2Jk1gvURV+CS9g7 MWC1SXkKmq/FI0bsnsnpeOXJXTHRsBDEuro1P9TfBh3PKOXqbz05YsrpNP/6UFZGdJ5s h66g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=kXZcXt8L; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2d as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb2d.google.com (mail-yb1-xb2d.google.com. [2607:f8b0:4864:20::b2d]) by gmr-mx.google.com with ESMTPS id u189si7098388vkb.2.2019.08.12.10.32.58 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Mon, 12 Aug 2019 10:32:58 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2d as permitted sender) client-ip=2607:f8b0:4864:20::b2d; Received: by mail-yb1-xb2d.google.com with SMTP id n7so4134999ybd.8 for ; Mon, 12 Aug 2019 10:32:58 -0700 (PDT) X-Received: by 2002:a25:aa74:: with SMTP id s107mr8181888ybi.437.1565631178093; Mon, 12 Aug 2019 10:32:58 -0700 (PDT) Received: from mail-yw1-f53.google.com (mail-yw1-f53.google.com. [209.85.161.53]) by smtp.gmail.com with ESMTPSA id a13sm3580078ywm.59.2019.08.12.10.32.57 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Mon, 12 Aug 2019 10:32:57 -0700 (PDT) Received: by mail-yw1-f53.google.com with SMTP id f187so38922287ywa.5 for ; Mon, 12 Aug 2019 10:32:57 -0700 (PDT) X-Received: by 2002:a81:4607:: with SMTP id t7mr23067386ywa.246.1565631177078; Mon, 12 Aug 2019 10:32:57 -0700 (PDT) MIME-Version: 1.0 References: <9d23061c-4b7a-4d69-9c22-f28261ad3b33@googlegroups.com> <06e24c98-7409-4e75-88ee-a6e1bb891e1e@www.fastmail.com> <61d38dbf-541b-4d5a-97f2-094c3f3c1da4@googlegroups.com> In-Reply-To: <61d38dbf-541b-4d5a-97f2-094c3f3c1da4@googlegroups.com> From: Michael Shulman Date: Mon, 12 Aug 2019 13:32:44 -0400 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] New theorem prover Arend is released To: "Daniel R. Grayson" Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=kXZcXt8L; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2d as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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: , Maps f : A -> F(A,p) and g : F(A,p) -> A such that g(f(x)) == x and f(g(y)) == y, where == means definitional/judgmental equality. On Mon, Aug 12, 2019 at 10:44 AM Daniel R. Grayson wrote: > > Mike, what do you mean by "definitionally isomorphic" ? > > -- > 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/61d38dbf-541b-4d5a-97f2-094c3f3c1da4%40googlegroups.com. -- 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/CAOvivQw17Au6b1P6FwxZF7x84qM9vhCgOf5xuKcdzW59_F67Ag%40mail.gmail.com.