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-ua1-x940.google.com (mail-ua1-x940.google.com [IPv6:2607:f8b0:4864:20::940]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 6b11d092 for ; Fri, 9 Nov 2018 13:46:47 +0000 (UTC) Received: by mail-ua1-x940.google.com with SMTP id f5sf616471ual.14 for ; Fri, 09 Nov 2018 05:46:47 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541771206; cv=pass; d=google.com; s=arc-20160816; b=G8PE3mBT5U2CwpvA+5+Dpin2A/Avcbg4Sh2AdkgpMz4xC3phrCDpbMvQn/8dl+eRG0 ATxpKcRjFoZ0om1AnNWjcoVakNNSnUHlo2GiUUBGO10tUrSCcZ9BrbIvIKYgCti/noS8 RfsaHpdcgXba0YoYRtl/bWZF3z6J7rfsZTHL/nh3yTs4oxEzG6bBvPgmgVpDHSRPmtpC VxqCQIILcy7g9G/evdU8zOBYZmNv4y762wgqrKOeaW1ZSxLo3m6iT+768l/G4ZVFW4nM 4smJwDM+nH8H1cZnqPRaVWeMl/dyFRZmFf0C99jP92W2u8LuXG8WqdW9SkqBrGuQ29XT uWRA== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature; bh=fj3pddrVAawDEPrDE2L3Ou2dq89b5A/TnxpPbf3uWec=; b=Qv0W/+6ZB5Ujvhy6ZomnEv2Ihg402VIE6cSqDumCjl34CIudzm0PtZk3JPYbw7o0l5 e4heSy4kRvCwW8bl9PzHwpGvGGtlgU8qlrWClIxT1PVUb0PCa9RHu5Rc9Kn4ZIP0rJbl 2w+r2D/WmXeqCRxQso5+2hC4xNrQFEuXEUqg4wrG8gqRQkB0sAbLmu8GmzDPx6euhgRI t5CheBgKG3bXoSWHoHBJXz4hpfthsgACe5DtBxj795ckuetfFBWPeSxM8SEQMRVXo9kh 7rS7AZ5Chj0SJtKio0FI2E0WkF7GzTh85mf/TV5ah4tTHQiIqgvFC0E8E7ZQlEHccyls opzw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=RNzJX2NB; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2f as permitted sender) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=fj3pddrVAawDEPrDE2L3Ou2dq89b5A/TnxpPbf3uWec=; b=hdchu6beS5zC7Zf7e7TYRqkwtU/cNvXRG5tyxPmLOgJNrtbShdN8daPWv+54r1WxE1 kB1AKVvyaTHKBFzd0Abv9v+we3LusWdJk39kbNaGeEPiURFWOI3RjZ2zfSvWf3NP/62b cb8HcIbEwN6NbaIO0cPRXVcOKEHnhADBwkOnypJQFqLvQPj8Sk3faal/J+ZECuvwDicW tWyiEKTaQo5q6FV39fEr7nkMSpUI0g6pLEs7/Lo74amRzn5vM07i18lq+Gj9oWwdaSj1 nh7IG/lQ8d7xf8yVFlzy9tUlZzeM9DFRcmonpcqQacGx4ZZkS1bgFClD9NGQoSt2vlR9 n9Rw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc: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=fj3pddrVAawDEPrDE2L3Ou2dq89b5A/TnxpPbf3uWec=; b=Mly8RcHt9E+cDFBONp5HjQYL9R2VKPf9izPf6JvEwuO8A0MheGcj8DSm5nDABZlpcd iY9RE+p7gUCMrbUQNJYWsfXK9zEmZ2xAL6HyJeHq5xiOZX7axgnkzzT5a30GyXeUWSnA 6lmMZkclIFXN4y/zoiJf4kGkl+JISppJCHym1LEFdibI6tBQHVkwW/faqDF81yQsaQXD VjR0vlZqfwYD6x0PNAUqb0ldYIeV7LC7SpORoxL3/gM+NuaK6wUXlPLWUS6v6OQClcsG PXn++hPEJvI4BT93FsM/wmwFypH4Sx8i38OVOR68gdxglPBhIaSuyQtEZLFMkgisOjCW z4bQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gKEYCdNuctIzTYMscCqEXHVSBDkmlDqjYadBbhXAL3U65dKL3ev XU4su1i1ar4IXqHrfY2tUgY= X-Google-Smtp-Source: AJdET5fZ6GhcpdERcMK+XvgNPMlVOXGrVaij3AOT85hfw4cg34zRkcOQ2vbALX4viXnWa6mEPYsHXQ== X-Received: by 2002:ab0:4162:: with SMTP id j89mr49840uad.1.1541771206255; Fri, 09 Nov 2018 05:46:46 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ab0:645a:: with SMTP id j26ls260573uap.4.gmail; Fri, 09 Nov 2018 05:46:45 -0800 (PST) X-Received: by 2002:ab0:b99:: with SMTP id c25mr7463773uak.2.1541771205969; Fri, 09 Nov 2018 05:46:45 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541771205; cv=none; d=google.com; s=arc-20160816; b=WvnwRELmwCyxluS0PAo9CFLo0Z9OxX2KhXYtqMBGlAFAxOpohof85Dmb38ppMpeKNm c4XrR7+jz4tVWSkSo2JZikiYqOcEdn9T34fETBfTFIUqx6r2Fo5XZL8bM6PHy61/4uHX NYpACPQp7SAO1l8aVsZ60bwG651y3mb5hc8ed1bK2eKKxDCX4r2/oZwSdsb3+gwgdMj0 aQ9exAeUJOEpziGoYt+4wXmV6cXaM95xkjrVwDAWDd4Hze4KryxJIXcCom+khVL9VgTI NRjMwF1InVGwliHxHzBtZyWUN4ETjZtZglxf+rdqsZwycOFqfyuPzkLHALiFnq+TC07y WtzQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=svK+B71crFY8BPUKjF478WyD6cgorQ72/uX/y8ZH+IU=; b=rnZU60rdjX86lZvWMaeIaDz0ClryBlmbF4XuH6EBFTON+y9hc3KYwg0WU54xDoz6Pa JgdBGrcumofVnzfLou+eGtvuRehyKOPwMBjTCb0HUt1/ZxeVOrG3b7evTOvATFTcHRGa k32qm0KnYRK83Y0IXV8C8Xmv5b1HJB7MQXyUZKgyaik8CR/vrvcpXNOKkHhvvReL+MBa WAt2l23f6CtQLMjNhSzdhznWgnZ/vvbcSDFhrq8uV89lew2r/z4kyq/qh45iFQTaRpk0 SJfQH+JUd5n00onnfysAlsH6vfNsMBQjcD2Ni/LMT7yhMTz6jzcnQ8WieazTRHHsZPkV gerA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=RNzJX2NB; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2f as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb2f.google.com (mail-yb1-xb2f.google.com. [2607:f8b0:4864:20::b2f]) by gmr-mx.google.com with ESMTPS id 143si241386vkw.4.2018.11.09.05.46.45 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 09 Nov 2018 05:46:45 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2f as permitted sender) client-ip=2607:f8b0:4864:20::b2f; Received: by mail-yb1-xb2f.google.com with SMTP id d18-v6so1058823yba.4 for ; Fri, 09 Nov 2018 05:46:45 -0800 (PST) X-Received: by 2002:a25:1043:: with SMTP id 64-v6mr8635862ybq.159.1541771205264; Fri, 09 Nov 2018 05:46:45 -0800 (PST) Received: from mail-yb1-f170.google.com (mail-yb1-f170.google.com. [209.85.219.170]) by smtp.gmail.com with ESMTPSA id l185-v6sm1865663ywb.93.2018.11.09.05.46.42 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 09 Nov 2018 05:46:43 -0800 (PST) Received: by mail-yb1-f170.google.com with SMTP id p144-v6so1028593yba.11 for ; Fri, 09 Nov 2018 05:46:42 -0800 (PST) X-Received: by 2002:a25:37c5:: with SMTP id e188-v6mr8548260yba.243.1541771202556; Fri, 09 Nov 2018 05:46:42 -0800 (PST) MIME-Version: 1.0 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> <20181109115653.GA7030@mathematik.tu-darmstadt.de> In-Reply-To: <20181109115653.GA7030@mathematik.tu-darmstadt.de> From: Michael Shulman Date: Fri, 9 Nov 2018 05:46:29 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories To: Thomas Streicher Cc: Thorsten Altenkirch , Ulrik Buchholtz , homotopytypetheory@googlegroups.com Content-Type: text/plain; charset="UTF-8" X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=RNzJX2NB; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2f as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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: , Right, the *forward* direction requires either equality of objects or using "essential fibers" instead of fibers. That's what I meant by saying a displayed category is a "refinement" of a functor: you can make a functor from a displayed category, but the opposite direction is harder. That doesn't mean that you can't express composition of functors in terms of displayed categories: it just means you can't (or shouldn't) do it in the naive way by first making your displayed categories into functors, composing them, and then going back to a displayed category. Instead you just have to "lift" functor composition to displayed categories in the same way that we lift function composition to Sigma-types. Suppose D is a displayed category over C, with types of objects obD(x) : Type and types of morphisms D(f) : D(x) -> D(y) -> Type for x:ob(C) and f:hom_C(x,y). Then we can form a total category Sigma(C)D whose type of objects is Sigma(x:ob(C)) obD(x) and whose types of morphisms are similar Sigma-types. Now suppose we have a further displayed category E over Sigma(C)D. Then applying associativity of Sigma-types, we can construct a displayed category Sigma(D)E over C, with type of objects ob(Sigma(D)E)(x) = Sigma(y:obD(x))obE(x,y) and so on, whose total category is equivalent (indeed, definitionally isomorphic, if Sigma-types have definitional beta and eta) to Sigma(Sigma(C)D)E such that its projection functor corresponds to the composite of the two functors. On Fri, Nov 9, 2018 at 3:56 AM Thomas Streicher wrote: > > 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. -- 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.