From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCYM5VPR6ECRBXUMRTPQKGQEMPK2NFI@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-wm1-x33a.google.com (mail-wm1-x33a.google.com [IPv6:2a00:1450:4864:20::33a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 5ca8f781 for ; Wed, 7 Nov 2018 15:35:59 +0000 (UTC) Received: by mail-wm1-x33a.google.com with SMTP id f3-v6sf14563942wme.9 for ; Wed, 07 Nov 2018 07:35:58 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541604958; cv=pass; d=google.com; s=arc-20160816; b=c1xtzkpGLiTCuL32ywsrRD84kj7eedKz9pCdABF9/0MgtQ3QDKASULu1hH7Y908X0j 8/1mkHKK+gdonowBxRdgPCKDmUMT/8lGJGGOpMQfUkPZtZclmOg76HWccFIEvaDeDKr1 FaEgX7k1RY4E8TgMojuuMcdM9BV7ZObZU9hmzfWrOBo4cbIGeoXMSQ7KIg3no+2s836L TlJz9bgdOucgh6X7U48+wSg2HHscK2NoeSd+D4esOuJrVKWkzIn+Hl4D0UugEwMQVkz9 2n3EETq/r38i2dJ5hbtqdW7uSH7AiP5yluj5fUcABGfrPki2B3keCjUn95AsMY6oyRMK uhRQ== 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=/58mjpYc4930Z9TXQxZUu6J+60Ctfvt5FkTtEPsM5t8=; b=X2GOmPy78dRtkQGAZPMNmqUwdSfLxIOQEWlFDlEnOIY3hvnN7l0y+s2xbwzjGsznrR dx9wERP2WYe3O15Ukk0fKm4ijOuCtvNyWIBOnBDOJ5jpmf2F754zyWRL71xxPcmbTUo6 AVnSI6AN+gmhmpe8Me5TzUOaTkwmbGJtfKsn/S/9XTHgiu5hMBmPyuHhdLX1a1wP41Wl n2UV+54D8ZVS9ZKEs2V7rNDwwCLmeG8OJrkDxKMe1Yb+nBrqfQCSufBPZjHKCHENLV7Z rUbmYP4Bo1UE5pjcKB8ZV2dkcQ3FLokHZAvT0Qbe8qWQcLTNtGIF3y6LxCEzDEi/lGr/ SMmQ== 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=/58mjpYc4930Z9TXQxZUu6J+60Ctfvt5FkTtEPsM5t8=; b=CO3EX36Gx78JTjOZPqjrH7KJ+7KQ+QAS8dfQfkdVfs2GXdXeVpnuBcrUgqexDbX+dX R72VuZ/zNF/UpBKeI4ghM6RoFTmWOmic/TxX5PJHr/4/mijRHaVr2zH8FjR7IZWltyqX zqzHBTwgihkUw1/l15RgH0QCd7YTQwfF9CJZ4pICvaEIAjIZTA5dptoIUQLa+JuqSe4Z jhICAjw9FFWORpCFNl7P1T9wbIz1yPTM9z6IRzB2sc7cwEBOtde3q7gx+rI3CjxagLjg eUyydt5F5JNwTWR4cEI1+FqROEglVpuuc1aOImcu5T33AWNOb5MB/WjwvP3EowXeasP8 vSpw== 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=/58mjpYc4930Z9TXQxZUu6J+60Ctfvt5FkTtEPsM5t8=; b=HFdH5MfRo2gtjRpL+9adNCitXfBsnYkwHml3M7r/kfB2/zYUcrICxg/2vo13wtmT4N /nF3U/Qcel+ufUjJLC5afCc/2QQ7xCX18vJH1iGvaEhTWkdSnv0gfOQwJ5aqu6d+ZQd1 mOfQgeOEbVOEylanIFKKfix6nouHpoFM0kzdffl7ZWFOeeTbQsAXnNUfox8pNY8OtXr7 ZQiKYTZkk85uiv6rdbUdze4Kz35q/P2Bf8ADGScSOuNsoUV1ZWPe9P23Ar5xcDFGOX43 2SLil+5pOhjui6GZ0Ef47JM5tWtbovv8qjXP5biwQzgRyOi+lgtkGd81L1upK5HI55af RteQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gKzb/doO67WS1LNh7Qzw2uEes9c4F6qBiu0HKrhmJreo23K3RBD gKL3xX4/YaEljthCHQiwDq8= X-Google-Smtp-Source: AJdET5cEBSB7YUMRVFcbIScbdhDr8hSKhslAFZSOqlMFZLemzDePSIQdGfyan+XXe1eFHyb6U/DXhw== X-Received: by 2002:a05:6000:10cf:: with SMTP id b15mr7746wrx.4.1541604958714; Wed, 07 Nov 2018 07:35:58 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:9c3:: with SMTP id 186-v6ls2398722wmj.2.gmail; Wed, 07 Nov 2018 07:35:58 -0800 (PST) X-Received: by 2002:a1c:9645:: with SMTP id y66-v6mr162473wmd.6.1541604958299; Wed, 07 Nov 2018 07:35:58 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541604958; cv=none; d=google.com; s=arc-20160816; b=xxyWDkL6Q7KxcLer5jSPcPatkscEe0Edyi9oOewR01w3ebXiQ4DR3GJW3c2ujYduwe Nqr7DY8v+nNZ4kderz6XFMdcfifEoa/K6+S+Jw8/2EatRnkotmvpeoU/xAGAsUiLfIfm Vs+GMcISUivmzkHw8YTZ7wRLzn+8mvxKT+rUK1KnB2M4O87J5Pz+LF+8nz+Dry7aWhJP V5D2kkB18lobKVxcu/eovZoIFWM/mwVUq4qR/H8W4PbZnwxmOXzDcXROo//LDB6dn/1a sF8Y6WBvYQNTb0RzepYISKDPfndnZZkzOXVog27Fg4KApWxeyXbp4GjWyn48UHM3+aC0 WPXw== 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=pFgLCz7TowLmOouCnVRwr/xWdKzguY3XSURQ5C46nC4=; b=wyRBPx3p0KAlSHfPvpyi+4Oia9yxm10ZESzaG3+j4+pVB90CluaY5LEyRo505wLR4Q Ic2TG4LcHxE3uXXzq/XU4lTBQonq9eaONnc3MBGf1fwaLNtHYzWhajBjapKYJFUHmLgK mU8cnVe68f9nxwlaitHnDGklIt8AwA22wQt0jrEE2xFl2UZ3ySoyuYRj5kj5+671023O C+LNqOxYdoX8xRUwnbXi+LIu19QAn0f0YQndQ+doMTCqhZq6XDRTanhq5mARomHruM6l +zRc7DnKCSww4DQZ6mqlMLUdyfkVUlYiJIKKwOo8HsJLMHmjnQEdwDO33nKh58OEbMOy JSSQ== 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 n6-v6si38750wrj.4.2018.11.07.07.35.58 for (version=TLS1 cipher=AES128-SHA bits=128/128); Wed, 07 Nov 2018 07:35:58 -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 wA7FZuvY013828; Wed, 7 Nov 2018 16:35: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 wA7FZup2032632; Wed, 7 Nov 2018 16:35:56 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id B1DBA1A39DF; Wed, 7 Nov 2018 16:35:56 +0100 (CET) Date: Wed, 7 Nov 2018 16:35:56 +0100 From: Thomas Streicher To: Ulrik Buchholtz Cc: Homotopy Type Theory Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories Message-ID: <20181107153556.GC26970@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> MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Disposition: inline In-Reply-To: <4ae4c745-a00e-4ebd-9de2-e29474b75d48@googlegroups.com> 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.152717 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: , What one calls a category should be a set in the HoTT sense, i.e. validate UIP, but not a set in the sense of size. Every deviation from that should be signalled by some adjectives or prefixes. That reflects the practice in category theory. 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.