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-lj1-x237.google.com (mail-lj1-x237.google.com [IPv6:2a00:1450:4864:20::237]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 83c7e46c for ; Thu, 8 Nov 2018 16:11:08 +0000 (UTC) Received: by mail-lj1-x237.google.com with SMTP id f5-v6sf3426122ljj.17 for ; Thu, 08 Nov 2018 08:11:08 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541693467; cv=pass; d=google.com; s=arc-20160816; b=TResQEM9Jc4b491v2ivzRRLgaH9FygCSuSBw5/rSJE04tZUr0kpq/YUg11oeLDVlxI 1SNd5j2yAgvEyUg86cP2qhQTYx9XFoCACCDp9L+qTRXfssZBf9DPaJ/hMZ+DEXgcpAjL LGiC0wRRhnP56z53Mx9R7o1Zhdygw8r9NXuI2x8rReEmZp7HKnUVDN2wcN9b+7370Qnh a5WK4hIXGgkr1tikM2hWVM+WOIAJk/QFTynYfGoK235civzL7/o90GmsxPWxV1BQX5ON lB9wjbPJxXIQNHWHHdyhspPDFEYjEyk5KnevAJVo/0Mlv6UD6zt5Qw9tzjz/b4gxqhE/ v9jw== 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=RASh7XoJ8zblWZO79O4qa6Tshg8W+MDpnK1YvmOee0I=; b=rf6sCj3QykAsuZJZqQmwoxjYu2HNSGzj/LO0sS+OgOGKX7E+T8BFJBCHoUm4b4U7nS jmZ4U2CwbQnaeRDSqCdQPMqwfcL2li83YHf4n03Ln2zjgPicD9O6N59XhcFdUzI5U+su 224qb+UPIBsZ32egCtgoG7VQ7i669G13WQZx8GkFXcQ+Ppi+TRoWQmNxfTkRrDZ+7fbI xwpkxjGEZ5oLiJ7J5eph1zfpHzZ35azKi+YbNQkzZA/b13TSVY0zJi2MmmHkXR7XqKYw d7o4u7GvBtXBYEEJo2SsdZdofXthCrxgruLJV2iFnFqs7ne5qACj1ja0cHwO6oY33QWx 6ing== 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=RASh7XoJ8zblWZO79O4qa6Tshg8W+MDpnK1YvmOee0I=; b=i6BtmLg/g28MWiwqNNRK0RuzGDWPOx/jZYNxQ+yLy8OWF6OIhOXybGSB2JpxRrXvBl 9v3Zs3/QinaJ/LyZXfINvTZoP8Z/Y2b4BCKN+wLghhul04BVCoYII33s9yQMYe+nKJgq +0IIKuZkf9b7wx9dRgHHYcYbKp/k4gMqPwYwneRsYlG0MLmCHjTBDicF1QNCRLvRAf6o hlSVKUbacqCJASNrMeaLYaUepAy99iWKWVn/zZ2t32Vy9QMwQARRTK+jnK7VgzXlVWQK 4a7f91tffygsAYKjBgtiW1EsCuvDgIR/YCunrfptjAexXtCg9DGcYhw4lptfrPxXHuMg hXvg== 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=RASh7XoJ8zblWZO79O4qa6Tshg8W+MDpnK1YvmOee0I=; b=W75SdZtyw5tzkeynk2tOAg+steJUgokSqmBFD1SNxiN093J6Qm1iF2zSuJ+AigZTtT IsIFrEehBKdC/XqgiCl7j9LIIex7gtkAtVGQPRYMRY3qiI3K8BxXmlOazpz2cGBD9N8p zu7kh/OUIaYY5m9sN9zzawg+7fwxyMrSNNK8WtkkGvtelpaQGyepNVwLEvGum97OzfDN 0F6L+a4VhGqisp9R3NkrfHwnxLfzstBuwY1Pv1HTEUcKG1Nz6FAXFN5HH06czRvvy9Nf sVY8gRqrYvHBn2Vw91nW9es/pLp5m8nfv3NLl2lg9lfhBgwYElsi4llqykLlA1DHtJA3 LHiw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gKHcDfpM30ZaJLIb2Mk3NmSUvRFhUtAafBgIYJArU/ZO4ZqLnZP xjF4WXvxi0GiopTqfq5YF7w= X-Google-Smtp-Source: AJdET5d83sEfWvV0WaeVOu5p2PWrW//DSN+2YlFCIKFoZeuJq1yD6NB+Kqz7wmvuQgN3IHjDrvQU+Q== X-Received: by 2002:ac2:428b:: with SMTP id m11mr31357lfh.3.1541693467926; Thu, 08 Nov 2018 08:11:07 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a19:d206:: with SMTP id j6ls190628lfg.0.gmail; Thu, 08 Nov 2018 08:11:07 -0800 (PST) X-Received: by 2002:a19:5f43:: with SMTP id a3-v6mr532946lfj.17.1541693467370; Thu, 08 Nov 2018 08:11:07 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541693467; cv=none; d=google.com; s=arc-20160816; b=k+uoJ+IctBByLfE6fU5zzFa03LT70DeDA/+c214LwI3MupYFuLj/0Hiqy6UCSqH3s3 TQ0SzGi2nYeWDpFnwl5KqibUk+4x9KoWJkudj/uBR+xBUdHFjVKNZ9M+BcLtNeSw0J9k hUjsHQauIIlz/fTnz0du88wm37Z5/v31P2jFKGgenXkNDJqbptrvlzql6b+o+c1VKuPF iXtxVcMU5wq76SZ3IDYKnjloAV4xNNTN/UDsohYvrdB7xlefPZaVlrRfQr7QOWnpgMJf hhvveV3xyV16k340tTHSjxvr8HjDmK0O63KsN+FibWdZ+Y+XHj2AAAMoW/ZwJOmHjkl3 mmFw== 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=aCClT90gKX2hK+mVVnheWgIlq/mh1kD/rqpj4EIP0gU=; b=M48QcDpb1hxp3KtfTTixlI7ASuh+pLctxim2gHQho4bVv416Vw+OXFtlylN7Cbup25 Ies8Pyi4DI/tmD7YJpTgu8Qi3Od872sfU1u/yJy+S4LmsK5ujaomirW02JjAPvlAYh0F 8TCa07im6rX2ZOvGAKRNlnMzmav1v6HcHwPRc06Zq7hkRSbpuHqchZUIBrctpGFJ6MPG 4pc///0MTNV9lchAKKW4wNC3sJ2nsLXk5qxOuM9atlWQ7jiUoiWcmV1rPSCHp88eJfCc 7iMCRgPf29HohjsgfVvxU8qPZ9tz+Bk7iQ6SyvonBx/JmzbDsjHvdFmRSRYCaPdTtL/u TxLA== 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 73-v6si113819ljc.5.2018.11.08.08.11.07 for (version=TLS1 cipher=AES128-SHA bits=128/128); Thu, 08 Nov 2018 08:11:07 -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 wA8GAebL010155; Thu, 8 Nov 2018 17:10: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 wA8GAep2016116; Thu, 8 Nov 2018 17:10:40 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 51C051A35F9; Thu, 8 Nov 2018 17:10:40 +0100 (CET) Date: Thu, 8 Nov 2018 17:10:40 +0100 From: Thomas Streicher To: Emily Riehl Cc: Homotopy Type Theory Subject: Re: [HoTT] Precategories, Categories and Univalent categories Message-ID: <20181108161040.GA12857@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> <18A8A179-4ECC-4C70-816B-0F700F47CF0E@math.jhu.edu> MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Disposition: inline In-Reply-To: <18A8A179-4ECC-4C70-816B-0F700F47CF0E@math.jhu.edu> 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.160316 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: , > A functor p : E ???> B between (???,1)-categories is a cartesian fibration if the corresponding functor p^2 : E^2 ???> B/p admits a right adjoint right inverse (right adjoint whose counit is invertible). That's not the definition on the nLab nor is it the one in Lurie and also not in Joyal's writings. 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.