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-wr1-x439.google.com (mail-wr1-x439.google.com [IPv6:2a00:1450:4864:20::439]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 4a38e7bd for ; Thu, 8 Nov 2018 14:01:05 +0000 (UTC) Received: by mail-wr1-x439.google.com with SMTP id h5-v6sf9722809wrt.7 for ; Thu, 08 Nov 2018 06:01:05 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541685665; cv=pass; d=google.com; s=arc-20160816; b=YxnePZ15sYW2zqE38uFLr5hGsF+qM3HN5KCKJCHt9vFDLqWCZ5YbHyTZpJW/UnC8rC ICZNLbH1OnDDvxQk1jLzBIErY/AwFYmQfXZ0f4ExoU/gMycLyQK4Qm68q7qP/dfjw8BX 99cJeVqTQtu/O68FWG2TcoWbxSAFoDu7Pn/7K7bYslOpGGXHdBiZehn3GgR1UioyHgml kPncmkkXjz5TkjnuOibp2FIeKZAdzUQ7VD2+PqRX41OsPgD4GI/zCz7m79THbVnd+D0G qYQN7ydQH29DbuUxk1Hc3V3Dwx5cGbtXI+XazFpRBK5VS+iN3i492tCZgJ4itg1ZauWe GoJg== 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=zZMU8xF5KUw+fXd6UyQIe/3buNpWgDBoOWffT35tZc0=; b=RAzwEDNa+u6Zx+NEGqAC9Q4gD73URUZB8WkGGjTi+rIinnsbh85C34ZvX1EFFclPH/ 8O/aupYLCgQTkOHyydu2+yqhGM7VzCrEjPzn3JLaImaDukR0UyncYvkK7uqU2zaRpOKF CAKrkMlUlcYsfKCGI1ZXvOsOlyHippSOMkEdkL1VCZSdlIA1NvK/+sHjxRj1K6v89r6M xXbapHW3aiSyFQ+T+R+f/FLvgtraSy/8tLj9gipCFH+SwFt3zagN7+c1Hj5IDRuM/TW+ Jl5j6b4Zi3i5/vLL8QnxMXLLUaidg972a7tik1ywRv/wklKUk41MDaOI2xCL95itPr3W JBWQ== 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=zZMU8xF5KUw+fXd6UyQIe/3buNpWgDBoOWffT35tZc0=; b=th7JEMNbec0QwdIbXofPD6nA1lkBx5HwAdT/6uHHxzNjGAi0koBiUJuzsyy5j3Ny34 y87jk/mEmulcukpD/ycuvKgP7ZztrO3JlqRuOr7JXBGTx9AClv0sMvHm+/TGyDWWqSV7 7D4dmW0J36wDxsJdum3zhBRF84P6fgPU8eSSguIkkQm+cp0uoQTsGBk/a42PtJi5+YFS F7sWkuxNEVQVaPRItefcewv4WTrsxkOYHzjudnvHopU/4dimb5nV9NBnwjzGMUT1Ar8j 1GaKTwfzD0jpZ/ta8vcUyyhRxFTcHYVYc7wMiV/Qx6Rj6qxlTkGrI7/ywi9GWraboBVC sXgw== 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=zZMU8xF5KUw+fXd6UyQIe/3buNpWgDBoOWffT35tZc0=; b=cknuJY3eGv4hYnn9tUSbw+NfSSrL3O2a4sPwQmE1D9b84PrnysDG3uewXkCLA0Wwp7 DDrxPTklhLDrXtevAcf8kK/aA5ZvZbqSS1Xrq+EHEUV5ZbP0tCi/NdevEnlJzuH2j8fd S3eLoS7qzu3e8SPQB2laU9VaT/AKfIod3sGd8vXJTUvbvRTDL9sefJOnviCeFtIoJior xuXQx8dzoWnVYNFA/KOnp2Jdaqqe6rk85P27nOa16blxySjLIyR4EY+uwhrhezUDmbFu hSF/YF1twiew9LWwqimdWdSnurJlKeAdjfX9cYH7u9p696DHFtv/cz+buXNfuu7D6eqE K7sg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gKU8uM3KhPUjJlc7Shc02s5EBQq+yyOxUKTXyLCQc21HyHWejYb 0zoW2DQ+44b9kRQozWQNmas= X-Google-Smtp-Source: AJdET5fxpe7kq29AjTQ6geaxPBVdCvTvN8PtwQkFlH7/TQYsH3H6OCP9exe9DHidkYQXDIzkBOuzmg== X-Received: by 2002:a5d:4acb:: with SMTP id y11-v6mr50390wrs.6.1541685665277; Thu, 08 Nov 2018 06:01:05 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:8489:: with SMTP id g131-v6ls245284wmd.5.gmail; Thu, 08 Nov 2018 06:01:04 -0800 (PST) X-Received: by 2002:a1c:cc11:: with SMTP id h17-v6mr137116wmb.2.1541685664672; Thu, 08 Nov 2018 06:01:04 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541685664; cv=none; d=google.com; s=arc-20160816; b=J6Ac7c8ClwFzDoz4BoMH4RezHjOmlaveLn20bvw7Y961c1nW0yF8nXvAjNKUIwEYAy +1Vnc+p6osNSLPE+KFnr/feogK9ijocz2rbGmvIF3lnYqAZOmm2kNaGDRAar5OEGQhuG srC5OOxllBmoY/NpMIYivbJ6XfeIBO/4CtwDKnUKEs3iN7aRhR98ETPKR6peclojJ5ZI p16uviGVF+0O5XQPCU3lGGM4GLoJflW6Y/FHWSu2hC/p2HnQSEN/3K/R1PURvuMyoFrd /M+WwJGr4qipm5PPtSzJY9IW1ZPilNHRcv6coqoFvlR6CtML9oZZeH7tfjuzY6sh26Bh CCFQ== 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=zpNYGqbcPfnrI3Lme0kfUfZZ3I8vYfua5jaoR4ksy/I=; b=tnZZoPOnS7jM2y1nmQpCRMGMoBveEdgKw/+ifOpYt2lJ6j6zImStdh/16UR9yTisKh vPtQ1Nv3neBuCpZ7uJYKAvAA/50zfbKtN6315IxhESyMo9imPpTxtNMbizCOP1gkPWHf ymNCdlFwFpan8LLQzj0H3Mx6MeAMtI5WKwuKM72K+X4QOesHVB145/btypy8y7USma0+ pJw/Pqd4V4mMLfVwbS+AABctZhZDt6o8l+bSVvxwiNti7gC6fFl1sAQfjV9cQ4H7+HeL fBrAhkYLVk8epE5eVwFEcwyiX0TiR/90uoHlgoSYwTpQJyCbSk5OoxIYcjRrGfnkZmVK UKEQ== 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 p19-v6si35950wmc.1.2018.11.08.06.01.04 for (version=TLS1 cipher=AES128-SHA bits=128/128); Thu, 08 Nov 2018 06:01:04 -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 wA8E11Ol024326; Thu, 8 Nov 2018 15:01:02 +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 wA8E11p2014413; Thu, 8 Nov 2018 15:01:01 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 258731A35F9; Thu, 8 Nov 2018 15:01:01 +0100 (CET) Date: Thu, 8 Nov 2018 15:01:01 +0100 From: Thomas Streicher To: Emily Riehl Cc: Homotopy Type Theory Subject: Re: [HoTT] Precategories, Categories and Univalent categories Message-ID: <20181108140101.GA9923@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> <3EDFBA7A-AF24-45D3-9CAD-7829239F458B@math.jhu.edu> MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Disposition: inline In-Reply-To: <3EDFBA7A-AF24-45D3-9CAD-7829239F458B@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.135416 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: , Dear Emily, thanks for the various references. I was aware of Street's generalization which is obtained from Grothendieck fibrations by closing up under categorical equivalences. But when one works with fibrations P : XX -> BB then it is intrinsic to have have reindexing functors u^* : P(I) -> P(J) for all u : J -> I in the base. And these one doesn't have in case of Street fibrations. For me Grothendieck fibrations are a most useful tool for 1) categorical logic 2) category theory over toposes or even more general base categories 3) conceptual understanding of geometric morphisms and properties of them and there the stronger notion of Grothendieck is indispensible. For Street fibrations fibers over isomorphic objects need not be equivalent anymore. That appears to me as counter intuitive. But, well, speaking about fibers is evil anyway. Thomas PS (1) Admittedly, in HoTT one needs fibrations less since one has universes available. If I had to defense the HoTT view I would say that fibrations are meaningless and they were used by the old category theorists only because they lacked universes. (2) In ordinary category theory, at least in topos theory, speaking about internal categories is very important. I guess that is an eval notion because it is built on equality of objects. Is there something like an "internal quasicat"? -- 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.