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.7 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ot1-x33d.google.com (mail-ot1-x33d.google.com [IPv6:2607:f8b0:4864:20::33d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id a2ff4f51 for ; Mon, 12 Aug 2019 14:44:22 +0000 (UTC) Received: by mail-ot1-x33d.google.com with SMTP id q16sf84788989otn.11 for ; Mon, 12 Aug 2019 07:44:21 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=9DcFIsQL8AobprwDuHiGrLnC5iwFtifPm2kgTAipe7A=; b=LZAs8eD8KMN5jxfJJzpAhG3x6q4qsqzzYLJWtSRsrAazevpkCl69Do7BfrvEQ0dKOp fJEuLBWSvvQ3u0ccLP/K3l+lWtiCne4wS1Dm1g22AfK9nuGeclNiBfJFY3pbhhW4nV0M p4wYxmTqerloQrG0wiG1rX0PmhTABrpb8vQzPmYTHC0WBdBDVpYn5KSfgPrIEOT4CnNE nWnPHWunbMmCHufGhfbWQwgVptcTlpiFBt51m/feCggh6bdIAL6HHLr32l0fGhecy7Q0 RNYg0kg+V1Z0l9HNrpmDLgrhUcGuVZo3NaupZXCWoR1TDplVcHfJxqYQjl2DvPuuY4/+ 1sOw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=9DcFIsQL8AobprwDuHiGrLnC5iwFtifPm2kgTAipe7A=; b=ODQuc7iYk1oswdJ31vAa03RFEkOxvVxo2EcGsP2YhyaW6E4mV5M+yB+GK3BzG/YR6h /Kt+M1t2Tgcs8m9B3HAo/N9I8Yh51wD54j+hhsOCM41yyCgPoU4fWJvX44XcxUVVnjmy atzYciBlvqEKahnU2NlsfrfJWuhPvUVwtXPCvHi1nZGpVVTysZog4ftbL1xO63LF5ezM GeZydCfnJfVq1ocsaGHhJ0YeGnCD3ZyuCZWNcIVBK3KejrVfiIysmqkonJzqnxAoUFKo XxaHHOZ8Owm3GPx01/3sZbOK29c1KD7Bc30rAsoHpwwtrM2HBGOKvzrFL8eDgeWIJh+0 nOZw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=9DcFIsQL8AobprwDuHiGrLnC5iwFtifPm2kgTAipe7A=; b=tDZ9wnGjjhTFsxhig3QFVoWxuQ/ElQ9DQr+Zy+IjnN34eMdp3Hq517h0rPMFTk/M4Y 8Vp+i8G+lzSdSBUaUwU9u+Oldp1pgG6YxHZ6Zof7QU1MmD8x8MoF4bbHXKVLD4NAXmH+ 31OKmuOG8Y2R7D6jKPtQKgXHf0FKY7ZIotX5JcAV/rjO01i47r08ND1z9KFRGjv5h+ie jgB0jbiGbOPJGg1V1lGpdIfuGe/27MaUBTwLctOpBxfVqoRWdvTz1zc0iNITN1ytpBCT PCAzb6YhflzZCWK4sdkaOJKOUS4EjK7Oe6QgZ0E+A1mTr/M0f68xYrkkGeEy1ASu/btY KRAQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWN7AMEcbzeYLupL1e4Mh4AZ4lyqYt1YwhDp4PJH0/IijV/S1tU KIcsQlPZ+up4+/SBpPYC4ZM= X-Google-Smtp-Source: APXvYqyGYbUSkSsdjvxJd0wglcaYVG323+f2OHwazrGVP4wynC+r80inXn/2y9y+hPGhsGU3xtxXaQ== X-Received: by 2002:a9d:77c4:: with SMTP id w4mr1441613otl.40.1565621060267; Mon, 12 Aug 2019 07:44:20 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:36c:: with SMTP id 99ls984493otv.3.gmail; Mon, 12 Aug 2019 07:44:20 -0700 (PDT) X-Received: by 2002:a9d:588a:: with SMTP id x10mr30943867otg.144.1565621059783; Mon, 12 Aug 2019 07:44:19 -0700 (PDT) Date: Mon, 12 Aug 2019 07:44:18 -0700 (PDT) From: "Daniel R. Grayson" To: Homotopy Type Theory Message-Id: <61d38dbf-541b-4d5a-97f2-094c3f3c1da4@googlegroups.com> In-Reply-To: References: <9d23061c-4b7a-4d69-9c22-f28261ad3b33@googlegroups.com> <06e24c98-7409-4e75-88ee-a6e1bb891e1e@www.fastmail.com> Subject: Re: [HoTT] New theorem prover Arend is released MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_739_1951525924.1565621058864" X-Original-Sender: danielrichardgrayson@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: , ------=_Part_739_1951525924.1565621058864 Content-Type: multipart/alternative; boundary="----=_Part_740_517765002.1565621058864" ------=_Part_740_517765002.1565621058864 Content-Type: text/plain; charset="UTF-8" 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. ------=_Part_740_517765002.1565621058864 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Mike, what do you mean by "definitionally isomorphic&= quot; ?

--
You received this message because you are subscribed to the Google Groups &= quot;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.co= m/d/msgid/HomotopyTypeTheory/61d38dbf-541b-4d5a-97f2-094c3f3c1da4%40googleg= roups.com.
------=_Part_740_517765002.1565621058864-- ------=_Part_739_1951525924.1565621058864--