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-vk1-xa3d.google.com (mail-vk1-xa3d.google.com [IPv6:2607:f8b0:4864:20::a3d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 6646fa81 for ; Wed, 7 Nov 2018 20:01:45 +0000 (UTC) Received: by mail-vk1-xa3d.google.com with SMTP id 101sf1426931vkd.11 for ; Wed, 07 Nov 2018 12:01:44 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541620904; cv=pass; d=google.com; s=arc-20160816; b=CqIp3BMUVxKa/gDXhp8aGUQAskOcky5+iXcVwSdHdmNLa0mdZjQSyFpB/7329ZRCeC vI6VxDkjZVju3gy/XVxuH3ivm8B7nhVAsRXL83HQm901MIxDEfHOi1ic/ikPK1Lc2L/7 dNr0xzUr8FVER/9R4zVKFLLvUPWNJJnIsMNZEZJZDs8naMANxP43CiV4NfkShWR5l/8W GTdrOqqeTPVjCe7DDkF2kXqUS44gHQ+nIkNYPW7HUyIq2EQtwYTrg16DZlIh5H2EIPFV uzCubFVP5M1p/9svmgBttiNJI0mnG33mORP4XZv37qDTAss+noWeGLnA4hG1QuvGPRJ9 6RcA== 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=Ednn4+VgGODTlUWEyMIigLWJik6iXGIKswfue9rPWfQ=; b=a/gaeBhvzwCyGCXuV4am+FqEb2F9LzS4f/Ex3XdVG2BUuQmUOdnywpVxCFOfF9IFts U29MrTobCeo6JOnvOxVHbdaAroIw/46koandbU0VlokYOQ1xSOlS8W+nPQc8Gn6fWn+J GGbPTd1xY/WWtqzlkG3/jjP5MV5aBAqC1DM87avlYnFj9hTn6NUE6v7B9IWwRUKpToHQ FbAOxms7bnxDts9NOPZvPBKXL/OwKbeZGQn7N6mhyCx+ipjzgdRVZWpsQCAyrADjTjwr IdhVqNBHmM6MwRqKA9Oygtw8Hq4bu4RhbHbv8eJjBnAg6pzEzQQ9QPwbzjODOpNSrRLr am8g== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b="WtJGirh/"; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c34 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=Ednn4+VgGODTlUWEyMIigLWJik6iXGIKswfue9rPWfQ=; b=DJA0IqbRORwIBMq+Tgm+cSOhRzNKeIi89B07MlV0d2ZlPotTaES3gvkfL6SSfpTS9c 1ugSOcqw2y1gGs0Ch6buSXAm/v88FVeJCIT/lwrQDKgPhLgcm5sc3+4ab1jF4hxXLwXt KaaDn3Y3X5jhbEDMeea7gBOnW6NGQ6j9LXT5oWk/pG67pZTBTZvaDEOFHL01z8jQfEMH FhpRCt5MA4NfNyAw1J5h2JUy5vtXoadIG79/6Ue3qDN5Yd+80OxpF7j+U2GLa2ZyWcSX PVUmsw90xk3jMY7/jwkdITynacz6SarA+UIBo6FtGOV6YRp5bh151clB5WkDVJB5geSK axuw== 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=Ednn4+VgGODTlUWEyMIigLWJik6iXGIKswfue9rPWfQ=; b=EbG+ypZdqtCisAfzr1UlnJuYDZW7yrkes8AFqEvkVMfg8JHWVO1fgN79OTVCpoxRK3 gV5G3zunkGNaVJOafPaq6RUnU6ZGN4D8+svanKU30pPcRZhEfdKhQ+PazVHbe2I8IqKB jJ/OvwUGk7s5yTCl+/lyzLlsRT1Odv6VbwNfXAYkYQ/Ji8D5bNatlR1lfwKZAdfrYXUL EIMIZ3uh+Pdnnp1IGIGuj4pqWArS2Z7KSguzKneYFzk3q2SLVfbzEHF4aGWXVoDM+VaV IhgQzqHJnrXbdgSyFcRX3dIupXkimPBtRZC9vT7ocxrzrnLjo+XXfQRiraWtIjdqghbC aprA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gKeWKMw58nJRmsFKPQTaltk8If168zyeiUj+QLdt9ASXljyVBU1 b4G1vqTWjTQiSngMJZLQoSY= X-Google-Smtp-Source: AJdET5chQzNfnNKKXTdc6ppdgziFnZkc0+drrKU4tp5PFTMXbIWLNs5j/iFebiwzY3FhS38o6tOW2A== X-Received: by 2002:a1f:9613:: with SMTP id y19-v6mr4753vkd.0.1541620903906; Wed, 07 Nov 2018 12:01:43 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a67:e146:: with SMTP id o6ls3042740vsl.6.gmail; Wed, 07 Nov 2018 12:01:43 -0800 (PST) X-Received: by 2002:a67:ba05:: with SMTP id l5mr1371155vsn.18.1541620903607; Wed, 07 Nov 2018 12:01:43 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541620903; cv=none; d=google.com; s=arc-20160816; b=Tduk0RSeHpXb0hJRvUPsngEnUULiqtUuxNt4l4BMvMD8DfEILyshr+kZ0iDzi5+jwS qFhZ4Dl7jAex/DnxNICiJ9Mh02lIRwuJSj8j8lrfzXO0zTeFWtAQK8mu2+e/xCJXc0pO hJTWUhCKUmaOalI5La2d5ff9hQN7SuTN1ovlC5jKRNjXCcjiIfbyzGI/vm9cDavfxiNv 4XZzf47e4H4Tu81BK0/n9jGSp1x9G5Dx55UpUZGNlVlPInbQebBAJYhZl+ToFq3mbv0I sEsRazyVh9ruUjcoDwcypkC668IIaU/zNmF0Ys81DURSamCGaXAEjjesRo52hr8cp6c3 6U/A== 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=8IPTGh+OPUbHBMLNU4dtNHkTQKRqyRJa10yKfig05Ro=; b=XxmXWbnNks1mcJJfsDn/A65By5N3RNz4OdAkUIX6MYhtlY9+YKJkjmdJUmF3x7QG4j DeLGkt91ANegchN6S4tHdWamtJ9iAjn2k6vnPaOMAKPxpOuSpD8MxLUd8k5Dvx6DzaUK zcEqZZxFx8YiKusw04by5i+Di5jUvTg/PBdIAaYaawXGWWgPaexUTXsjkWGrNmqu8eXK MeiIAyiQ9XnU3Z0S4ak51QYlD+7Qha2XI0kalKdVI1fz1Qj8KnpudK1j7T2Vo4avZ13h BKQ1KeaKXKCro7umYmwXiPX61+SZ2qhtgYX+qZJYJjRf2Gcj8o11NT4BQWBq3xx0keEW hamg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b="WtJGirh/"; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c34 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc34.google.com (mail-yw1-xc34.google.com. [2607:f8b0:4864:20::c34]) by gmr-mx.google.com with ESMTPS id q8si42635vsd.2.2018.11.07.12.01.43 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Nov 2018 12:01:43 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c34 as permitted sender) client-ip=2607:f8b0:4864:20::c34; Received: by mail-yw1-xc34.google.com with SMTP id j75-v6so7085294ywj.10 for ; Wed, 07 Nov 2018 12:01:43 -0800 (PST) X-Received: by 2002:a81:7506:: with SMTP id q6-v6mr1660414ywc.51.1541620902959; Wed, 07 Nov 2018 12:01:42 -0800 (PST) Received: from mail-yb1-f174.google.com (mail-yb1-f174.google.com. [209.85.219.174]) by smtp.gmail.com with ESMTPSA id s129-v6sm363317ywc.41.2018.11.07.12.01.41 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Nov 2018 12:01:41 -0800 (PST) Received: by mail-yb1-f174.google.com with SMTP id i17-v6so1056816ybp.13 for ; Wed, 07 Nov 2018 12:01:41 -0800 (PST) X-Received: by 2002:a25:a349:: with SMTP id d67-v6mr1696843ybi.334.1541620900997; Wed, 07 Nov 2018 12:01:40 -0800 (PST) MIME-Version: 1.0 References: <3c553ba0-2181-44ec-b790-969a8115ea1f@googlegroups.com> <1a3288ec-ca0e-48ce-80ad-9cad01f56845@googlegroups.com> In-Reply-To: From: Michael Shulman Date: Wed, 7 Nov 2018 12:01:29 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories To: Peter LeFanu Lumsdaine Cc: 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="WtJGirh/"; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c34 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: , On Wed, Nov 7, 2018 at 7:55 AM Michael Shulman wrote: > I doubt there is *any* > choice of terminology for plain MLTT without UA *or* UIP that is > sensible in that it can be specialized to the right terminology upon > the addition of either of these two inconsistent axioms. Well, with tongue slightly in cheek, here is one such definition: a category is a precategory C such that (if UA holds then C is univalent). (-: -- 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.