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.0 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ot1-x33a.google.com (mail-ot1-x33a.google.com [IPv6:2607:f8b0:4864:20::33a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0e035e80 for ; Wed, 20 Feb 2019 12:05:23 +0000 (UTC) Received: by mail-ot1-x33a.google.com with SMTP id q26sf6936846otf.19 for ; Wed, 20 Feb 2019 04:05:22 -0800 (PST) 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=VxFHWZpjBaMg9Q8WcoD/wD5cJWkm+8GmIBRXN/pGLY4=; b=pgkI5J3gytKqkSOj5EvnUyjdDCDUqWPl+kVH6vEpDjkxmYh+1/BbIC5l3iMbW6wdOS mhAXP7J5Kad8eTDeQl4Jnv4FIvLhq5iAIqR5homs6B21mDxLy6Ouy/5jad6D+/VZ54Hu aD9FByfHEsnkB71B3p6W8qUdyrs3uStThXRW97LzTkQPktIC5kldKpHNLz5l42+nnauh 5D15McWMz9evAlrQq0agSkLpyYs8hpEK/jCW/KbM7sPP5B6IuP35rin0Ifwa+zawZQzh zf2N9G1ZPraFSQZZm22QxaEB+i/Tu+K9m65qzlPipXTfO9ZtJcQFaPIR44xonck8/mce scAQ== 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=VxFHWZpjBaMg9Q8WcoD/wD5cJWkm+8GmIBRXN/pGLY4=; b=OaOlIr84EWbXnCkV/WL0cXoE5zb5kU49J/vHdAXxKkoXecAddF9DiRN1Y5m1lFoSuc A1U50fzPpHkS7oTgFPnNqK3kHz0+tBBEUV/M+oGV5B2WDFRXOYa30lLq7pbpaIhX2OKu 1jbdRxKmNVsm99YZKMQA+mqXUoSo53Q+FSumJ4MevXJuCzmwpwC7APc2sptv8GaNf8Ci oUsiD2ZXz0yQla4glf7eEEf428E6axeujze9+rc0ntlSd/Q6j7KV9dwwRZoMKqSgeNFz 7MsfJdgZNkt4NJFs3uQ5FcAdkeJ/wK5ntJp9ZSSMaltYAzScC8JmhQkykgzzBCREZGyJ fGKg== 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=VxFHWZpjBaMg9Q8WcoD/wD5cJWkm+8GmIBRXN/pGLY4=; b=BvqMWoWBxVaD+ZWdADsKxC5mrnu9KSA3PxUuVCn5QClOhH2olyNwvVK0Me+sKJW4sJ nIV8r3x9Lx4lg9ORk/hEduGh+xZh8r2i0DElTj5XaL5Xn1QGQ2sKY1COpT0RYihz2+ZW bXCCdaRAU+colDl88ePmdf/5IwnYeCqZOk/WTEJBy5Sdpvqx+VGmTcGjG7ct0UA7tTgS qd508r66k6OIjzv2OYfWEQBRSS2eIxr5NHA3qkJnfvzKMgs+vcJZOvNMqb4BuVGqi/7K MQ7Y4EH74eq8ve7G/wXC0r2hhtTtQ/uiTnbiRLsRtaWcDmrz0D5RD3O+3P6N8mmAiMrd 5eTQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuaIF9QeS6tuQQE7g+KYvyn6OUBEEC+U5JFIP0h5zXxrE76MwkNg s+m1hEgr4cRVBiJcL3wYTDY= X-Google-Smtp-Source: AHgI3IYKb89IfJ82LaqAnjBHeIAULNi01ENg/fCvI1djaPCjcq75FBNe0HqyCxtMQ8TQHLYELSG3ng== X-Received: by 2002:aca:4b89:: with SMTP id y131mr400596oia.3.1550664322036; Wed, 20 Feb 2019 04:05:22 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:bbd6:: with SMTP id l205ls538443oif.3.gmail; Wed, 20 Feb 2019 04:05:21 -0800 (PST) X-Received: by 2002:aca:4b89:: with SMTP id y131mr400594oia.3.1550664321562; Wed, 20 Feb 2019 04:05:21 -0800 (PST) Date: Wed, 20 Feb 2019 04:05:20 -0800 (PST) From: Niels van der Weide To: Homotopy Type Theory Message-Id: <9e6e273f-dcf4-4c05-b94a-5851650ec8e1@googlegroups.com> In-Reply-To: References: <591a0ad8-cafb-41a2-8353-c8e389c64a32@googlegroups.com> Subject: Re: [HoTT] 1-Types are groupoids MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1460_2030185850.1550664320844" X-Original-Sender: nnmvdw@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_1460_2030185850.1550664320844 Content-Type: text/plain; charset="UTF-8" Together with Dan Frumin I formally defined the biequivalence between 1-types and univalent groupoids. See https://github.com/nmvdw/groupoids -- 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. For more options, visit https://groups.google.com/d/optout. ------=_Part_1460_2030185850.1550664320844--