From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCYM5VPR6ECRBUG4RPPQKGQE4UEM6OI@googlegroups.com 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 bdfc6955 for ; Wed, 7 Nov 2018 13:53:21 +0000 (UTC) Received: by mail-wr1-x439.google.com with SMTP id d16-v6sf14937693wre.11 for ; Wed, 07 Nov 2018 05:53:21 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541598800; cv=pass; d=google.com; s=arc-20160816; b=SiTF+61HQYV4OSyr4sRsPgpSxnw6lahUI4vo6/FnzpMso/1pJ/AvJ/752FQsvW4WyS AsqS5mZIEkf2H+bhKrqiN96YZndNd/+05RZ3Z5dKsWRE6xf8Tr6hHf3MwRlnfVbu0jfM u/sPDJq2byV/wwb+DJeF/z0MTy81WlDIBOtW3aR1tbxLrZWRuxwkMI4Ra8GlhQXgxI1K wUyYeXnQ3+rONjF00F62Q0IXpa9BaSbohuu7iixlhV061IS1E+hUK6RQQr5FM4dZ11Nq ixu1BRUXLyMwFC5mJCvncgFJ/ttc4DdQuoJNrntAfy1qmkWt3dd+/BZsui/mE/VSRgKW LgHw== 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=HsGZSiwM/nWtYDK0qaVI+NycDHJrk19a/R55lwlT3LE=; b=NZ0zGQIH2vHkQTr/Ebgb2ADLjJWx8Xzt0QlVc6h2tvlVF8VjOJyvVFN87Q6dOAeCnd QpWlmPdo9BjTwKfT3XKZFaVg2xIbUMh0eMBVqwQLCYpXJdDhUxXO/pCohBZkNuqSpdjR c/6gqEF+BYBAavDKsLloI51dAYCYrGoaSr1t4DvEBAsO7nwZX/k5Q+9ikzJD0C1P8QyI rL+I8yw11rrs8NU00V3qNtEXzWBvI5HBZXgChlKwARPPqlA8LRzKoAPhJaxQBYIO/gQj nGyozqsAIx5Pm7nh4gXmBTb55/VYCmJb3EnVQtSc0veRfG3IPTwA2ybeI912wsjCgTwz qpVw== 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=HsGZSiwM/nWtYDK0qaVI+NycDHJrk19a/R55lwlT3LE=; b=h5OgPFKWHCQK2zKELO1lJKHAGqkm3g4/88SZEwxZfWJzmGwwKvejul6S1hR68mgmVi P7lvEGTFel1NxhR5EF5Pi7RtYRp22Sbac1Z6jW25FHbkYdfVpTmWpaeAJrH7kkSwCL6j rR6gLNB2Z+B846CpHFYRP/bFnhFD1eJrcIQtd4sQRjgWhQ7oubjI1rsPoacShqNlYcFM ElyNukL2vMn1TgPbUTbk7F+UP+cx6JFnloLepFlQgSZbrJGiV/nQZfhYb6mwC5v6388A gp/qk1RIGgDC6frxLtfMfFRGb4QsSLxfPcE8LjimRe4F8binmiX6AkEJKkTst00CxMU/ RVZw== 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=HsGZSiwM/nWtYDK0qaVI+NycDHJrk19a/R55lwlT3LE=; b=E8KDxDlgh7OAXeZH0M2XYeoO3p0p3rvTAMM26SyxVOzGKGqFj2iiMB+dhG0odljVEW YH1T/kdYMX4lG3EDDE6yirZV7rWqHhBdhJSLAwm98lKCH5zMWlaapmcguyhHepM0iOe/ emUVQSmlE98hStaVmGl3b6jyjJI8zx68su/iBrh3bC0bVc7mP4OidA8cCLD3tJolXnfS 0KnpH/hHkyVzYmwu1obvz1kWqZWbfBFaIlU7O+YlcDGBwM5kHI5bxRILU04lcj9hovE7 udvJk4TrOgRdd0WPEeDb+DbYu/wg48EkD4PJ9nm8Wki8LJZAEoLhRzrWqAPjDZXmtcj+ QJJQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gKdxQucF/SbiKv7HB6aiWH1igLbaMc7XZ+n0ytNRCEnJ1q7qh7v l33ED4gF+SgTjHuvN2c66JU= X-Google-Smtp-Source: AJdET5d/IEQUnM2KtkYGAsAwAe76H27LU4VbJoioi7xpXFgITL6mMED/rt73NxFbBLrZM2MYY/ThVw== X-Received: by 2002:a05:6000:10cf:: with SMTP id b15mr4085wrx.4.1541598800873; Wed, 07 Nov 2018 05:53:20 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5d:4cc5:: with SMTP id c5-v6ls3072553wrt.30.gmail; Wed, 07 Nov 2018 05:53:20 -0800 (PST) X-Received: by 2002:adf:f907:: with SMTP id b7-v6mr61173wrr.21.1541598800495; Wed, 07 Nov 2018 05:53:20 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541598800; cv=none; d=google.com; s=arc-20160816; b=TD/gVEJh6YNLNlUpPtcxX71yi5iiRN4kDiIjp7YlUpjSGn2yN41f34ffyO4tyuXBwe tZGv4uJf+HTy49TGzM3f3tla+FPJMc5ixxY9lrm1FWlCbZiP6YFLpC9qkLfastc7WooZ TsIaMxkF/NZMQKKKPTYhjQ6RJiqi2hqzWnM4Irq1oT9Uztl6r5r9dWrb0e7sDjEO4gU9 7PEt1/vnAJbBovdRYi0Sx0Ymkgn5cs9RveZqlvnmd2x5zs4uP5O9HuLVox0WB35lHrTH If5CZEeE1nuflw+5J7ukd5I472/ZHoF6u+qbsXVBwsGeMCRCX4LHXkMJipzIzD6+zQxi AJIQ== 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=nZXvFTbW49HE6j463M6msoeOFROIn3hJO3h6IgtWwNU=; b=QloTwIRjNi4nxc8StK40jazTnI0qlLeSbVREPVMdvs5wkrFbaY9+kxzoUAkLMIUFNT tmU3z+yWe2BQhqg2pdNm9oiUEywdfxxzY0UkKk3FeI6U/sTZ927f2KSxm/PXU9HfZqy7 kpWCP8/5jhj1oUCoklEIMDCybBOfJs4d6uQO7bCCkEKmI18DjZVnRTRlHrzzXBCpmqmU Ks/klc2odDIPLlrcKDNBYoZF7I3xu8ntPNq4sGogBhSnzm351ZIL5X7XtNV8NlwL2eSe sKwSOSwQ19YAi6g2i+sXilL5PIqCBS4fMdhW2mi/Vc4S+yeJ0eC4x8M2YmOZv3FAPZQB X3zg== 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 z129-v6si28686wmc.0.2018.11.07.05.53.20 for (version=TLS1 cipher=AES128-SHA bits=128/128); Wed, 07 Nov 2018 05:53:20 -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 wA7DrHiv021596; Wed, 7 Nov 2018 14:53:18 +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 wA7DrIp2031423; Wed, 7 Nov 2018 14:53:18 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id E293C1A39DF; Wed, 7 Nov 2018 14:53:17 +0100 (CET) Date: Wed, 7 Nov 2018 14:53:17 +0100 From: Thomas Streicher To: Bas Spitters Cc: =?iso-8859-1?Q?Mart=EDn_H=F6tzel_Escard=F3?= , homotopytypetheory Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories Message-ID: <20181107135317.GB26970@mathematik.tu-darmstadt.de> References: <3c553ba0-2181-44ec-b790-969a8115ea1f@googlegroups.com> <1a3288ec-ca0e-48ce-80ad-9cad01f56845@googlegroups.com> <706ac90f-ebd1-49f8-bd0c-2029549373c3@googlegroups.com> <8fffa0be-9bf3-8a7c-ad75-ae2249f2ebd3@math.su.se> <795a64b4-f62d-4fd5-9503-20c997b7b42e@googlegroups.com> 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.7.134816 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: , It would appear to me as natural to call "categories" the most general notion and "univalent" those ones which validate the univalence axiom. In any case the word "category" should not imply univalence. But there is a point that one might call the most general notion "precategory" and "categories" those precategories whose hom types validate UIP, i.e. are sets. But then univalent categories are not categories but just precategories. Why not call the general notion "\infty-category" as usual? 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.