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-x53b.google.com (mail-ed1-x53b.google.com [IPv6:2a00:1450:4864:20::53b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id db45db9f for ; Fri, 9 Nov 2018 11:56:58 +0000 (UTC) Received: by mail-ed1-x53b.google.com with SMTP id r21-v6sf1060167edp.5 for ; Fri, 09 Nov 2018 03:56:57 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541764617; cv=pass; d=google.com; s=arc-20160816; b=kAMQf2WpB+oYivjPlO/6wiJ6/WbUfz+nsvqffUaM7yS3ZzDljUVo09KSAzGAgO/lEO g36z2mjCnTlk9bNrRm92/kKcbZ8zP5d+3FWzbvE7fV4W5AdcZyx8ZSROf94bKfQjmrps 8Y5WtVObWNUOnf4gqvh6ang+oq1ubGww6lZS1oGxu92yn4FfGdTettqCa1jtVqWvt+jg Eu30v86eFFc68vwsjDvmQX/W8rYJ4Uh9+DyDy2d32o+liK+RAUQDTnwis9ptjpAcpJCT JYVIa5XccZOZ9T2/VpPI0ce1S3LHaAvDgZh41lCgFgGez3rk1O6mr5/2jEKT1Zd23xpm J65A== 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=2KUpSHYxK+WAIi5hFfbhVTViLscOTdMmACzzYRYk194=; b=XodenpHnmqaLeigx7srlefhwsXWPgsu/RA++f8lk38ESlGtc3VR7v2RKRUiBAhBUWK Q4DlLKVJEJzN88idfskc11DHi/YKiGnDFVC2ykbikmCnmPan7MU+kr5SDbTSly4ToYNi 24TrzNCTyookFZIejWH9oui8oN08NP56djE2KMHZFzo7rn6/j/BCiejRzbHKujrZN62Y IztRJppxGbeNaT7m9ML+geColqmwZo/Fei8RpTTkkjDXPPXl8rM+w8u1qY1NGwVAF6xo 1EGqEMXQrN9SLmpflbj7Q3vQVFSVveKZtf/ouxhLU8Amb+Q6r4aTjP87gdbMPpXyfHns oUgw== 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=2KUpSHYxK+WAIi5hFfbhVTViLscOTdMmACzzYRYk194=; b=aH4r9u4glxtsnPqfq3b0xHG3fsZ3rHTJXJOh+y8pSbnkRPDu96vHPBpmgcLEdnfDBi W2S1PP/Bpim75H9tHapG2NSMMB1ZZlRCvZz2A1c/BWQh7cksuIvR9GhhShl1e92wKom9 pQecPOhKCDW8sK2kRgT2Nj3vzVjABxLrfhdfGZE404zmvIuVmsqKde8hm04Ch6w2GVv3 oKJQJqLYwlcmCW63b0TSHygSEkFw+u84v8js52+i3H22wHJqPEz8DB3S1HC8NRsiWI8y wJLKpJKSaG/26+Sdqi7Ieog40QA9Y74KGhrJ1HmXXJ2SaZziC/euGy1oX++IhXcGcqn3 qHTA== 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=2KUpSHYxK+WAIi5hFfbhVTViLscOTdMmACzzYRYk194=; b=AwRPGKBlbn6aa9KRR7JguSFPPaEki2Tl9UkurVity8CS0RciTWp6FpyAELPDoFdDi2 82SCmorvQvU3UfRjL/QGSGBW/gB03wLPPEj2J+wely9+C+wDGodkyidc37xnz88444U1 G9wR5vDhrm2BgfJfK+2BB10+sOR5svAGPubmneK82uDlPZz0BmsKM5Apqt6h+OEzRPz4 SiWuxvhNPCOcM4t5bjns6LXm9NaWgn8IiiZc5/Jpe0gNcTCF7NBBXi0YeU2tmgedf5Jm DmW9BGoQVnHIMfyaRjBXnMJR8QWlectcbk3y6nQqsVxpboSBswMxTW1oERFiJKL6VTay 5xnw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gLnP6uZqD6Na9lqyYGnLH6PK50LPmjlmng+qeWvnRfRI/rT1/by vHMUcT/NmTlTBa4awXX3inY= X-Google-Smtp-Source: AJdET5d3GJPiTOhdynOC1blE9cqJXjF5zLJlYo2l0YVbn7H7v1qDmN3BTBZsgaJi+GU7lgSKJm909w== X-Received: by 2002:a17:906:1e54:: with SMTP id i20-v6mr9228ejj.0.1541764617542; Fri, 09 Nov 2018 03:56:57 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:b362:: with SMTP id r31-v6ls378510edd.0.gmail; Fri, 09 Nov 2018 03:56:57 -0800 (PST) X-Received: by 2002:a50:a702:: with SMTP id h2-v6mr463623edc.6.1541764617095; Fri, 09 Nov 2018 03:56:57 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541764617; cv=none; d=google.com; s=arc-20160816; b=YnfGcjSwfc1XPlhRPcVX0tofMgHRLijKoDj4yo1XYK/hHCRb2mwIMHh8dn+LNZUz3/ lP7nuBNCliVq0tV0LHH51kTLHY8Un1BHLvbHQOq6jfahauDpbqFPQGxLe4lpYCtxqRdR BdV/InWvWmVUFO/eLdBtLphejQ4/JbE6jqIldzxtZp7boPNo2D4Ko0BbFux+QXxXc8vX kSAwYxyEE0mWHRJTTCWZEL5PrBnLJayzS+Wev4f4nSGvOXvX+ra4KQMEiL/d0b3sf9zK /UWttt8FOc8sFgvH2wcyeGGhi3Rtmgzj/IZ2o55F8MxezkBeA5Ro0WBChNJ6OnyNA08A 8TLw== 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=3E1UVDtqzeaO5t2AvTwyUiC2ghk7fYR0IUdm+czdmXE=; b=MUBXDegxauqW137z5ermDgHFtVMyPDjK+4vCkcm4KABeUKHKn8JBgs0S67P+buhZau 5zp7ThFi9cStEHaxS+tTujX91TcmqfnUQoY/M58MqFwBf6LSvg4Crq6yXBXqSZ4RFYyq nI7iq0waZhfDCznTJkMiBR2ln+QOkhbPOSP28eXVW+bwJ1YqWVjfa+2IuxzVIeDGSaG6 dfvR9Os0BTo8EHgyF1YMhL3d5LPbU1hvC6XC4x9GWPld51vbFrE4IEVZuwX/MNaUju4E QWZTrTYuEMhXtIgf8fX7R5C2V9THqn4SUeio5NcpU9AI24LhMvuFEUlTEhPJ2DQdUzun PdeA== 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 c7-v6si151744edi.2.2018.11.09.03.56.57 for (version=TLS1 cipher=AES128-SHA bits=128/128); Fri, 09 Nov 2018 03:56:57 -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 wA9BurUd012184; Fri, 9 Nov 2018 12:56:53 +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 wA9Burp2027123; Fri, 9 Nov 2018 12:56:53 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id D6553C7249; Fri, 9 Nov 2018 12:56:53 +0100 (CET) Date: Fri, 9 Nov 2018 12:56:53 +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: <20181109115653.GA7030@mathematik.tu-darmstadt.de> References: <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> <20181108210848.GA11931@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.9.115117 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: , Benedikt and Peter essentially employ an old result of Benabou saying that functors to BB correspond normalized lax functor from BB^op to Dist, the bicategory of distributors. But, obviously, the forward direction requires equality of objects. Accordingly, they can't express composition of functors in terms of the associated normalized lax functors. Even classically, going from fibrations to indexed categories involves choice. But going from functors to normalized lax functors just requires equality of objects. 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.