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=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,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-x337.google.com (mail-ot1-x337.google.com [IPv6:2607:f8b0:4864:20::337]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b1c82487 for ; Wed, 20 Feb 2019 11:08:37 +0000 (UTC) Received: by mail-ot1-x337.google.com with SMTP id q26sf6824414otf.19 for ; Wed, 20 Feb 2019 03:08:37 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=hFAarR1zL4DSBwrQ8SldBp8FEIDzuHcxPJPd4MtTkGE=; b=PSqtklZZkCtjCuFkTD6aWexGsdHE6YZJ9zb3i2/RtDXrcSvdu/Tpdfy/Aa4w/b71pP vrqq3Uwl6x1uswyK+39X509ieUw9mM1Z6P4d/mAzNtn2u/qaLtfr7KL9r6dcVpmuqcx3 4Zs/FmBkLOr87HM7pL68sTxhwHIW7aF7MroeymaDFccC9uG7gNskW0F6qXIrHcN4RWma PRs7TWCVW9HfQDNw1nmzq1woJVVKImJrnXiMx0l8BHnl9OZ1r1cgZ9Go06I4RDYKkyEW zFOgiUPoYUiKgocF2fN8cU2bwrZlRZgpkvPCbvEXWWpO99zSrB9sgH8ZcLCRP/qF4LpV pKnQ== 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: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=hFAarR1zL4DSBwrQ8SldBp8FEIDzuHcxPJPd4MtTkGE=; b=Jil+Vyl3IuiiBVlmX/oM1Fu8FznyNsU2cUJI58kz8oxVjuaFQNlUWjRWFFEUD49CbX 6zPsLU5BUZ2hEZvnair+t1HB82iaaVy5hOK1q2VnZPTpbHxHDLxz2r1u1yBy9+qOYDJd vPw/8ThdlwDB48RTzGLbz8DlT3+Z907G8SZJcCMPIBrkBg94lOq2yMxb+V5YE94DDa4g K1FIGGA5nEDS68DxvqgwPo/7IbWg9GYsBKXmYlePzxTdEuVivAysavhIfMhMX9fikDph hG1uIBBESGTv/sE22xGQMErG2MhLbG3fXS6MZYN6jyHvCpTnEUMqeruS9dVNCcp7qdft I6Pw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuZuG3ekz/n5JfIQDJtshs6wyyk8ihlGF78GmYqCVumAnl8cIsPv 6qubWgSfT7Gn+ejRfPQSlWI= X-Google-Smtp-Source: AHgI3IbrbH7sohGqu159TUcXAIQTB66eFhyzQw9LhzZXqO70bflBntFGLpmCWE5zgmXhrQiwcduGOA== X-Received: by 2002:aca:afc3:: with SMTP id y186mr394673oie.0.1550660915863; Wed, 20 Feb 2019 03:08:35 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:3d54:: with SMTP id k81ls406053oia.1.gmail; Wed, 20 Feb 2019 03:08:35 -0800 (PST) X-Received: by 2002:aca:cf4f:: with SMTP id f76mr390098oig.7.1550660915290; Wed, 20 Feb 2019 03:08:35 -0800 (PST) Date: Wed, 20 Feb 2019 03:08:34 -0800 (PST) From: kristian.alfsvag@uib.no To: Homotopy Type Theory Message-Id: <591a0ad8-cafb-41a2-8353-c8e389c64a32@googlegroups.com> Subject: [HoTT] 1-Types are groupoids MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1552_1145142.1550660914555" X-Original-Sender: kristian.alfsvag@uib.no 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_1552_1145142.1550660914555 Content-Type: multipart/alternative; boundary="----=_Part_1553_1559558912.1550660914555" ------=_Part_1553_1559558912.1550660914555 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi I was wondering whether there exists a proof in literature that the type of= =20 1-truncated types is equivalent to the type of groupoids (defined as=20 categories with only isomorphisms, for example). I.e. a truncated version of the "types as infinity categories" viewpoint. Thanks in advance, Kristian Alfsv=C3=A5g --=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. For more options, visit https://groups.google.com/d/optout. ------=_Part_1553_1559558912.1550660914555 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi

I was wondering whether t= here exists a proof in literature that the type of 1-truncated types is equ= ivalent to the type of groupoids (defined as categories with only isomorphi= sms, for example).

I.e. a truncated version of the= "types as infinity categories" viewpoint.

Thanks in advance,
Kristian Alfsv=C3=A5g

--
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.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_1553_1559558912.1550660914555-- ------=_Part_1552_1145142.1550660914555--