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-wm1-x33d.google.com (mail-wm1-x33d.google.com [IPv6:2a00:1450:4864:20::33d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 4f9f87d9 for ; Thu, 8 Nov 2018 11:58:21 +0000 (UTC) Received: by mail-wm1-x33d.google.com with SMTP id 143-v6sf648279wmv.0 for ; Thu, 08 Nov 2018 03:58:21 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541678301; cv=pass; d=google.com; s=arc-20160816; b=cIuCMz+vzY8pwjtl5W2791xnRb4Okh/Y1pSow5UFz+SVk2ynp2jrDEhD7mWzQx2yfg /Laiib2EFYG3XSoP9n2erYKvW86AE+1oXjmxhZ/qnN00QFWnSZxvQpo1BgbcROTtvwKg BSB5nNe43NxDEFQvDyF2iuNWbF7xbLWVpbbFdMPz3MnA6ASZp26HwpKwa5Dpa0vIHXFF DXggyMBHSca9Mpl/1WTvcgMtmCnojK7xswrWgC2leIZSrDDo+7zet08NcHT2NcYrZzml GeVWHkZZzQTPKkmPOwb99JQs6+oGUYnoeiOIAbrURB4hlu/cVbvosm+puVwFk2dZFyB2 h2jQ== 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:user-agent:in-reply-to:content-disposition :mime-version:references:message-id:subject:cc:to:from:date:sender :dkim-signature; bh=EJXWjPVXEVLBd+Rj4kecxbmOd5P5/V50MibdX6IAbUg=; b=Jb17tSDQAwOqQ6LwFwo60/NC9yrdhg83JKCAWtk00wgRDdJAV12jZT3PsU8/FbuhYw BqqtbP7rJyO2vJ75Lyo5mqf5crjiHwgOhw3SJeMfGhzfIWsXNHZoqIS4xA1/DT+HXMjD OTsP86xusc2M/3mX/jgrm92JCRXqKaxKMsuiwxViXIXq+V/iptgN1DgpUBoVCPtXvGpA MOfENNPQNqBr7mujybpgZLM85Dq9Vxghf5DmwBE8Bd2u/NwZgI7vDDa7ro1FOfipRVDZ VfJiWt5MNbthcBjyBK2Rc4Iul8HrK80UxgxpCpxU0kooulDbD5QrpnEr6cv2gyYFRA8R timQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.225 as permitted sender) smtp.mailfrom=streicher@mathematik.tu-darmstadt.de DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:cc:subject:message-id:references:mime-version :content-disposition:in-reply-to:user-agent:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=EJXWjPVXEVLBd+Rj4kecxbmOd5P5/V50MibdX6IAbUg=; b=Y9sE4VDZyaRcn9GeM/KIZq4iL971ThHcYOdXP6CGW2+pRamxwSO19glU6ZlJTR88Z/ +K11D0+4nRXVJ+BPsuL9Ai0xAFun7e8sTkfZFVbJWoB56klO+1g8wG0cPYA5ONTfeWAF P8SDJC2yXWt0RprVuBPxyJonnmldQMP3o6pKeVKfwqVE0FGft0Y4M0yvGjQjT0/y1aZI 7Dw+tsjbJVuzNTC9KQU9ftL7vzssQQ/HOp0eY8He4EXx4jwNoub8Lzc9Vwup/xmSR/oD srE3V9t37Gu5iyp5mjvHyTWWqDH9PVOq3XxhwN/IMtMgTSS5m+qNOftXSBjHroPWwYn1 U6Sw== 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:cc:subject:message-id :references:mime-version:content-disposition:in-reply-to:user-agent :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=EJXWjPVXEVLBd+Rj4kecxbmOd5P5/V50MibdX6IAbUg=; b=FlyZPVSvq1UDHWDYIOdIa7dbQQO1Q1qQZdnFMlbM1i3iEMPWxRJGfjWn3sPskBBeRK xSbvCWFjwVl/IbjG3peSHxSMgpcpEqqZnb5Qz9TcaHRofYZG5yr+pLrJbK204DsAtRw0 9rLbEDaPSuDIHm0TRpjKfDYF8UdTleTV4x9iZ2SCqD0CW4GTpEONCVxGJqNfmaJ3+ANs oPc2moFIlRA+60BVejd4tpVu2yAVnN5uo+WuJ/Zrz/RsGE3OPkUESRv5YKhT/mPI9eHg Y57rcg3mZkDBBBMoazch1lzAl8mSUWX/pHN6uqp6TelsG8by/6NyZuJ2U9+tW327iuea nYiQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gLrbUvbNsL7m2d9S4dQQRCbAN1E8wFe4kG8aS3+MKMozA3jWBLq s0yknq6LsjOWL8z6hjmz5yk= X-Google-Smtp-Source: AJdET5dqoM+o0awCB2c2r7eBGHJ2AiK2YQK5HLsNq5b7f1RgqWfqOPp94rU6I5lsmj0ag9LmjROMqQ== X-Received: by 2002:adf:8226:: with SMTP id 35-v6mr46598wrb.0.1541678301188; Thu, 08 Nov 2018 03:58:21 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:cc1a:: with SMTP id h26-v6ls175237wmb.18.gmail; Thu, 08 Nov 2018 03:58:20 -0800 (PST) X-Received: by 2002:a1c:384:: with SMTP id 126-v6mr205043wmd.9.1541678300673; Thu, 08 Nov 2018 03:58:20 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541678300; cv=none; d=google.com; s=arc-20160816; b=JheTlolTYscj/113CRb45U5XrAhicPNa0bWDj+aMGfWlkPpfv4JJvKP90FTb3GFozu QDr3VVSNDADGCsXh/T8melex1tKY6fn2IJfpY/MRVlAVlsTPTS25TtSxgkEdav0LG7gF zzXGbKSoFWXfnQ6Wz4Wzw65R2kn+qv5Dz8wSa/G2puc8acAQJpc5f/UsM3R/w0exnRFt eUQZT70oj1x681qRWZ+88KsjFA83FVkhQxwK5tCShmZsi9rIQ1tIYr5CMPgkY/t0strM pG5f17TBrMS6UP2XR5WbrgPoYXgl9JUJIOTRAAZBAs0L+Du0+Ahj0MS1MfnBtdYXv1L1 rUSQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=user-agent:in-reply-to:content-disposition:mime-version:references :message-id:subject:cc:to:from:date; bh=RIytPljmBadE+x1bVYKM9ejH4cHJ7qqp9cei7388G6A=; b=zc0mCKrFXodQtiD7s2yiCZ5XuXkjvn3H4qTEd8HDkGdrsCBz3rQgbLZkzu1PutYqxW gyy8rMjKYSjo4sAwgTle9YlNuNz7PlHPjjjLf9v//9VOgyAE5yibvXuagmhik3+sbuws +tAgVWxRfHupIGKR/wcQYEwtzmckP9nx6uFGHV4tOHlEvih96rSujop6CdGFp2iKBNOL IMVmei/cQ3CIJr7Mt2X5sG7NEZBMClA+WUx5EycVQMFYtOj9hCMjBWEqslQlMz6BeqvL O5yhlkzDcdT0XGYW4v1ZOid0rViUBD30REakfsIklZWHL/2qMQkp/w/qe7CJmwGzonIg Y66g== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.225 as permitted sender) smtp.mailfrom=streicher@mathematik.tu-darmstadt.de Received: from lnx500.hrz.tu-darmstadt.de (mailout.hrz.tu-darmstadt.de. [130.83.156.225]) by gmr-mx.google.com with ESMTPS id z129-v6si110614wmc.0.2018.11.08.03.58.20 for (version=TLS1 cipher=AES128-SHA bits=128/128); Thu, 08 Nov 2018 03:58:20 -0800 (PST) Received-SPF: pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.225 as permitted sender) client-ip=130.83.156.225; Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21]) by lnx500.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id wA8BwEHM024018; Thu, 8 Nov 2018 12:58:16 +0100 (envelope-from streicher@mathematik.tu-darmstadt.de) Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209]) by fb04281.mathematik.tu-darmstadt.de (8.12.3/8.12.3/Debian-7.2) with ESMTP id wA8BwFp2012544; Thu, 8 Nov 2018 12:58:15 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 415661A35F9; Thu, 8 Nov 2018 12:58:15 +0100 (CET) Date: Thu, 8 Nov 2018 12:58:15 +0100 From: Thomas Streicher To: Thorsten Altenkirch Cc: Ulrik Buchholtz , Homotopy Type Theory Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories Message-ID: <20181108115815.GA5022@mathematik.tu-darmstadt.de> References: <3c553ba0-2181-44ec-b790-969a8115ea1f@googlegroups.com> <1a3288ec-ca0e-48ce-80ad-9cad01f56845@googlegroups.com> <4ae4c745-a00e-4ebd-9de2-e29474b75d48@googlegroups.com> <20181107153556.GC26970@mathematik.tu-darmstadt.de> MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) X-PMX-TU: seen v1.2 by 5.6.1.2065439, Antispam-Engine: 2.7.2.376379, Antispam-Data: 2018.11.8.114816 X-PMX-RELAY: outgoing X-Original-Sender: streicher@mathematik.tu-darmstadt.de X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.225 as permitted sender) smtp.mailfrom=streicher@mathematik.tu-darmstadt.de 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: , Thorsten asked why I prefer to have strict equality on categories. The answer is that one needs it in category theory typically when speaking about Grothendieck fibrations. And the latter is most useful in many contexts in particular when understanding geometric morphisms. This by the way also extends to Grothendieck fibrations in quasicategories as in Joyal and Lurie's accounts. Thomas -- 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.