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-ed1-x538.google.com (mail-ed1-x538.google.com [IPv6:2a00:1450:4864:20::538]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 9a9e190e for ; Thu, 8 Nov 2018 21:08:52 +0000 (UTC) Received: by mail-ed1-x538.google.com with SMTP id h25-v6sf29762eds.21 for ; Thu, 08 Nov 2018 13:08:52 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541711331; cv=pass; d=google.com; s=arc-20160816; b=doeM5EDG4oKME4fjtNonx9i+lUHwyJ/TD8ddamYEOqSdPZzLy6jL1UNAdWXdhQcmeL jq/5MnctrTIiSjILbYPL9q7QETH8POLkbZLcW3sFNkMcNdZkbqTjrE4vhmJ/95IX2nHB o0MEsC+JWMnQFyI6nmHskl8WMZYp8rRiedKWE8I+kgZjPS+f2JPOBf4vPk0QnrzGNpzn 2+t6si6rST7gi1qDRJ4NOzMctW5GZt2riUhiS6NtmhHsX0sJAoe19yGqSkhEEYPpyneF +NCaeJo8mXqfd/9hB6r9DfTNhFwPT1aW4TrCCq/rCTdmNhXQKVq6CT24aTeUXSZpLPtZ QMRQ== 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=Iojht8YiIExXXhug7fNLId/SaLDrl8MG1iOl3FVFKa4=; b=sQ8zY4zi8kpdDlRkCbO3Bm0spGXnI9N6/207QJ2P776WlNvV9W0KGl0nubqHInFxLj gcmllpOo6/VvfJ0AyWh+qWiYyxsFjduQqj56zdy6txCvXYm5Zg4fo0JBHH8ZLi75HVno c8iQc33NNXr6EpH4j0N1pCoa0X3r+L52XtLMrkucu8hBtcRxS7mulhJ8ZWYzkTc4eubb E6bn4YHrH54QpRrdMYhym+1KbRzchfu+9Gzp8T1UQxPaEWWjWVv5iLao+lajXy6xq5cP 7lE81iY4DWgnd1JytnqRGrx8aA1zFiee3zYshNgBzZAWArq8uYqlPaT5P4LmcLAZxZTt 5zwg== 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.239 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=Iojht8YiIExXXhug7fNLId/SaLDrl8MG1iOl3FVFKa4=; b=bO1BDKxJAAQHY8nwEt2WOweWnxNqHT6tH+dX00fJz6MEfvGfodpmo3nAllA70199Q3 3AFptZOCmM93Nh39ZGjdTOhOPuSjktwBcMUliQIlhPYJtG8+da2+ed+R9e7VXLyqrUdH AmJMgZANn+c/lTRZa8P9beRZC4YeoU/Fy4/Z2NLwZq3huj3gS/14D16Ns1zSs0qBWIuO KNd7mPQFevwCU2phwG9O2Ag/GBk3fDkAcscr+4sN0Wk/nz1o5X5YnL74zXDut+Q1fIvL mhnTj5RSPtBtQ2/lZrBx/gtHxcYAM4+Mrg29pSihznx9CBAqXcrF0n/hsy4kljSvnu7P zH3g== 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=Iojht8YiIExXXhug7fNLId/SaLDrl8MG1iOl3FVFKa4=; b=b9f7B/rcA3rkeIlv1z6ELl4+hybF5hWMAzNV+le8XwzwZ+C2pnuIYCwK7uwitrLx2Z hvEUS49C39PRvb7I8ayEvR1VUEx35AdVllpPOKniLdEmJeJvAeQlPu/CQENcq+ea69CT fABGEd6v3eZsX9VWs+Fu+5+SNR77ls80FQE9650jpZRDXGN1auSEcKl0rdGdF3PZi0D5 dwRI4jKSYl74PGzW/SKBkEPjQmREwGjGCCX27OV4HEcIhg2K2rTwMBHTflksYrDKyINz YPPOjrULhMZuMps3EV9Gkjp1HxRy+xPAkp0LJcmF76knCAC7hM7/qY1OE46o7IJ+3LTx ZOtg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gJhEV/+qgYkf7PQPdwfVbWIlhPSk7ayrZEECucuHiWI+GPrq7dI CSXhzJkMTlUQbW8rmCpHqdI= X-Google-Smtp-Source: AJdET5eEXfeUiqQlwvF/lYas2IjXwUChogMu6wRt7GqAbCkr7dRZng4uZ/tdyJ3CBdZm08sPFMyiIg== X-Received: by 2002:a50:893b:: with SMTP id e56-v6mr219ede.3.1541711331177; Thu, 08 Nov 2018 13:08:51 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:f5f5:: with SMTP id x50-v6ls428edm.1.gmail; Thu, 08 Nov 2018 13:08:50 -0800 (PST) X-Received: by 2002:a50:be0b:: with SMTP id a11-v6mr3170edi.10.1541711330150; Thu, 08 Nov 2018 13:08:50 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541711330; cv=none; d=google.com; s=arc-20160816; b=B+1wfDwDX8jbgU/4Pm7AG5TYJQJ5/xARfQ/15DKxQL/FUwBxC7BxhAk5gHtA1DTwfQ HVQnzj30sob9bxpcyUYu1y84f7jCpPnW8V2JUvQ++GxFoBsJNbJlonTv9Wv1jPGqVIbS 4u38giiHkLaKS5s+/SFPPpvOiF2IHj//7aPrvxNOCwRanlyNohuwptqZSv9hTYHUcAgc 9grz4xQVi+h9oKv7OpbdyZy+/OcymWejqKesp8Z6h7iOsPjnQo0RqILyrgq2lJxnTLDf vib8uYcfMYxZLkeH6lY0XuCbfrXtlxercht3fULdlY9KJJ3ACQt+HRH84S9SJbz0TC7S lc/w== 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=PS3dGIAw1ETgJsXYzVp3luaz1dzS7QqdyZeGoUPliqM=; b=uZ7hNhW+fqLdDbGO37vxqsbeG2OEM6SJyyQe8aOx/y3oMfHXSFvB0kpru9ViOJb+iq 4dfhsbPlyhIeZnjSrkw5ZAKkDnRogqxGsUWBOtdf3/HYSuam9SiFRTKnu+rxODTU+VBa ZMsQERlNSYNm9zO6ffb3w3QLmv+9N8f4flkuoLpZwMVGmbfMLmz5Clq6dp+TFakIvjJn OHUflbZHkqovqrMUx8W2LiVdgAp9qUW2t9m17aPGJU3Jp9uTkoW8UFdfdXHcCplCb8Yv z/pNH3G+0fvwH41zQJO7nVJ2YcTkDIIr3uBQ0h4am6eM0A8S2Ym+oQQmm46tkWHQrku8 kjgg== 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.239 as permitted sender) smtp.mailfrom=streicher@mathematik.tu-darmstadt.de Received: from lnx503.hrz.tu-darmstadt.de (mail-relay239.hrz.tu-darmstadt.de. [130.83.156.239]) by gmr-mx.google.com with ESMTPS id b56-v6si143471eda.4.2018.11.08.13.08.50 for (version=TLS1 cipher=AES128-SHA bits=128/128); Thu, 08 Nov 2018 13:08:50 -0800 (PST) Received-SPF: pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) client-ip=130.83.156.239; Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21]) by lnx503.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id wA8L8lJ0009462; Thu, 8 Nov 2018 22:08:48 +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 wA8L8mp2018946; Thu, 8 Nov 2018 22:08:48 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 2FCD7C7249; Thu, 8 Nov 2018 22:08:48 +0100 (CET) Date: Thu, 8 Nov 2018 22:08:48 +0100 From: Thomas Streicher To: Michael Shulman Cc: Thorsten Altenkirch , Ulrik Buchholtz , homotopytypetheory@googlegroups.com Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories Message-ID: <20181108210848.GA11931@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> <20181108115815.GA5022@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.210316 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.239 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: , > Actually, you don't need strict equality on categories to talk about > strict Grothendieck fibrations in type theory: > https://ncatlab.org/nlab/show/displayed+category This is indexed and not fibered (see my MR review of this paper). 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.