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-lj1-x237.google.com (mail-lj1-x237.google.com [IPv6:2a00:1450:4864:20::237]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id bf58180b for ; Thu, 8 Nov 2018 16:02:02 +0000 (UTC) Received: by mail-lj1-x237.google.com with SMTP id j5-v6sf1789493ljg.1 for ; Thu, 08 Nov 2018 08:02:02 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541692921; cv=pass; d=google.com; s=arc-20160816; b=zPCG75L7ZNIxQbXc9AhDNrfWkHF+Za7T3cjgmQexB+3PgyKCdHc7KSNibSYDnKD+Du EreJaef/VCvucD1Y4gKOrxt6fJCzLKB/qD4mQXV3kakxkeesjVVN+1goheW2no3aAYG6 pS6NAD5CuH91Jgw1wUeI7M8zdp/L+U3YrHQvDQyPZaoNOLHGIxa28dA8ap8P3BG1oc0j 19TwfxJgsHx/8P5vXkKkNXDLILLwhVpbh0x+nvkg1d4GuqxlJ/eZDJ4Q0ynbvOkvR0e0 GGbD0ocqpjoog1RBc5DiUA0WAogfgZE49PIrZxDRfl65PWFUFZtkkgQUmDGSK3E3bDfo Tbaw== 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-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=Lt+b5NsPhcw7dWT5XBKC4t4jsKSLWz0z4CVnaMxKrKU=; b=xUmIjIvVDxMTwPVKwL4/c/rTtP2J/cz+p/I4F/RETBwoes8RsmXFRJEXnqRCAm1Xzg ZCMxvxOyJXtYAnksFw5cUvW98IcJS7vZ7hqfDX7xEoVFBstwj5hJtIH9Tw9x9/W1Fsn9 FnyAPb7MqaVNHm+TgABOFsfIapuhHxjv/v95Jguh+T/Ik6FPuxBHxhVBqIK4XplGdjJy HwyagbOeZ3nNviIS29lI/EJ72OvaSWE55ASpKFVQrht4f/d0i6Auej5dnjx7MenGs/ST EA/7tJiYRj4g1YWDLzSkcBssPbFWVWwi1VF4j1DZi2t/wRtuqn4FG+v6JM9RsQg5QyaJ g0xg== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 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:mime-version :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=Lt+b5NsPhcw7dWT5XBKC4t4jsKSLWz0z4CVnaMxKrKU=; b=i9BX6QW4DSDyut5+aoTKCDnIxxI/wvNIqV6QD7S6PmOn+xH2QllkMbGkvMakq5oHBB XhRHaz7Gvm/pLr6s3RNNPkZGfBB+2fLEJn7xhnpDKouoZPBBWGwekNDS2p2ThlOGArj6 MDm74QhOF8o6D8B+cNuX23nBliGZ2nnozVdbTftNAwTj4a9rcZYp/+s91+nO8bMTAPHw qx/H9mD5ESqFix08aqcnsr/tCwwydAwuYim7B9ti7bGpjkB1/xkCAR5pp4Fif9FoHVGG WLO72926H5CLHfHbCxDVUcpW7EySRKVE5Qn2Ny9VWfrVwhoGZAXPLfTTqtgqinO+iLJS xUbQ== 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: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=Lt+b5NsPhcw7dWT5XBKC4t4jsKSLWz0z4CVnaMxKrKU=; b=AFIX/1Y04ByT0Zrxb3xGRecpd4qc++GjKK9JXwRu42kaU83tvcFxwtSJo+eNHWH5Bs V7yPSU9/cZPtxdlgBXIBw9b5sMuaYDMaacNYA5fj/80jYUmQykzoA6hJJQfg1xOllWnt HMfXyHAjaMB0oXQUDhQB+u+7lP8bRyO7PCSi8B+3f644O6pGlHEMgBKD7nSe0RgJIBqe x5catFrUS9Nl4GfsTB/1gXFTirclc2pfj1PUCm+uAR6NIBqBhLOAV4OZyi1xBZNDd/P7 x5P6edBk6JnOzKHs18gmDqCuVdsKIflddzyd1T0VXOQwGVLO+f0cqM0y5sZvjdnamnTw 1EyQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gK+VJfGgPpOwjQulWjpRc9nkN17ftq8fFTw2fYcyvqtwVsX5vtJ Vb7JmDQaQd3WzFPAZhO+8sU= X-Google-Smtp-Source: AJdET5dXy/fJFfPbmaafokIolekiFKPSD0P/IV276KF6Lr0uJQNkej8STyDLiLYDZpe5J5S75BIRfw== X-Received: by 2002:a2e:93c5:: with SMTP id p5-v6mr25161ljh.7.1541692921597; Thu, 08 Nov 2018 08:02:01 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a19:3804:: with SMTP id f4-v6ls180617lfa.7.gmail; Thu, 08 Nov 2018 08:02:00 -0800 (PST) X-Received: by 2002:ac2:410b:: with SMTP id b11-v6mr509560lfi.11.1541692920695; Thu, 08 Nov 2018 08:02:00 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541692920; cv=none; d=google.com; s=arc-20160816; b=n6mZnmZUq3HDUvzHGPoi6OARK++LuS9BMUccpIjMmvVYtK1epUpqfEL9i7AZHJ6rHx RclDXK2/VkQpLjTc50UX0Fg/bwGuxyaQjN07HCEw41xCfqZA/xKjGxljCqftqkLn+Bno TMq8+HC3K5K1wvKF6xRl4HE+H9aIeYvFLdFV6IaUwacpEXWDXMMBLCTgGGOvtzzFWTu8 55N9pV5vWwqlwgfNMLjk3u3R9+F70+FASth3PIKXfjfXEpz3fY7nXAwshyoHfvpsaLKe wH5sTYQo8ukfUrS8GjOZoUJxLdF5+Mj9CX0QkhzdURAKdTrLT1Ulem5pBeBNiPSB0z8h B+aQ== 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=/z4ThyInsUHa67wtHyfZI1y3Anpkm5ZOKBZIzoAXLtE=; b=Xx7/UjiDfXjvFqIpYJSIWafEytk2MzXjyujACgr5Jn66XhLjULDcv73dapsUiJSvGr zLzbLJKFNY8UyK+xsqB3s+pHXZwZKOVq/4zNy30S7uLykq+jf7TNXdQ6KHZO2uK6kEpN CfPiKX7R+k3zSOvpt+0qpCMlqpHBbPMS3HnQTki8cLFToa8HjCRjDBIbo8vE62YTHSA7 1KDufhguqg1jYKlmk5S67ZswBQQv/wuUM8iZFcHqeHncie3FK4dpyET2niaDa2PGEsem NTg60p5jHgOW4yxLjnYqj6GDsWo8P9flfq7YpcQa/eb1CU5/2A6sovq/eEGKs9c/8Ggm 58Kw== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk Received: from uidappmx05.nottingham.ac.uk (uidappmx05.nottingham.ac.uk. [128.243.43.128]) by gmr-mx.google.com with ESMTP id y12-v6si137563lfh.4.2018.11.08.08.02.00 for ; Thu, 08 Nov 2018 08:02:00 -0800 (PST) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 as permitted sender) client-ip=128.243.43.128; Received: from uidappmx05.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id B32AC6D129D_BE45DF7B for ; Thu, 8 Nov 2018 16:01:59 +0000 (GMT) Received: from smtp4.nottingham.ac.uk (smtp4.nottingham.ac.uk [128.243.220.65]) by uidappmx05.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id C3F8E723636_BE45DF6F for ; Thu, 8 Nov 2018 16:01:58 +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 1gKmko-0006CA-1w; Thu, 08 Nov 2018 16:01:58 +0000 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) 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; Thu, 8 Nov 2018 16:01:58 +0000 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.1531.3; Thu, 8 Nov 2018 16:01: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; Thu, 8 Nov 2018 16:01:58 +0000 Received: from EUR01-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; Thu, 8 Nov 2018 16:01:56 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB5359.eurprd06.prod.outlook.com (20.178.15.97) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1294.26; Thu, 8 Nov 2018 16:01:54 +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; Thu, 8 Nov 2018 16:01:54 +0000 From: Thorsten Altenkirch To: Thomas Streicher CC: 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: AQHUdoWaEWRL1VfTr0qqVzzaadLFAqVEJ8sAgAAJYQCAACergIAABn8AgAASxQCAABXOgIABP7SAgABD9oA= Date: Thu, 8 Nov 2018 16:01:53 +0000 Message-ID: References: <3c553ba0-2181-44ec-b790-969a8115ea1f@googlegroups.com> <1a3288ec-ca0e-48ce-80ad-9cad01f56845@googlegroups.com> <4ae4c745-a00e-4ebd-9de2-e29474b75d48@googlegroups.com> <20181107153556.GC26970@mathematik.tu-darmstadt.de> <20181108115815.GA5022@mathematik.tu-darmstadt.de> In-Reply-To: <20181108115815.GA5022@mathematik.tu-darmstadt.de> Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/14.5.7.151005 x-originating-ip: [128.243.2.16] x-ms-publictraffictype: Email x-microsoft-exchange-diagnostics: 1;VI1PR06MB5359;6:MWQqj+upyQUhU4ldpzGWW/hPwi+cLYrQcDT6gWjTZ4359w3SafbsylMylBvu44i4vcvf0Dr8ShJ/ZLcxQRrai2YDGeFXhQO32uJBI0Pz4WrTa8uT0X1XkxhqriQs8JZbVlfZbRpzFH1gVDtuDPekQKDEjpLnGokccP8f99XLhkAWvoWn3+4Co4o7LdI3OqwTa+zMleY1yZ8UmZdUReLme0Y9JFzspkd4397qU2coxgVVirPKfPNWFVP+OokV4kdyyrm7I1S/eO9W3Jaui545siuyoLr3Lk88dnGm5eCwvRtwYZtG6QBjDfuOj01O+CLrx0xE3Lw43NDtqgCF98PXEeHXELuW0wRrgCPeCiOj7thCleY/uUgIgXpU1Q1IQYSO3bn2COFRNZB2IPHYH+6z5e26KmBoiTCrcOn3d6vsXRQDvuIMZVk1HiJsXh9FnBxqhXmpSf9tqBT6NlWA0mqkXA==;5:zpSXZaAWzhldRlHtkhY4BrXFKiDkbEfLf/6bkw8bWCG+WfsNl8kvIqiQVqBkl3go+2VTRobChtdFGM81ZotAjqZpBPeBzy9rHbIhXdy5QmM5iVOVy4y4a8Kt1fBMdKHKaFbw5lW5Wr9Q1krINX+HYtpxbYDv0J7YEGxDiIE1vAo=;7:FsnsCenrZGDOEyiA9H7WlCY/e/7xAcqyFv9jGfNrdc3xdCwLGpRFl9KNja7uiAtZi0Ca9dzI//9p/y9nb1h47jbcloY9dBxrkMLifmWhR1id7FP3lEuUObM3Vj3U00do9UsDr16GmzSxNpiuJqFmxw== x-ms-exchange-antispam-srfa-diagnostics: SOS; x-ms-office365-filtering-correlation-id: 67131e16-dd3e-426e-3c13-08d6459380b1 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(7020095)(4652040)(8989299)(5600074)(711020)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(2017052603328)(7153060)(7193020);SRVR:VI1PR06MB5359; x-ms-traffictypediagnostic: VI1PR06MB5359: x-microsoft-antispam-prvs: x-exchange-antispam-report-test: UriScan:(76576733993138)(165104125076784); x-ms-exchange-senderadcheck: 1 x-exchange-antispam-report-cfa-test: BCL:0;PCL:0;RULEID:(6040522)(2401047)(5005006)(8121501046)(10201501046)(3002001)(93006095)(93001095)(3231382)(944501410)(4982022)(52105095)(148016)(149066)(150057)(6041310)(201703131423095)(201702281529075)(201702281528075)(20161123555045)(201703061421075)(201703061406153)(20161123558120)(20161123560045)(20161123562045)(20161123564045)(201708071742011)(7699051)(76991095);SRVR:VI1PR06MB5359;BCL:0;PCL:0;RULEID:;SRVR:VI1PR06MB5359; x-forefront-prvs: 0850800A29 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(346002)(136003)(376002)(39860400002)(366004)(396003)(189003)(199004)(54906003)(86362001)(2906002)(8936002)(81166006)(81156014)(74482002)(8676002)(229853002)(966005)(186003)(93886005)(2616005)(476003)(486006)(11346002)(478600001)(14454004)(4326008)(316002)(71200400001)(3846002)(446003)(256004)(6116002)(25786009)(58126008)(71190400001)(786003)(2900100001)(68736007)(106356001)(66066001)(99286004)(6916009)(39060400002)(102836004)(26005)(53936002)(5660300001)(76176011)(6506007)(6512007)(6306002)(97736004)(6486002)(6246003)(7736002)(305945005)(6436002)(105586002)(53546011)(42522002)(42262002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB5359;H:VI1PR06MB4029.eurprd06.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;MX:1;A:1; received-spf: None (protection.outlook.com: exmail.nottingham.ac.uk does not designate permitted sender hosts) x-microsoft-antispam-message-info: tigG9+7MkCYmaaJGiK6pogV94fjSy/3pXv712GGDWCVz+tXNlxZ20Hb+PdRKfuCjzZCbH7+CuXRVeYbmiXYBOGD1EfBa/tyaaGBZ1V6HZGsvmqDed8dYcEiZp63TmjIaolHdoApigurAobwu8+fH37SPRi9fSUrcsbqO8SmXnJL7cXPxlgFewHJ0IynadkxjL1ZKa4rzoXHQki58XHJf2/Fflbr0V+tgRkQQidpyXVoZ4eo9Sm7IDUEfnDtPtLDP0hgzZjpo8rBBvXPDY+VQ4eBKLbvLED16i971cvzfb3QUneM81y1X/MMWLvEPcUFsKXX7FplYJVEc53v5hOKWyG7xq7JpllhaKWLGZ+vzhks= spamdiagnosticoutput: 1:99 spamdiagnosticmetadata: NSPM Content-Type: text/plain; charset="UTF-8" Content-ID: <48E7467BA00AB1499ACF619BE8A92B83@eurprd06.prod.outlook.com> MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 67131e16-dd3e-426e-3c13-08d6459380b1 X-MS-Exchange-CrossTenant-originalarrivaltime: 08 Nov 2018 16:01:53.9760 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-Transport-CrossTenantHeadersStamped: VI1PR06MB5359 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.128 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: , Hi Thomas, two answers: the first is that in this particular case one doesn't need strict equality because one can present this as an indexed structure in type theory, e.g. assume as given a category C then a fibration F is a structure with the following components (here I assume that the base cat C is given by objects |C|, morphisms C(_,_) and so on. |F| : |C| -> U Fm : C(x,y) -> |F|(x) -> |F|(y) -> U id_F : Fm id a a comp_F : Fm f b c -> Fm g a b -> Fm (f o g) a c coe : C(x,y) -> |F|(y) -> |F|(x) coh : (p : C(x,y)) -> Fm(p,coe(p,x,a),a) The 2nd answer is that this is not always possible and the most well known example are semi-simplicial types. In this case we can produce indexed structures for all finite approximations but we can't generate the approximations in a uniform way (the question is actually an open problem). However, you don't want to force your categories to be struct but you want to be able to talk about your univalent, non-strict categories from a strict metatheoretic perspective. This can be realized by a 2-level type theory as for example explained in our paper [1] http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf Cheers, Thorsten [1] @InProceedings{altenkirch_et_al:LIPIcs:2016:6561, author ={Thorsten Altenkirch and Paolo Capriotti and Nicolai Kraus}, title ={{Extending Homotopy Type Theory with Strict Equality}}, booktitle ={25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages ={21:1--21:17}, series ={Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN ={978-3-95977-022-4}, ISSN ={1868-8969}, year ={2016}, volume ={62}, editor ={Jean-Marc Talbot and Laurent Regnier}, publisher ={Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, address ={Dagstuhl, Germany}, URL ={http://drops.dagstuhl.de/opus/volltexte/2016/6561}, URN ={urn:nbn:de:0030-drops-65612}, doi ={http://dx.doi.org/10.4230/LIPIcs.CSL.2016.21}, annote ={Keywords: homotopy type theory, coherences, strict equality, homotopy type system} } On 08/11/2018, 11:58, "Thomas Streicher" wrote: >Thorsten asked why I prefer to have strict equality on categories. >The answer is that one needs it in category theory typically when >speaking about Grothendieck fibrations. >And the latter is most useful in many contexts in particular when >understanding geometric morphisms. This by the way also extends to >Grothendieck fibrations in quasicategories as in Joyal and Lurie's >accounts. > >Thomas > > 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. 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 where permitted by law. -- 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.