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-wr1-x437.google.com (mail-wr1-x437.google.com [IPv6:2a00:1450:4864:20::437]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0271f634 for ; Wed, 7 Nov 2018 16:56:40 +0000 (UTC) Received: by mail-wr1-x437.google.com with SMTP id 88-v6sf15850524wrp.21 for ; Wed, 07 Nov 2018 08:56:40 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541609800; cv=pass; d=google.com; s=arc-20160816; b=ayJh/bF3jicpNOlpRR+JMzw1CCdVGQlKgEPRNVlfui6RwA1d3pY4sufk2PrlReXGXs Utzp9KcOKGu1n+FtUD9vFacuqsVsdo2A5IK6o2ybBLMN3TfolG+TAkmD1wkJPz500r4y 8DV43izOkSr6gtKqq1yJdBtpnrRmBE1doUbwRIVu9CNNP+WIkUnMCeymFU1UOSk7AI0q VzR0XSbmxos4bTk7wyEyjICkB/f4j6mGk73Y8joG3tmKmrvgeahFDltb4vURQypNxdb5 AgLeKfnmhEsStdsNngOr8BxNahBrI6lMPCL/pVLZKrkOyyXT5Azgl9AD+SWdVZCZh/M7 0I8g== 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=3XAzgl9Nm3y1V4BxMwt6CSyq4alVNimVKYk7MoVz4vo=; b=Wpc5sAKoe7WzFNgOHjTlpVUiIkhZ9d0pY1O+Z9X5KlmunypaODB4VP6PtkMScyEp/v L4kfNAFJJcz6+3dwtG0zlEXKug6tDMgh+usP/iJmGhtMSWlbLRHgQwGEY30XBClzU9p/ JeR2dHKxkVM+1Mrm4W4b1rCKv7kgvDmOdEegCKJ/lrxhUpblKXOq2zA6/14m//w05I5l pFodNMg4jyIMfsu/xUiT1WT/fg7FGp0LU6XBeuQgWPtw6P5K+sf/Xyaj1MfTsbN1FV3R aeojURCUdxWxjUxTRVGzCsxJvO69/b4QbNpL/zMVZ561ljUeF6YOZpgKQrA6E0bmV76e ttWg== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.125 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=3XAzgl9Nm3y1V4BxMwt6CSyq4alVNimVKYk7MoVz4vo=; b=rp25Y0lgsvpcfD/VqzkCa1jCzAbcHl0IRlo1VwUfa74mnvEON5OnlifMUj3yIV0FID Cd0YHWx5QXXHt7auuGxZJSzJReKxjJHHzFpIIXBhWfBZlUJuKVAAFG1E6SuahaMd4qJC imvl96uqeKacd5M82r9IwY0hXL31SzpaX6yadWIb3j/a00WYjJvA74PKw1irJ7FmsT9E DeDw299nxsbN50qLue2EcozCVJTHUkwMZtE9k6AIOCJI902PlMbiEQ2BwSzUtxfvoKcz 5z0vWpNyQazkB1SlJ4pptjE2sJd7plC6XefDvXf4h2NCG8RwUN1XV0Wjecla4gxOTreB jNHA== 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=3XAzgl9Nm3y1V4BxMwt6CSyq4alVNimVKYk7MoVz4vo=; b=NBECBvWo5kNWAlO8AZGYg+vv7PCP9ZZYOuuDmmGCB579z1n3LoOaUIaxW7Tl0msw2Y h2d7/NvYxVxeVs+/1k9jOdN98JW83jneazjq71p6GmnI9fW5F7ZLMhJhwBOtWKGKXirt iqSkJ4lsMVdOcQvkrYAJHlTbUYHiapQLHMb3W6E1tJKcfAPRhq1nzFC70dlSCb5YmJNB rZTn/9lkAlxwRV99YpAJkFR9aKE/EsLh23MmwUucJb5mQfLs36kX7PN/W2BDqCHDMeSy hlv3jFOxXiYHLPAvrY8FcpA0II98f9OXW1rX0xCi0HfI3J2Ewv5TWhWzGUFpu+m3VEVQ exUg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gIHQUHexUwvfFvqyYLDXkN8a7grMI1mD6qvMBDpGYF5XIdyLoho DspDG4DBTqQKMUxoHBznnTg= X-Google-Smtp-Source: AJdET5d0uY+xsR5KQEawwB80we2IlPVlY+PEmiRg+/6AuV7Dq9hh1QNTFOSsIgrAuQHr5/SWF1JttQ== X-Received: by 2002:adf:f5c6:: with SMTP id k6-v6mr10917wrp.5.1541609800555; Wed, 07 Nov 2018 08:56:40 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:f008:: with SMTP id a8-v6ls2562863wmb.21.canary-gmail; Wed, 07 Nov 2018 08:56:40 -0800 (PST) X-Received: by 2002:a1c:e4a:: with SMTP id 71-v6mr237652wmo.20.1541609800013; Wed, 07 Nov 2018 08:56:40 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541609799; cv=none; d=google.com; s=arc-20160816; b=nNGRn8NboI184MYa2Xv5j3Dy4vV24wJDA91nGWDKxO+4nogqSkmpXvlvzpEEUZmCz1 KSEdwHk/YUhjH/x28Dzg0ITYtZx6XyjByHKswxubc5nX7NlxjCTSQ3vxqcqM0w+wJnGS vNkT+/edRw8MHAvccv7FrAm/ApvAAaOs3N/+cWA62OS4RQHcyawycNxAra50/rh7R99t RoiqQPRkE3q7MR6YrEMAUQGVUil3FEk6UlmM+Q2DaLZpbQHLbikJGRdzpmtFOL6YSo7F eOsE9D5vLBmkbg8uNH7vraKv4e7+W1IyjMGECoeNW7CH6pXQyYE5TbFmfZlRdXPpFU+E 4bEA== 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=csfoLa5vga2aTts/58R8AYqc379k+VJWx9YKCbAvsdI=; b=p1mF0+sgZZCmjEcwUmdGYrVkA26QlCScn68TlULgUyamdt+zjipWHNWYSiWQZyKRHp CeABMOJypSWiizOt5uhMfrWulqiuxsZDVK9Vsbf9UvN3nLd2RhoMbyR2cTgCORjJMfvy /n93YBIrlzDyYXvFRtuLHAvwyxaGVJghvX2Boecd5P0v1xCIzo2fZ+0x/E9lrAY2gpyH xMsS1jWsWzzikSmVkh3zy9DXvMBFeDhSjHz/Nd5jRt4If7TjNawwb8Rr8/c/8AgjuWwl JmkPzo+qvpsfGFLFhX0NApXsFaC+/AFTgDx3/xJqjpbLWe0prTwXJDP8ElTKd61XVqbr +2qg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.125 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk Received: from uidappmx02.nottingham.ac.uk (uidappmx02.nottingham.ac.uk. [128.243.43.125]) by gmr-mx.google.com with ESMTP id 191-v6si202600wmv.0.2018.11.07.08.56.39 for ; Wed, 07 Nov 2018 08:56:39 -0800 (PST) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.125 as permitted sender) client-ip=128.243.43.125; Received: from uidappmx02.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id AE1712EAAA9_BE31947B for ; Wed, 7 Nov 2018 16:56:39 +0000 (GMT) Received: from smtp3.nottingham.ac.uk (smtp3.nottingham.ac.uk [128.243.44.55]) by uidappmx02.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id 771812EFED5_BE31946F for ; Wed, 7 Nov 2018 16:56:38 +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 1gKR8A-0007ov-7i; Wed, 07 Nov 2018 16:56:38 +0000 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) 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 16:56:38 +0000 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.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_GCM_SHA256) id 15.1.1531.3; Wed, 7 Nov 2018 16:56:37 +0000 Received: from UiWexEDG02.ad.nottingham.ac.uk (10.159.172.14) 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 16:56:37 +0000 Received: from EUR02-VE1-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 16:56:37 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB5630.eurprd06.prod.outlook.com (20.178.121.216) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1294.32; Wed, 7 Nov 2018 16:56:36 +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 16:56:36 +0000 From: Thorsten Altenkirch To: Thomas Streicher , Ulrik Buchholtz CC: Homotopy Type Theory Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories Thread-Topic: [HoTT] Re: Precategories, Categories and Univalent categories Thread-Index: AQHUdoWaEWRL1VfTr0qqVzzaadLFAqVEJ8sAgAAJYQCAACergIAABn8AgAASxQCAABXOgIAAALqA Date: Wed, 7 Nov 2018 16:56:36 +0000 Message-ID: <25749C08-4CFC-4B16-955E-92E59EF4D180@exmail.nottingham.ac.uk> 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> In-Reply-To: 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;VI1PR06MB5630;6:4Q2v5l7M3l8tUWx0w0mPTC/bnBORSKwNiJZiOJIWnQ2xTXK8nSwSeVO/6NCD/KXTB4hFfMJnW843v/IVgl5BsnbiEz7ysn7QQ1GJ+OKCVOxLg1NHt2eZNS90sZCWnMDusvUlNNMI7dRruL4DJ/uY+bOP3eu+hk9lqDxW0GaH7U6A7wQtq5e/WYFHKUPH3AnDaPyYJY++3sRJdZ5eXctroCWT//QBW66/ffG+hAe7hwomnjCdLNycx0cmxyhyUaGvC2z15U1fOJ1GUhrywq0qq1HMEVOY+6igS/uVuwijNV8kdfbEIf01DDQwcjDwRBnNC9jbXWoRLSTtwKMAxlTtgSjf/w+JXZPCkCOAKX3xG8s2HHV34lfLj2IOIVzembCDZDutxSPHuA9WxMbiLEVgdRIKjxJUfOgrywcrv7bxj7xKOCdRDE3nyJgEsrsvCZZKSeKjgLhU340vN7x2YOjBug==;5:Vuvboj14rWxvF0298Fr3cpF93WwWRBREV2cH5H+Ufsr3b6/5s1OvGdYyRepA6VxXjsfSfXRla39mHkbcoFz+91NB4I45lWL6ZEycLzaR3Kf8xyUgk/rZAX38daN6eUkRFKBbYaBTGr6XbULMLLbc5RX/12wUCAPEsV6Q1uwP9Qk=;7:MYP400e+sonHqphtRROLNylc4gZyyqTduT+kyDhEUhkwkzcRwP74WESXiTz7nUxGifvjSWY+vc7thUbeakG3ZewrX77W1v3W5LjzdkZMf54KoYWk7syaal+0bxIXO52PAqgJpanidgBvKp1Vu9yWTA== x-ms-exchange-antispam-srfa-diagnostics: SOS; x-ms-office365-filtering-correlation-id: 75d0a0e2-962d-41b2-57a5-08d644d1fac9 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(7020095)(4652040)(8989299)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(5600074)(711020)(2017052603328)(7153060)(7193020);SRVR:VI1PR06MB5630; x-ms-traffictypediagnostic: VI1PR06MB5630: x-microsoft-antispam-prvs: x-exchange-antispam-report-test: UriScan:(215639381216008)(228788266533470)(211936372134217)(214861330456307); x-ms-exchange-senderadcheck: 1 x-exchange-antispam-report-cfa-test: BCL:0;PCL:0;RULEID:(6040522)(2401047)(5005006)(8121501046)(93006095)(93001095)(10201501046)(3002001)(3231382)(944501410)(52105095)(148016)(149066)(150057)(6041310)(20161123560045)(20161123564045)(20161123562045)(20161123558120)(201703131423095)(201702281529075)(201702281528075)(20161123555045)(201703061421075)(201703061406153)(201708071742011)(7699051)(76991095);SRVR:VI1PR06MB5630;BCL:0;PCL:0;RULEID:;SRVR:VI1PR06MB5630; x-forefront-prvs: 08497C3D99 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(366004)(39860400002)(396003)(136003)(346002)(376002)(199004)(189003)(93886005)(305945005)(81156014)(81166006)(8676002)(39060400002)(7736002)(97736004)(14454004)(82746002)(186003)(4326008)(110136005)(53936002)(229853002)(68736007)(2616005)(786003)(316002)(33656002)(2906002)(486006)(76176011)(6486002)(6116002)(3846002)(53546011)(446003)(11346002)(6246003)(2900100001)(6512007)(6306002)(6436002)(478600001)(8936002)(99286004)(966005)(58126008)(476003)(26005)(74482002)(106356001)(102836004)(105586002)(6506007)(83716004)(25786009)(14444005)(71200400001)(71190400001)(5660300001)(5024004)(86362001)(256004)(66066001)(42522002)(42262002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB5630;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: TrBOwyTIGocjBHLd6q7uZJSJsoSrfMAaAEJ2rv4IICdH0ueB1Mh35JZKOGHxrwl4AMiKZuSC9Xzx3HyCsArhlkVpyrFJJZ+pgXkzqVwiKLx9BEy8SUZAQqIWwLWKRKLoJXSUM96rYgBQwq/vl6CarL5IUF+NfzJxOuk6SiLR6wx31WbHP7UfD+MXTgg7LzIbTUt5Zk8spUm2K9yWJx6vW3O+uA6zOvINkRelLpZfOv1TsPUBsxii72S5XWQ3ud4SGOpqG249hWGwkAbDoKBqD05BVcmTCQgXfX6Wplin3Y2UEVnyNDOjcw5GWcaRqRE/VKzDmi11QPT2/otXK8AyJboMKmVWptarFENjWq8Nc24= spamdiagnosticoutput: 1:99 spamdiagnosticmetadata: NSPM Content-Type: text/plain; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 75d0a0e2-962d-41b2-57a5-08d644d1fac9 X-MS-Exchange-CrossTenant-originalarrivaltime: 07 Nov 2018 16:56:36.4505 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-Transport-CrossTenantHeadersStamped: VI1PR06MB5630 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.125 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: , Sorry, I meant to reply only to Thomas. That explains the language which is= not the internal language of some category... T =EF=BB=BFOn 07/11/2018, 16:55, "homotopytypetheory@googlegroups.com on beha= lf of Thorsten Altenkirch" wrote: Meinst Du dass die Homs sets sind, oder? =20 Man braucht ja nicht, dass die Objekte ein Set sind. Insbesondere erlau= bt iuns das die Kategorie der Sets zu definieren (also beides klein und HSe= t). =20 T. =20 On 07/11/2018, 15:36, "homotopytypetheory@googlegroups.com on behalf of= Thomas Streicher" wrote: =20 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. =20 Every deviation from that should be signalled by some adjectives or prefixes. That reflects the practice in category theory. =20 Thomas =20 --=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, s= end an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. =20 =20 =20 =20 =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 =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 =20 =20 =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.