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-io1-xd3e.google.com (mail-io1-xd3e.google.com [IPv6:2607:f8b0:4864:20::d3e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 07a60b4e for ; Thu, 8 Nov 2018 21:30:52 +0000 (UTC) Received: by mail-io1-xd3e.google.com with SMTP id o8-v6sf24697457iom.6 for ; Thu, 08 Nov 2018 13:30:52 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541712651; cv=pass; d=google.com; s=arc-20160816; b=iETeB2VRo3lSyr+Hk68O70UmbZ1WB7M6ssYHivaeBW0hcgBnVAWp+XK+hbq1uHtiSW OTvjCQ52ZvKJTcmacltdrplqT8uxbW9A9K4KHe1ECjejuCZkIJMEe7po28o29Vu8+8HK IfB4qoAgbf+q8djRpO1oEE/gUhOVaoxYBe0Gaa1lbtkpHQci1rFSG4Q5yk5LAQcoPCCC jYb6Mw+GCSkXSKD3hYFmFCM4DWOiVLalkPFGE4jiMcqq+BRIpJZGsF2PoWlpZpk7OXYT I+ZGGTfhUoHgL1Em2akySqRPnd+P+4nwroD7W8iDXHL6hHUrfgE9TuXMUAHWNW64myai V2tA== 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=vSJS4YG7H/W3RI5WmOVp0RQmnUXwjqEoZORVX2ebFiM=; b=hXyyb97LZDKzez2fX+exBL4GNtlybgYvVv1zfmSSH2viTuXx+Um4Mr4URZWef99ktr JYrk93nnGd09wft1gUub2vJfylkDCeaVr9jFITHAcRpHBeHckTzUGnxSQfHrCRLER1Cl VdM1vfF+5BAeePJRJg9iBIa+0oyfQAbDZHhpO1qnL/kSbjSG2tPbd3iksZOstWCzA5nV o9XfMSEGeUg/tEQGKiVt5HwvPhvcaJt5yYLjcgr6r/OKv5rAmuVmmKZhwZoPRq2TMuwQ XggvHkS/gKCAu9OKgL1BIjtloPxMQmHeeU/m+4zWAXb9LfL4Y2i88aDbOk3sJxXHGxFN Iqyg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=TjX9TAvb; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2b 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=vSJS4YG7H/W3RI5WmOVp0RQmnUXwjqEoZORVX2ebFiM=; b=LDLcCez96Em6So3ZLmO5iccJkecB8z6uFQn65pvcpcKXSS5IrnVAbRVedSrUPAx9OQ 0LnEnei9L+om6Ec5rUyPZ97ikNUnxaHVj8nWPFSfG2M8AvUtxWG3RfW3dImBvdeyHdlB chVca5Xgu6fdvfO5XE0cEDp4WgVlF4QRu0IPiGLz5oyPRT+UKVjNUvzE9rI5TYsm3cUp IyordMidjmFKLZQ9zCFKdmCn0yGZ8azKoAw8eRKPw1rasa8uSnvuH26t72dygNZRJomv W11ebVmjkXXxJQ/Orq3vrT9JPVaQ2Qoe6L9+YGdtwss+9snRFQc2sXR03v956vWOLeH+ LDLw== 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=vSJS4YG7H/W3RI5WmOVp0RQmnUXwjqEoZORVX2ebFiM=; b=ksdn1mtErK4xORgOhcojQRo9FFxAD7m5eTp29R9WTHSlM46RFW4A5HgoXrnmVs1kAQ N+81/zPT0qFRYV8bYHgZ4d2G3E2dwaHaEGS4+54wV2ROsQAnnWG/gXizNYeU+/MphuYE JPCFzIiWl7zHalD5MJTth00KbzPWV84qbgPlgvAhqqfUeNmSiip4nf/y7bgpj3O9zeMp PF0WUlM0iaHrVgzo4jbAKHSaK7N1mS8fHxPOWEchpNaV+4pPFhX8qgCmVair2YK12Ron OzH8et5PJDuSGEehz8D8TnwZcDMzaACbzbZY5ftLvX0rGpXE4fd79HADxNeu1dOQwW4t GhYQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gItZfnBf745S82B4hvRSAeyUKSe8zKb9B5Xv1FueCtYY9/pprBy /9aKwklrkRSdjKLM3zLwCr4= X-Google-Smtp-Source: AJdET5eAtxt3SAYNxxHQ9SdZep2lBtoEj3Amt+uOGWXEHzkaeN+lrO3CcuJ8xhxE7mlcXRAjCbYSgA== X-Received: by 2002:a02:8890:: with SMTP id n16-v6mr46500jaj.0.1541712651629; Thu, 08 Nov 2018 13:30:51 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a24:624e:: with SMTP id d75-v6ls7687itc.6.gmail; Thu, 08 Nov 2018 13:30:51 -0800 (PST) X-Received: by 2002:a05:660c:b0c:: with SMTP id f12mr76749itk.22.1541712651271; Thu, 08 Nov 2018 13:30:51 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541712651; cv=none; d=google.com; s=arc-20160816; b=m99EuFAuIQjb+fGJg4kYzxKa3aKQWxb9EAEjcSc+GguJOM9G11bm803urOaY1GUv/+ jZRwvcRMv8yRnHBJCJPrP3zKnudSwhb21SYSbwTTF2wbhGzCyCKFdUlTwgcS8uQGh1Un /B78oaSIkeXoA0LhefRhZJaUoMpIV0O30wcIdQudE60bf8y210iqZunZ+EziinKYPTDi DB6TyxDikiA4ozeEUSqhrVvCG1bPuEofu46yAU2qgt+w6fRsOTirzWXfHfLGlRG9d5uE 0K7HGOjBxsixUOrTfzYAxdR7bqgr1o28sszf+QpfzgUOs0OUZMJrtAU0gstPhrUbh+Gq OzMg== 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=x3boQMtuc/WxULFqWcP6poxAzhAyv4/Aa5AcO42nCA4=; b=RjN7vCot6ohT9GmVcKgV5/iqV2GKfM7Mz8I/Bo65hhH2lZ/Qu1OmzTf7BZv8nsUhS/ qFlSVVTrmkxo1v0ncHYWb0OZ2Hd0hAwqGKp00eqJJzVAxmNEbOSot4Ak+t0QiyUVVq/w iGMH1Z8X1ao+c3Lkhkcyq7127BpetOl3rMDkaGeFRygMVjENAkGBvhBqcACGzf2tsecV 5nTPrsX4CxvMRQJifZ8CZON8T+DLGGwHF8yufknGMYZ5WknLlc33XbOK8EkKbv9IyOXE T3aGuLd0ZAPGVfkPcHojSsvVXsIryUXFgwfXGASfs4nw4qyIunSTNMx2ZQh6qJbFwN2x 2cpA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=TjX9TAvb; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2b as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb2b.google.com (mail-yb1-xb2b.google.com. [2607:f8b0:4864:20::b2b]) by gmr-mx.google.com with ESMTPS id b81-v6si254560itb.1.2018.11.08.13.30.50 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 08 Nov 2018 13:30:50 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2b as permitted sender) client-ip=2607:f8b0:4864:20::b2b; Received: by mail-yb1-xb2b.google.com with SMTP id p144-v6so8943316yba.11 for ; Thu, 08 Nov 2018 13:30:50 -0800 (PST) X-Received: by 2002:a25:268c:: with SMTP id m134-v6mr6323158ybm.277.1541712650351; Thu, 08 Nov 2018 13:30:50 -0800 (PST) Received: from mail-yw1-f47.google.com (mail-yw1-f47.google.com. [209.85.161.47]) by smtp.gmail.com with ESMTPSA id a187-v6sm1476018ywc.101.2018.11.08.13.30.48 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 08 Nov 2018 13:30:49 -0800 (PST) Received: by mail-yw1-f47.google.com with SMTP id h21-v6so8606645ywa.3 for ; Thu, 08 Nov 2018 13:30:48 -0800 (PST) X-Received: by 2002:a81:5b83:: with SMTP id p125-v6mr6236835ywb.154.1541712648680; Thu, 08 Nov 2018 13:30:48 -0800 (PST) MIME-Version: 1.0 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> <20181108210848.GA11931@mathematik.tu-darmstadt.de> In-Reply-To: <20181108210848.GA11931@mathematik.tu-darmstadt.de> From: Michael Shulman Date: Thu, 8 Nov 2018 13:30:36 -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=TjX9TAvb; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2b 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: , It may be "indexed" in the sense that it involves maps into a universe, but it is not an "indexed category" as the term is usually used, since the latter is a pseudofunctor into Cat rather than a lax functor into Span. In particular, a displayed category can be a fibration, an opfibration, both, or neither, while an indexed category always corresponds to at least a fibration. A displayed category is a refinement of a functor in the same way that a dependent type is a refinement of a function: you can always recover the total category by taking Sigma-types, and thereby formulate all of the theorems mentioned in your MR review. The advantage of "presenting" a functor as a displayed category is that it solves precisely the problem at issue, giving a way of talking about two objects being "in the same (strict) fiber" without invoking equality of objects in the base category. Requiring the type of objects of a category to be an h-set does also recover the ability to talk about strict fibers, but the resulting theory of "Grothendieck fibrations" would be pretty useless for HoTT, since almost no naturally-occurring categories have this property or can even be replaced by equivalent categories that have this property. If we want a theory of categories that includes important things like the category of sets, and toposes and geometric morphisms constructed from it, we cannot require all categories to have h-sets of objects (i.e. to be "strict categories"). Thus, to talk about fibrations, we have to either use something like displayed categories, or a weaker notion of fibration such as mentioned by Emily (in which case one simply talks about "essential fibers" rather than strict fibers, and these do have reindexing functors and all the other behavior one would expect). On Thu, Nov 8, 2018 at 1:08 PM Thomas Streicher wrote: > > > 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. -- 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.