From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCIPFMNR2IEBBA67RPPQKGQENJ2EAEI@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.8 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-wr1-x43d.google.com (mail-wr1-x43d.google.com [IPv6:2a00:1450:4864:20::43d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id ce4d458d for ; Wed, 7 Nov 2018 13:58:28 +0000 (UTC) Received: by mail-wr1-x43d.google.com with SMTP id v2-v6sf15556459wrn.0 for ; Wed, 07 Nov 2018 05:58:28 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541599107; cv=pass; d=google.com; s=arc-20160816; b=tOGZ9shoAjWI6uYeCvoGjTrDsJ7w94IpQWanUIb0K97lJF0kXjmycZhLblEthpopL8 c7CZzUTT9W5hufjSAGcPGCsYsxktaGGk6JT1dfc23VSdXKbPzDHqpeUQwh05HTqcBHSU 4sIl7x7rgA3WPyqHSLb79e4w/N1LsP3zOWDGU7SI7nQHmM/QkqMIhUXrTKRGvRyvHWSS p2Lpl2sYunEEvQSN1T39JqYU28T6p605fnYJS4OZ1tCL7+mRtHU3srl9fG8siWJkHEw2 nV3KHHC3XM9Wq/qSAXfdZrQIA/d+cT+7Vtrv69FvH7CXKFmmYabdecHArK/gxCSmguh9 sW0g== 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:spamdiagnosticmetadata :spamdiagnosticoutput:user-agent:content-language:accept-language :in-reply-to:references:message-id:date:thread-index:thread-topic :subject:to:from:sender:dkim-signature; bh=VINc+Pg9WzvjCvPSkpQyuLj1WGMEou++fPMdMLmKB0Q=; b=gQZmZ41ukLkxRIvyLVgmc8ZWxq1MKNk3y9ragzO3UZC0lf00UbtcM9NmCKhNy7xZ3u 4LYAS6KDa2g090wgu4rO1t+FlReVyrqqAUNsFYlgzLcxZv2UZ629dqfThROnS01zcbRY ziY4Y4Xdrbp/EqDsONuc1phnNx3cTh4EC8+ogO6Xr1iWa+rsJQ7tBDLDrGbd10DPaY/7 vmlRPYRQaPQVEv6msyhRkUkevEulCciaN4ULa8VcrYdL7Szua4hgbAKTz5FKVr0T2M6a xPwn18Y64LYcJOnoILF5ehC/uwTY5uHxni40LmPYISZT2n8cvVi20CV7GD4TMKhdMXjn RYDQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.129 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:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language:user-agent :spamdiagnosticoutput:spamdiagnosticmetadata:mime-version :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=VINc+Pg9WzvjCvPSkpQyuLj1WGMEou++fPMdMLmKB0Q=; b=bwfI/54mWhbse/ylWuhba6c4cZOr/baF6iqwJ+0lKxM6nTP1eS0RXFrHYK8WxrbeQL r9gYNhmZ4sCQiFH8xliU3V9JKyTh8rbvuIlLLZ6cRZjT+5RkPL7mfuZr8Pf9kVVmaERZ D5Lu5O/pFiCr/OCy/o9UV9CeF5r79L7Ek57cay+DFdzK8IEh0S/oxlRf/zxUJvVm0j2g 2jclLrgmZdm6LxVJcx0Zfn2MpQPRnvGXJIOqERqmXudnPFiOH/zgPebJ+nOHRJL/H6+s bt+puvX7GMJhPryGz8EOd+KbCSb9ZZJEYGKQijBTkSru5HYm0doF5UOob0cuquWUIoCO olng== 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:subject:thread-topic:thread-index :date:message-id:references:in-reply-to:accept-language :content-language:user-agent:spamdiagnosticoutput :spamdiagnosticmetadata: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=VINc+Pg9WzvjCvPSkpQyuLj1WGMEou++fPMdMLmKB0Q=; b=o3w8PCmEDoFaMH8jWcArhoOun/FfwldXRg+EuplONZoeGVJcKY8quSbZ8c88Tqg4se zg4jU3y2NEpDeu7AKcnAFvA2C50ZhCWJ4ol5gt0xZ9do6Erw9r1BkcCO4an2hVGt4gbK +ErlwVOEu5JmY0tjaPt8Q8kjcOrdm3VB0YyZmcHZyT/nG0j4Om5N7FiR0APyXxYDy1fW MpGNXb9t0bGbjFjSXCxw2yYVK5Qtlbxx5kfWtNArfwI7iYcRLZXRh76TA1kO0k8ex85j q5FtNy+xgZTotmNa6ocGwns/roPe0tts4h0yswdfJHwtrsyHpFnKNCZX6uP3bdvC/hfa zPbA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gJ+g7btIfS39luMhQY2zWcNHeQWwI8Ii2S37zLKXsda+uaohG57 g/UIv/WvjjsEFIFbTU0HXZs= X-Google-Smtp-Source: AJdET5fVSwz527gmq7SQmagtDVVWpNuABCRriUwa7BXGJenoZMRZ/tUHIv4+ygZL1Cr0qSPfJS3gDA== X-Received: by 2002:a1c:acc5:: with SMTP id v188-v6mr974wme.2.1541599107542; Wed, 07 Nov 2018 05:58:27 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:834f:: with SMTP id f76-v6ls2384499wmd.22.canary-gmail; Wed, 07 Nov 2018 05:58:26 -0800 (PST) X-Received: by 2002:a1c:2d4b:: with SMTP id t72-v6mr66268wmt.18.1541599106937; Wed, 07 Nov 2018 05:58:26 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541599106; cv=none; d=google.com; s=arc-20160816; b=MvcDeYtRIlBc5v1ZmaT73sXDRELXktokfRCs8W3bSww2buxwAKdW1ZkDI9Vkkd9ZtQ si563MnUc5B84RiFA2oKfWOnp86R0KjIxqDqJaGtUDghRvMEqeOFp/9n45opfl0ccYLO jZ1AdfxWo7tEkPuCdeSJOXO47ZAK3liGJO+Ew3sUaOCruAvAunMGl64AyWumx/JNWkka dEe/4zGY50zcYVZ8YxBE3YzA7pE30R+DhEts3P2ONkcZWimmb6gKM3+cByIP0TaPuduT oBOIBNEhpWXU16puhLcF84YQRBORo6+8A5TzLTMjoMxgo4s7adZOyoNEQPf334GQToXD KaQw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:spamdiagnosticmetadata:spamdiagnosticoutput:user-agent :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:to:from; bh=owVOvJrTTjVfTfnWI99rD2/EmNWoLp5hTBpfhLwdFT8=; b=nS3iuZCJ8klduIlRV51XdFO3istB4Iju+mIK59Dkg3OYGSawlC0E9CidKsYjRVReou Vzu/5H6XCaFXSbnX24Fivd9DWnilhWPlRmtjMuwvbi40P/Xein5VRL21zkgPoG0QyY+F bTmprPxjKlDVH3rwaUDad8xpkqL0HGGnTh2DyLTUpBQsc1sCgiRfBX3bRPsVQZb9Bh2L zENLGl9vDAQGh0vjEWzrt03vWj8kihqSDRJFw+TjJCIfPR9YYGwqDjdrusNnkZ2SBL3w 3MnuoTBXalStzdLw5EArTdKyPtjBcLgOwbv+8rqkIjpyWHfbCzt4K8QT5UY9OoMtF2fv 7hXg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.129 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk Received: from uidappmx06.nottingham.ac.uk (uidappmx06.nottingham.ac.uk. [128.243.43.129]) by gmr-mx.google.com with ESMTP id v6-v6si31036wrn.0.2018.11.07.05.58.26 for ; Wed, 07 Nov 2018 05:58:26 -0800 (PST) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.129 as permitted sender) client-ip=128.243.43.129; Received: from uidappmx06.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id C2ECE2B7B89_BE2EF82B; Wed, 7 Nov 2018 13:58:26 +0000 (GMT) Received: from smtp3.nottingham.ac.uk (smtp3.nottingham.ac.uk [128.243.44.55]) by uidappmx06.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id 36D8C2DDD19_BE2EF82F; Wed, 7 Nov 2018 13:58:26 +0000 (GMT) Received: from [10.159.172.14] (helo=UiWexEDG02.ad.nottingham.ac.uk) by smtp3.nottingham.ac.uk with esmtps (TLSv1.2:AES128-SHA256:128) (Exim 4.85) (envelope-from ) id 1gKOLi-00028C-5T; Wed, 07 Nov 2018 13:58:26 +0000 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) 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 13:58:26 +0000 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) 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 13:58:25 +0000 Received: from UiWexEDG01.ad.nottingham.ac.uk (10.159.172.13) by UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) 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 13:58:25 +0000 Received: from EUR02-VE1-obe.outbound.protection.outlook.com (128.243.226.54) 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 13:58:25 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB4944.eurprd06.prod.outlook.com (20.177.203.96) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1294.26; Wed, 7 Nov 2018 13:58:24 +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 13:58:24 +0000 From: Thorsten Altenkirch To: Ulrik Buchholtz , Homotopy Type Theory Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories Thread-Topic: [HoTT] Re: Precategories, Categories and Univalent categories Thread-Index: AQHUdoWaEWRL1VfTr0qqVzzaadLFAqVEJ8sAgAAJYQCAACWsAA== Date: Wed, 7 Nov 2018 13:58:23 +0000 Message-ID: References: <3c553ba0-2181-44ec-b790-969a8115ea1f@googlegroups.com> <1a3288ec-ca0e-48ce-80ad-9cad01f56845@googlegroups.com> In-Reply-To: <1a3288ec-ca0e-48ce-80ad-9cad01f56845@googlegroups.com> 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;VI1PR06MB4944;6:ErOpuhW0UGzMIZ/DbpiXf0KaRPimaQa1WY6I3l1seFNzoo8O6onmuLnckUX9++JUNz8tVGHpCVUxdnKMuiQOHs3ZL3T9+o7dLLIozjC3ih1UOhQ9vAeD+4T9AUmy1511U0fESlh/zHuwBF/KOyfFxD4mGT8oTLnkMwnDD+t5s7cEqU0VJ8BhiwIgPzn5BVuCqsJVBDP0CNzY2qSGYqlmrLecZf4G25L6TqOevhsENYNxo9Gi8ATz+nnHG1F6khybGdwg3t7e9aVTwqYRpRW1dVvD+hu9UQd+NoRAGoU3BmmVZAG43doOVsS21CQVpMsbUmBnpHKKRRHjFXKz+gK7jSOmjjLNE9nPnjvZN6uo9V4KkcrCoCW0v6v+aTgCMatnoQyQqIGxtfQFQn2+XfN6skve/8Zko51a+/d/z2YTZ89NN8jSRZZTd6pTjGfcO1ABym+xOaYUFQBdKe8P+xEhxw==;5:61WqHFwGGpD80I08w4ig5c7vAO7tebRjsT5c/PycVsrSBecYtRXjxJZ6yg6xi8l0l+YJMvM4G89wxAv9T+siTFKxa5RK2ogSd1Nivcdjz/vKpXxba6iQBwfS9AZ9thYvpNoBWMRKSoiuWgOU2834PADDh5vOZ1Bt6KFQuXNYn/0=;7:xXQUc8FaxCILzVApCrK2QU6K9Fn4XHUEA9pL5voTeLEQOib2HbwwB36vokdRGKBS2fXK57Enl7kTQfocH/3ahoc/dnjJXj2wSag4TGgGX7GuVqyTygtSRQzAXqQP8Ju9w82Yvesaf96+f2FRd/8cXw== x-ms-exchange-antispam-srfa-diagnostics: SOS; x-ms-office365-filtering-correlation-id: 8ca2b2f2-9e3b-4cb0-6e3d-08d644b91583 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(7020095)(4652040)(8989299)(5600074)(711020)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(2017052603328)(7153060)(7193020);SRVR:VI1PR06MB4944; x-ms-traffictypediagnostic: VI1PR06MB4944: x-microsoft-antispam-prvs: x-exchange-antispam-report-test: UriScan:(163750095850)(215639381216008)(85827821059158)(228788266533470)(211936372134217)(21748063052155)(28532068793085)(190501279198761)(227612066756510); x-ms-exchange-senderadcheck: 1 x-exchange-antispam-report-cfa-test: BCL:0;PCL:0;RULEID:(6040522)(2401047)(8121501046)(5005006)(3231382)(944501410)(52105095)(3002001)(10201501046)(93006095)(93001095)(148016)(149066)(150057)(6041310)(20161123564045)(201703131423095)(201702281529075)(201702281528075)(20161123555045)(201703061421075)(201703061406153)(20161123558120)(20161123562045)(20161123560045)(201708071742011)(7699051)(76991095);SRVR:VI1PR06MB4944;BCL:0;PCL:0;RULEID:;SRVR:VI1PR06MB4944; x-forefront-prvs: 08497C3D99 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(39860400002)(346002)(396003)(366004)(376002)(136003)(199004)(189003)(11346002)(68736007)(2616005)(3846002)(6116002)(476003)(81156014)(83716004)(81166006)(966005)(229853002)(486006)(14454004)(7736002)(8676002)(97736004)(86362001)(76176011)(99286004)(5660300001)(102836004)(105586002)(26005)(8936002)(74482002)(106356001)(446003)(39060400002)(2900100001)(6486002)(6506007)(53546011)(6246003)(93886005)(606006)(53936002)(33656002)(316002)(25786009)(58126008)(110136005)(66066001)(6512007)(2906002)(82746002)(6436002)(786003)(54896002)(478600001)(6306002)(66574009)(256004)(71200400001)(14444005)(71190400001)(186003)(236005)(42522002)(42262002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB4944;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: um1CQUsUHjZFaIMA/o5PzZjDec5rZmbyLHtTi1X/GDQF25Dl0HOaciF7w6qtdVQRRpbRet9ubg097LHT/lTKNHMVSQdwafxbnZaxGVGBgXPh2FS1JmvsxoIDJoOhDKcJTceRDcMIxcjg/yY35e0C1v23tr4LYvAK7jj9EnsuXVbGRwHxkGT3L8bHEfTvsjmGkEFt/yXuYwqyULjb/lezPxMQveh1Ub8tpgClJPiu3p4H413PF9Ol7LdioUqCZWUnz6sONOonkOWGYBxlbTVeFsS6cuw3RbITxrqSrtxhkGk4lQPcoiJ4UDnVEGxe8BedgWGDfZAL4Ip/ugktEnokzURbi3JY1B+b1POj/rTuowA= spamdiagnosticoutput: 1:99 spamdiagnosticmetadata: NSPM Content-Type: multipart/alternative; boundary="_000_A1F48786B8E34D79896796D507C7F0CEexmailnottinghamacuk_" MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 8ca2b2f2-9e3b-4cb0-6e3d-08d644b91583 X-MS-Exchange-CrossTenant-originalarrivaltime: 07 Nov 2018 13:58:23.8686 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-Transport-CrossTenantHeadersStamped: VI1PR06MB4944 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.129 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: , --_000_A1F48786B8E34D79896796D507C7F0CEexmailnottinghamacuk_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I'm a bit confused by your message, Peter: HoTT doesn't have a naive set in= terpretation and is inconsistent with UIP, so I'm not sure how that should = guide us. (Maybe if we're working in good old (agnostic?) MLTT?) As I tried to say, I find that precategory is the novel concept, and that b= oth strict category and univalent category should be familiar to category t= heorists. (They have a mental model for when one notion is called for or th= e other, but we can make the distinction formal.) This is too clever! If you just transcribe the traditional definition of a category in type the= ory you end up with what in the HoTT book is called precategory. This is co= nfusing for the non-expert even though you can justify why it should be so. Hence I think the terminology category / univalent category is preferable. = This also maintains the traditional wisdom that categories (with trivial ie= .e propositional homsets) correspond to preorders. We may add that univalen= t categories correspond to partial orders. And yes indeed there is something wrong with preorders because they have eq= uality and equivalence and hence it is better to have a preorder. The same = holds for categories, you have both equality and isomorphism and hence it i= s better to have a univalent category. Thorsten From: on behalf of Ulrik Buchholtz Date: Wednesday, 7 November 2018 at 11:44 To: Homotopy Type Theory Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories On Wednesday, November 7, 2018 at 12:10:10 PM UTC+1, Peter LeFanu Lumsdaine= wrote: Ulrik=E2=80=99s email nicely lays out the three key notions (pre-category, = strict category, univalent category), and the argument for the Ahrens=E2=80= =93Kapulkin=E2=80=93Shulman / HoTT book terminology, with =E2=80=9Ccategory= =E2=80=9D meaning =E2=80=9Cunivalent category=E2=80=9D by default. For my part I lean the other way: I think it=E2=80=99s too radical to use = =E2=80=9Ccategory=E2=80=9D for a definition which doesn=E2=80=99t come out = equivalent to the traditional definition under the na=C3=AFve set interpret= ation (or under the addition of UIP to the type theory). Choosing terminol= ogy that actively clashes with traditional terminology makes it much harder= to compare statements in HoTT with their classical analogues, and see what= difference HoTT really makes to the development of topics. Based on that criterion, I strongly prefer taking category to mean =E2=80= =9Cprecategory=E2=80=9D. A big payoff from this is that if you formalise s= omething using =E2=80=9Ccategory =E2=80=9D to mean =E2=80=9Cprecategory=E2= =80=9D in type theory without assuming UA, then you can read the result eit= her as valid in HoTT, or (under the set-interpretation) as ordinary argumen= ts in classical category theory, with all the terms meaning just what they = traditionally would. Univalence of categories is an important and powerful property, but not an = innocuous one; it changes the character of the resulting =E2=80=9Ccategory = theory=E2=80=9D in interesting ways. Making the restriction to univalent c= ategories tacit is misleading to readers who aren=E2=80=99t fully =E2=80=9C= insiders=E2=80=9D, and obscures understanding its effects. =E2=80=93p. -- 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. 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. --_000_A1F48786B8E34D79896796D507C7F0CEexmailnottinghamacuk_ Content-Type: text/html; charset="UTF-8" Content-ID: <686DC70A2E01DD489625A9E5FDFEF256@eurprd06.prod.outlook.com> Content-Transfer-Encoding: quoted-printable

I'm a bit confused by y= our message, Peter: HoTT doesn't have a naive set interpretation and is inc= onsistent with UIP, so I'm not sure how that should guide us. (Maybe if we'= re working in good old (agnostic?) MLTT?)

 

As I tried to say, I fi= nd that precategory is the novel concept, and that both strict category and= univalent category should be familiar to category theorists. (They have a = mental model for when one notion is called for or the other, but we can make the distinction formal.)


This is too clever!

&nbs= p;

If you ju= st transcribe the traditional definition of a category in type theory you e= nd up with what in the HoTT book is called precategory. This is confusing f= or the non-expert even though you can justify why it should be so.

&nbs= p;

Hence I t= hink the terminology category / univalent category is preferable. This also= maintains the traditional wisdom that categories (with trivial ie.e propos= itional homsets) correspond to preorders. We may add that univalent categories correspond to partial orders.

&nbs= p;

And yes i= ndeed there is something wrong with preorders because they have equality an= d equivalence and hence it is better to have a preorder. The same holds for= categories, you have both equality and isomorphism and hence it is better to have a univalent category.<= /o:p>

&nbs= p;

Thorsten<= o:p>

&nbs= p;

&nbs= p;

From= : <homotopytypet= heory@googlegroups.com> on behalf of Ulrik Buchholtz <ulrikbuchholtz@= gmail.com>
Date: Wednesday, 7 November 2018 at 11:44
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>=
Subject: Re: [HoTT] Re: Precategories, Categories and Univalent cate= gories

 

On Wednesday, November= 7, 2018 at 12:10:10 PM UTC+1, Peter LeFanu Lumsdaine wrote:

Ulrik= =E2=80=99s email nicely lays out the three key notions (pre-category, stric= t category, univalent category), and the argument for the Ahrens=E2=80=93Ka= pulkin=E2=80=93Shulman / HoTT book terminology, with =E2=80=9Ccategory=E2= =80=9D meaning =E2=80=9Cunivalent category=E2=80=9D by default.

=  

For m= y part I lean the other way: I think it=E2=80=99s too radical to use =E2=80= =9Ccategory=E2=80=9D for a definition which doesn=E2=80=99t come out equiva= lent to the traditional definition under the na=C3=AFve set interpretation (or under the addition of UIP to the type theory).  Choosing terminol= ogy that actively clashes with traditional terminology makes it much harder= to compare statements in HoTT with their classical analogues, and see what= difference HoTT really makes to the development of topics.

=  

Based= on that criterion, I strongly prefer taking category to mean =E2=80=9Cprec= ategory=E2=80=9D.  A big payoff from this is that if you formalise som= ething using =E2=80=9Ccategory =E2=80=9D to mean =E2=80=9Cprecategory=E2=80= =9D in type theory without assuming UA, then you can read the result either as valid in HoTT,= or (under the set-interpretation) as ordinary arguments in classical categ= ory theory, with all the terms meaning just what they traditionally would.<= o:p>

=  

Univa= lence of categories is an important and powerful property, but not an innoc= uous one; it changes the character of the resulting =E2=80=9Ccategory theor= y=E2=80=9D in interesting ways.  Making the restriction to univalent categories tacit is misleading to readers who aren=E2=80=99t = fully =E2=80=9Cinsiders=E2=80=9D, and obscures understanding its effects.

=  

=E2= =80=93p.

=  

-- You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+un= subscribe@googlegroups.com.
For more options, visit https://groups.google.com= /d/optout<= span style=3D"mso-bookmark:_MailOriginalBody">.


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.

--
You received this message because you are subscribed to the Google Groups &= quot;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 http= s://groups.google.com/d/optout.
--_000_A1F48786B8E34D79896796D507C7F0CEexmailnottinghamacuk_--