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-x538.google.com (mail-ed1-x538.google.com [IPv6:2a00:1450:4864:20::538]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 50736873 for ; Fri, 9 Nov 2018 15:07:00 +0000 (UTC) Received: by mail-ed1-x538.google.com with SMTP id h25-v6sf1300246eds.21 for ; Fri, 09 Nov 2018 07:07:00 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541776020; cv=pass; d=google.com; s=arc-20160816; b=SglAnJUINnztye4g9Tl8tQa90Ie+ra2YXGbnjdUhA4X/zfd4TvoNHlNEMe5wd6uoDc l9ibt2tdcgg3x4OiKEUIDc5VUjsUfTNAx7G2q0JJyN8ujORBJ30SMCsIq42mn9Y8EoPA Q3UqN1tI+Gaz0t7exld4g2KTshDasbGianLmkK/2KdpaJIHBEZti++FN+GMF2S+5IL3Q hs871zBP12mADK+BTCnYRoXGX/YkyRza1KFfNJ3SaIBxhBBD6JKzZ0uEd/c+8FfTWsUx U/vGwFyVJ4ybjuFwQ1ylsg3ZLtGXLm41AoVPLgSjlYDQNXsIfn4hbV8WT9jVOz6O0Up6 j8Pw== 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=6NCPSU9YMgc5tYPLUs9oOihI6kgpQWabp/hc0s/EoCc=; b=pptm1oAWznKDXCttSDCh8xJrfCr31WlMgntyYQ8SRHhOyecEOtPWtiQUBrBZuDQEll J2CiQolBBQpWTISNSowzF0yjEzUkcjN3mErCn5gQMEOSGUhLBcxM/DfwkaXLMSL505mK 5lw7A2YWerlpDAvQReOHUWMjWVF7ijpMXnSUgaTsD5ng6HlwfTS+7OEnsVsH27tuJjJR mB4ZSnta5zXbiJby5Ycoi0M54kRGIZiyfoqmXKKfvkIpJA9ZcotiZJapV0t6T3CBDujL ziLTvyeo5KOkqi2rMNK6l0FpNFyKnEM+o4qg+UmGDXt5l3EAeN3txXexEpQkX+mHaCAB Ea5A== 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=6NCPSU9YMgc5tYPLUs9oOihI6kgpQWabp/hc0s/EoCc=; b=qkkXZjNgm8L6UR/ZRqw/5HqRSTn0+8VnBmXyEzWzcv5olU47vNJn+xvvt6nlB+75P+ kpziIWUzVQhH8LYeXfYKVOkDS++ITdDSXfwIQeP28FLQh+wjAT/1OBU1BZX5jLbx9TmW 468RyfHTr2GEM7Qy2nbMrZ6gsFVJEBnjdmYXaseGKPC1cPqzTxdfbCiyG8ApnpLF9vLD i+r6FuAc6kPzNqStPgCGMyzYs4jOh6cZJ+8936QrINlCjTAfMIgLq0iR0pVCc2yTPhhP BtQpZh+KuaCfUkkFXklMBPFZcTbAPa5SvnFQWAZQmXE2jFNvqNzYpPFJSmb1Fn5F8yX2 8QYg== 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=6NCPSU9YMgc5tYPLUs9oOihI6kgpQWabp/hc0s/EoCc=; b=SsPnOfgpsdiCfwBbZL68PkgfLNAWHx0SPDA7DcrLgBxSBD6cTTb5XU0TmfGUP3W3JF tPA9SSzPzavAt3wuoz7yERB3S+BvOL/k6CPMiHqZgatH8ErcUjHmgkJexey15wz8FjCb AU+SxswFEdHkwHBUmvxrSxr63a4P+vrai2cN/vqBGR81AoaWQ6EP33SUn+fk4EMpk6lB 0RXP6oxvM6Ts0+nGbVmDajKS6MXrC39C5atCB9QxPzCXkRlW3blApz9a/TbHU+NJglfX /MMhDNjpBuZ3EeEvSjc9GpnXylkoHj96REvccfBSfLf+xxhq8Sim/gSVnFbXDGmmy17p pk+Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gKpC/s/3urdgAwjjhPLFaxpZIhv5EUC8iJbS5bVZ1xIITL28Bav aRyQj7JASxHW6h0kG60eG/g= X-Google-Smtp-Source: AJdET5citxXu+IMeFutAfAJ2SZJNcmJ33uUnFeTQrw2keujJAFMsLgLG6CZ8r+AOWHWQ3ENRRyVjRg== X-Received: by 2002:a17:906:d1c2:: with SMTP id bs2-v6mr9947ejb.7.1541776020577; Fri, 09 Nov 2018 07:07:00 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:5818:: with SMTP id m24-v6ls312220ejq.1.gmail; Fri, 09 Nov 2018 07:07:00 -0800 (PST) X-Received: by 2002:a17:906:6006:: with SMTP id o6-v6mr430885ejj.4.1541776020106; Fri, 09 Nov 2018 07:07:00 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541776020; cv=none; d=google.com; s=arc-20160816; b=odyextypUB1mErr0/rzCuraZG6EX39PrWb1nDfdWDVkOIgHkveX3J1498XnzaD5cLh ajbg95MHmhhgmEXz1ojCTA6etHfuk1Ity00B5NAnkMHuXCvoK44tQXVSjHECOwPZ8joL WyriCzviww9vrB9/creamdgtRa/CqLAhQy4LeinKuTLdihGTDfS0YkTBuM7EpmZQfXhZ my4kNpFKbjLAjtknt51bsaxlM4hYev4439nsS0xuEZlIYPDNEuhWA7FZoMKp0sMP0d0I iNbEtSm/U7/ViPbt7Gi4GQoHRq83yRqiLpBOPla5NUkubo+ItJ2kfSOIGDy5LnnxQ5/T cLzg== 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=6hvjy+YC8IBCJkC6XzjHH+ehUr5W4jDn+4FdxRd1j/o=; b=AU716bOZ4vo6OeJ3rgMFJi+rtsIWBsw8pJxuAgky7LetDCz+C0c642ljWxbWeD1Lyy Mr6C1mn9tv22xrQUCxfooCbi/1TLbQKz1Ah/nfzKBGJ65SaGClFOJ37xIkPmXVeOQolo AeEzKhrjr07+r3Pt4Fn0B45qVxkDdM1PSt7MM2vgMtlEXUUZJMaRqfiLaiAlGntig7fE pUpSsrrNppf2uqdWPGkniEj9LwehATr3OYajt+veL3WohmCcCC1qFFBsOMl2sQspMQ5l 7tHnta2jtd1e5doCVb+tM+rJDbR0RiKEaO2Yfq6pGLKJChiR8AGJW0C56d/CJojv5o4Q o9Mg== 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 b12-v6si288214edd.5.2018.11.09.07.07.00 for (version=TLS1 cipher=AES128-SHA bits=128/128); Fri, 09 Nov 2018 07:07:00 -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 wA9F6upW019056; Fri, 9 Nov 2018 16:06:56 +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 wA9F6up2030085; Fri, 9 Nov 2018 16:06:56 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id AE11AC7249; Fri, 9 Nov 2018 16:06:56 +0100 (CET) Date: Fri, 9 Nov 2018 16:06:56 +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: <20181109150656.GA15025@mathematik.tu-darmstadt.de> References: <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> 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.150016 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: , Didn't deny that it's possible in principle for this very simple case. But something trivial gets unnaturally complicated when changing foundations. That's already showing that the new foundation is not superior in all aspects but actually much worse in particular cases. This is not unexpected anway that different formalisms have different advantages and drawbacks. The interesting thing would be to find out what is easier and what is more cumbersome in which framework. As I said in a previous mail. Traditional approaches didn't have universes and fibrations were partly invented to overcome this shortcoming at the price of having to externalize reasoning. But there is also extensional type theory with universes. Maybe that's better than the other 2 approaches. But one cannot say beforehand which setting is better for what. What experience tells us is that different setting are good/bad for different purposes. That's the point I wanted to make. From my side no need for further discussion... Thomas > 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: -- 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.