From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCIPFMNR2IEBBSPCRPPQKGQEGGJXF3Y@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-lj1-x23d.google.com (mail-lj1-x23d.google.com [IPv6:2a00:1450:4864:20::23d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id db168b14 for ; Wed, 7 Nov 2018 14:06:02 +0000 (UTC) Received: by mail-lj1-x23d.google.com with SMTP id h77-v6sf3379995lji.10 for ; Wed, 07 Nov 2018 06:06:02 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541599561; cv=pass; d=google.com; s=arc-20160816; b=QXpPygVyFIFr3PL2Tw+NkxwiTueJ2NXiEuznKp3B3qofA1WHULS61eFYp8FVFx9aHM A6r/IXYyvYthI8IJPpIA78vsms5KaLlvJW4rtv5BGtbWZTBmInIVnqwQwhqJ1JYvkrN2 PoX5G51V5cUxNAr69tVBiCWy5q+QO4udjgmq5AfKAXBedQxBvT3nRjr6hxjWefSYRRMO gSj+NzL3XHrQkcB6Lg53epWfsYUJCSznDCa9JKpVySacXGCUYiFuTXkoUx+MljlaQGLj e5N2cr5b9LH7X62YTRDfBsbfWzt93BY5vEu9rUb6YJVp64TUDQ9+68DD/QQ12h1XTlgF PXHw== 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:mime-version:content-transfer-encoding :content-id:spamdiagnosticmetadata:spamdiagnosticoutput:user-agent :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:cc:to:from:sender :dkim-signature; bh=QCLAyqn4iNZbW+602NqB+pznat1rU3HPevMEjFyTVMg=; b=riatlGozD1ES+EL93xnD4c38kJdvCJCbwy+1madHpyEol13xbGr9Fxatst9vsIbpwN TfCTOLhMS63HohTBa/Yoh8lVZsMvLS0mIN13C1UgK9oLHGYrrnAsf0L4Jf1NHxa5FUVW Fry74g6M3zHM3FXAVkMwlJDgt8DOXxsz3PCINQEewQd5haI4GIXEYDLT2JbuX8TF9lCE acDZ9Nfme/y6X9T5RuG80fUEeM0D/5skrqChgjoibXjT2pxGGfQi22vUrttj2pLXvtMS P2O9/XVrXBfNLXpJjHqhX48Nss4lAQfCUL2w472Ixm6SG1U8/S5MGyxY+I/WUwKwJmE+ Pyrw== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.124 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:cc:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language:user-agent :spamdiagnosticoutput:spamdiagnosticmetadata:content-id :content-transfer-encoding:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=QCLAyqn4iNZbW+602NqB+pznat1rU3HPevMEjFyTVMg=; b=Ic/6f3Szc/3QGNIXfvDgKExksofdwosUjvfGYGGpTuYiBZjkRFqMKIX0Q+byD66/uv O4rWFssZPJXUL2dZZLN98TqIAMk9g84pwliXIXzNzMbJQsUp8erefJWtK2FXOhomX0SJ 2Gy57HjMrOtZb/t6gcSFawk6K49pswenLh403mwGV/7BOK2MJK+YzkTjFDSeocy/NPlG 5Wt9dSvZ+pNfBdEJpcu5qRnbK7jCOO49RGa7FJQjcQso1BEdcDrV6vtULcRqzVNGO8W8 iNiqeeHg5/ussjdWGNgOtxlUKO8RLnDlXJxF1236db49R8NF6kQ8ldqrkD/HPLtjFsHW Hslw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:cc:subject:thread-topic :thread-index:date:message-id:references:in-reply-to:accept-language :content-language:user-agent:spamdiagnosticoutput :spamdiagnosticmetadata:content-id:content-transfer-encoding :mime-version: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=QCLAyqn4iNZbW+602NqB+pznat1rU3HPevMEjFyTVMg=; b=iXICsuU4b70u618bbwBTmyhqViF87Rz502IzKLbAa1LPMNvbCkLz1+5yGlR/nOxlz6 d/cf6Za+MqKwM77PZK2w3RfyLg5sAgeVFA8bgm5nqXecss88VxsOZDSNTZ7mBLXPxf3G 6rnqmQnQxszjOwPy9YVOQS4OvMqUe211EdHRlF3u20yPTFDu6v1f+SXF/EuohoGm0P1x uWny+BqWTszcC9Nk76yD0Hzx9833uWCLESiitPPjzt1sCtr8cLv1pf9B7pXQryfc0DUp kF64bpB8wnKtfx6XVS1I50McuFcixdZpXHISDoEHN0O80jkd6mGA8+JnY+VB+ff/l3Ll TDmA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gLTi/g3GdvQ/DDv54euevtuFminbDLo/EOVcUipg4U4z/i5sn+p tUvyc4TOQtQaFpR3XNA66bg= X-Google-Smtp-Source: AJdET5fFBUTor0QAHWkSrPH8S78zscfAev3goTIZk8/wI6HfB9+1ZcQCiJE1nmsPq2HZP2gEvgS7IQ== X-Received: by 2002:a19:e34f:: with SMTP id c15-v6mr2569lfk.0.1541599561639; Wed, 07 Nov 2018 06:06:01 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a19:f65:: with SMTP id e98ls1004354lfi.4.gmail; Wed, 07 Nov 2018 06:06:00 -0800 (PST) X-Received: by 2002:a19:7510:: with SMTP id y16mr41888lfe.9.1541599560938; Wed, 07 Nov 2018 06:06:00 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541599560; cv=none; d=google.com; s=arc-20160816; b=EGOoSar6osRHeQKOHDQjeErJdgqE2JglWxrKBUJdCmaeeqizcfACJwv0v+Cuswr/gv DPv87CFyqDBPsQwD+ht4tHDf1c6+lfjC0oIJWpI/+cRsQsWQsIUS67uBLEE2QVKzWf/f QJCOKUBJ3XdG0iEPMuWA6bCOeqgRpLrgHA5nJa4xJz7joH7Jw3XSSD85rqBtkvsvKNDz jQ6V0yhAVdZ2Uxx/eL6cZO5zBckAsFLZ8Cxldc00y1zLAM3AV0kVUZbg4Ylue2OZcwCC zFtS+FpGPADn++iFHzMi+aHCEDTJYnurYxO3nEt3Dsj3E+IFoEuQEuw80+lj/ud/GEeM /1vw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-id :spamdiagnosticmetadata:spamdiagnosticoutput:user-agent :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:cc:to:from; bh=T8jNsoO0vs1DLsacF5BHwA+cNDqFS1KkR8Ag9dL6GQg=; b=VApzPPKhig6GQ5jmxYlfd+31eSM7gINHXuIPtzYGvS33jZYIUqiKM8+WVu0l8wrvY6 9H2aBqZjF5tPifXnYbN07fYvUgwAn04hA1YUdz6fhdLQFp/iOnf2sjGcJPD2mq0KKnaz HQZZ/g2MwDXTa+C2I5dO34Y7BRflXhbTjfS/pDr7J5nBwa9g4wN3ouaGO2T2u8r9liDr 9XyhpNf9PatABlP85yKZqNpQO4XvJSMeihH6oss0CjcBMnmWpRPYlLomrhptW2xDjkln p1kh36/JWS1LNeMVGqY3cui9vvOEz0pmx5DtP9vvbUKAL8d4T1nbSaRmIK6lR3ygLdgv 7LwA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.124 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk Received: from uidappmx01.nottingham.ac.uk (uidappmx01.nottingham.ac.uk. [128.243.43.124]) by gmr-mx.google.com with ESMTP id a79-v6si29543ljf.1.2018.11.07.06.06.00 for ; Wed, 07 Nov 2018 06:06:00 -0800 (PST) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.124 as permitted sender) client-ip=128.243.43.124; Received: from uidappmx01.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id E5CD73C5B89_BE2F147B for ; Wed, 7 Nov 2018 14:05:59 +0000 (GMT) Received: from smtp4.nottingham.ac.uk (smtp4.nottingham.ac.uk [128.243.220.65]) by uidappmx01.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id 209243D2D1B_BE2F147F for ; Wed, 7 Nov 2018 14:05:59 +0000 (GMT) Received: from [10.159.172.13] (helo=UiWexEDG01.ad.nottingham.ac.uk) by smtp4.nottingham.ac.uk with esmtps (TLSv1.2:AES128-SHA256:128) (Exim 4.85) (envelope-from ) id 1gKOT0-0005ZP-Hy; Wed, 07 Nov 2018 14:05:59 +0000 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by exchangeSMTP.nottingham.ac.uk (10.159.172.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Wed, 7 Nov 2018 14:05:58 +0000 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.1531.3; Wed, 7 Nov 2018 14:05:58 +0000 Received: from UiWexEDG02.ad.nottingham.ac.uk (10.159.172.14) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3 via Frontend Transport; Wed, 7 Nov 2018 14:05:58 +0000 Received: from EUR04-HE1-obe.outbound.protection.outlook.com (128.243.226.54) by exchangeSMTP.nottingham.ac.uk (10.159.172.14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Wed, 7 Nov 2018 14:05:57 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB5486.eurprd06.prod.outlook.com (20.177.201.158) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1294.30; Wed, 7 Nov 2018 14:05:56 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::4f:450e:6b43:f35c]) by VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::4f:450e:6b43:f35c%5]) with mapi id 15.20.1294.034; Wed, 7 Nov 2018 14:05:56 +0000 From: Thorsten Altenkirch To: Thomas Streicher , Bas Spitters CC: =?utf-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= , homotopytypetheory Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories Thread-Topic: [HoTT] Re: Precategories, Categories and Univalent categories Thread-Index: AQHUdoWaEWRL1VfTr0qqVzzaadLFAqVEJ8sAgAAJYQCAAAJGAIAAA04AgAAE8YCAAAujAIAADhiAgAADiIA= Date: Wed, 7 Nov 2018 14:05:56 +0000 Message-ID: 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> <20181107135317.GB26970@mathematik.tu-darmstadt.de> In-Reply-To: <20181107135317.GB26970@mathematik.tu-darmstadt.de> Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/10.a.0.180210 x-originating-ip: [128.243.20.140] x-ms-publictraffictype: Email x-microsoft-exchange-diagnostics: 1;VI1PR06MB5486;6:GocW09Y3qeb+BzcrCHmi9wLt/KCNg9nz/HP30izxyuVJmHXlaW/RBiAH+SOd/aWhzE6K191CpObl6+N4g6++a1mcna9qsHqNd221QrsdBEg0Z4n9C2ieWjTZrcZ5mvicKgYXaNmfB+eWLx/HwxIDaaxv0pRLMVjhhKaYp4wpBhnCy0XxiElQVyp8ZszTGUjloKDc5SzQk4sSe3LWumxrOwCrn6xRZoZnmaQ4xDPERL21i9TDM84csqY9j6nevbZLXXov5ZzsXKbRtnhgNHxh6lvfZzptdC13KBud/Q7qB8ydAIbzwnrZyHxp0FpMQwYqZqBgfp7iUAXFGkiEczLlV51JajciEmR3BAuyhKGT3yr4oPdWRwXQXHHdbME1Zs9TYSOFJS0y9HMdzHHFk9n8DH5hB03WKMMR9mu3ySgsEC6H6AIzbgYfXy0fFqWtDzUIIUROpTPmGYxwQhI+GjvPtQ==;5:jdYr6i3Jj07n8AM6o0DvU1XP6ITVY0G9I97S/w2PUMriLd1LWHhAjuXqNEvIV295wvFgPEXYQYjx0yQ6fA5foWYZZlsZPV2hLWW+bk83zDM6pr8zP+FuASuWiUztrtANdc2i5WTpY2MQ+ydYm3KOG3NZTN6Mso8uPUZZB85TXN8=;7:2QLkA1uv32zqc62e8oTG2PUKpFeXd8aL4TjbTVuFnnd6FEgE3zz4JIlh13ekNqzgwxNJXutOvlRZKkg+x19Di0GkVIzR3m4W4HIAaF0x45WX2FTB2Z5mxmp2TAOjK2J0LVRTfU0/Ckb6lt+fYXnQ8A== x-ms-exchange-antispam-srfa-diagnostics: SOS; x-ms-office365-filtering-correlation-id: bc40c93a-d6c3-4316-fbd8-08d644ba232c x-microsoft-antispam: BCL:0;PCL:0;RULEID:(7020095)(4652040)(8989299)(5600074)(711020)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(2017052603328)(7153060)(7193020);SRVR:VI1PR06MB5486; x-ms-traffictypediagnostic: VI1PR06MB5486: x-microsoft-antispam-prvs: x-exchange-antispam-report-test: UriScan:(215639381216008)(228788266533470)(211936372134217); x-ms-exchange-senderadcheck: 1 x-exchange-antispam-report-cfa-test: BCL:0;PCL:0;RULEID:(6040522)(2401047)(5005006)(8121501046)(3002001)(3231382)(944501410)(52105095)(10201501046)(93006095)(93001095)(148016)(149066)(150057)(6041310)(201703131423095)(201702281529075)(201702281528075)(20161123555045)(201703061421075)(201703061406153)(20161123558120)(20161123562045)(20161123560045)(20161123564045)(201708071742011)(7699051)(76991095);SRVR:VI1PR06MB5486;BCL:0;PCL:0;RULEID:;SRVR:VI1PR06MB5486; x-forefront-prvs: 08497C3D99 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(39860400002)(136003)(366004)(346002)(376002)(396003)(199004)(189003)(2900100001)(7736002)(39060400002)(6436002)(68736007)(6246003)(66066001)(8676002)(81156014)(14454004)(4326008)(81166006)(305945005)(33656002)(229853002)(478600001)(97736004)(256004)(14444005)(5660300001)(11346002)(446003)(106356001)(105586002)(476003)(2616005)(486006)(6486002)(8936002)(25786009)(966005)(74482002)(82746002)(71200400001)(54906003)(6116002)(3846002)(71190400001)(2906002)(93886005)(6306002)(110136005)(58126008)(186003)(786003)(316002)(86362001)(6512007)(99286004)(76176011)(83716004)(102836004)(6506007)(53936002)(26005)(42522002)(42262002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB5486;H:VI1PR06MB4029.eurprd06.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;A:1;MX:1; received-spf: None (protection.outlook.com: exmail.nottingham.ac.uk does not designate permitted sender hosts) x-microsoft-antispam-message-info: d5sZCOTaXbLP/k6R5tcq5QwVjNDtnqSDPXMEimb1py/lm/HcdwnFm1sDtFwXKB1sNaXz1C4SK4WJ8qmW3sFAb8e5VNkS0s+t18W26tKcfCJKbNMcwuyT9xdYKyunJHSsdfGZVQH//dhXyTn3JWFTYFVz7XSLvjAPhYXj4R9B7MBGwLVr6lQ8xSms8LQgc2LuCNc1NviYk2LawFj+Z/+w5Uv3sEVGmAvo8RV+ybTodVqmkgDkw4ZyXxMFSf310zgOmm3XYItR/cEaDRPsDRvj6rh8KiVEWCa7vkmAUtRKQQrqK7eQLPjvEt6UIzFBxecLmogo02Fn6LLtVMpdvg6FXnvVuVYlu+ZRbKqZUAW4OwU= spamdiagnosticoutput: 1:99 spamdiagnosticmetadata: NSPM Content-Type: text/plain; charset="UTF-8" Content-ID: <817DA4C3F5DBB54394A0A17F0E7F77AC@eurprd06.prod.outlook.com> Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: bc40c93a-d6c3-4316-fbd8-08d644ba232c X-MS-Exchange-CrossTenant-originalarrivaltime: 07 Nov 2018 14:05:56.2819 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-Transport-CrossTenantHeadersStamped: VI1PR06MB5486 X-OriginatorOrg: exmail.nottingham.ac.uk X-SASI-RCODE: 200 X-Original-Sender: thorsten.altenkirch@nottingham.ac.uk X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.124 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk 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: , Something that only satisfies the axioms of a category but whose homs are n= ot sets I would call a "wild category". So yes a category needs to have homsets otherwise you have to give it a num= ber. And -1-categories already have a name they are called preorders.=20 I think the interesting notion for HoTT are categories whose Homs are types= and which fullfill all the coherence conditions, i.e. they correspond to (= \infty,1)-categories. Nicolai and Paolo gave a definition of univalent (\in= fty,1)-cats in 2-level HoTT as "complete Segal types". From this one can as= lo derive non-univalent (\inft,1)-cats but in this case it is easier to def= ine the univalent version because then you don't have to deal with degenera= cies. Thorsten =EF=BB=BFOn 07/11/2018, 13:53, "homotopytypetheory@googlegroups.com on beha= lf of Thomas Streicher" wrote: 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. =20 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. =20 But then univalent categories are not categories but just precategories= . Why not call the general notion "\infty-category" as usual? =20 Thomas =20 --=20 You received this message because you are subscribed to the Google Grou= ps "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. =20 This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment.=20 Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored=20 where permitted by law. --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.