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-x438.google.com (mail-wr1-x438.google.com [IPv6:2a00:1450:4864:20::438]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id eb017b7e for ; Wed, 7 Nov 2018 16:54:05 +0000 (UTC) Received: by mail-wr1-x438.google.com with SMTP id d16-v6sf15454435wre.11 for ; Wed, 07 Nov 2018 08:54:05 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541609644; cv=pass; d=google.com; s=arc-20160816; b=QJaav0SLXRHPnOP+e/9QCsi47IK8tJIzVQmpV7TVhxNkRHaHi05GQnVCHx/ZawWxFT EtptmbbVeOuWDQMvD9JQcSfh2aNG/00pt0OwBHZ+ObqMmtM43SSvG9JHuVgfDT8L/qBl Ni0D519McNe80GbLkNwkChfN9a7jeeg0ZjA8kzJekFBl3mTwGWLnaXx/CYxP6pTWfK1p 1M29GOvHgiItOrl4Am7ulVaZma1Nl7ErEYbuCZLRL5DNoD+insjaSwjJHE8a/njbKBnD FHRy2ImObwIdbrVu5sJshD7fMBk25b0CBpdMQxf48e7DsNHanMiWxam8X6ZcUWbJnKmN EgYQ== 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=zp+wfBvZzPF8YbiSsjJ0zw4JhXplgxwt0CLtWjWhTe4=; b=f8CNFG1+qJXuYO6wMkc2ACswQAHye77a3WyGnUt3fy9c6I599Z0CHdg3b+UCzzOySR uc9qdaoDNnGClhnLe0Mj8fA58FLoV8gxzThC7qurpAnjmX6sDSVULWwzPvU7nI/gjEIw 7VTWnrH56xyn0idhmYAanTV2zGmFO1vPSGmNIPLhL2JIg8DN3wlCItmqXIKLCExTiai0 yzyW2bv9lzVx+6587IPTq9V0oKwjgxlE31XuYEEjWyq3npc6NuJX5TAOdrC9DQcMFg0l TfRGQmPQW+le3y43oBT025805wgxenhVtiVY+LBNa22Aq5LChSblOddrwKy0d8eZ37bl 3qHA== 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: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=zp+wfBvZzPF8YbiSsjJ0zw4JhXplgxwt0CLtWjWhTe4=; b=koeUHwI9UmYatpnaNfQ9383vphWkSVzbWfZfX33vGw6W/YecDw7/phAvSiVYpKN2yh aYcIuxz05xSiKpcWwNjEbmEEZUjzoY79bSwpPZpQbcLbJGZhduSE7oOGl/FaXpuzgAeg TMSsR1outjjsxFT+m6hlUAMj8KX4QSucJkpRZRcbEWYhE7mNbUujq2OENaNeExMb8STv UGmqN/iyR3v1GsUSlNoruosexd9BgU/eQYz6XAPfNy+9WkLUU8K1NrlP2b7nQobC0y7X JUn4o3MJFwb464V8bRPAGxjKF58pil4/lfZW78fsT55FTWP21Q215jun6LZWpalAN3ZG g+MQ== 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=zp+wfBvZzPF8YbiSsjJ0zw4JhXplgxwt0CLtWjWhTe4=; b=URJs3IWTT/k0UZSu4N+4me3ltwlz9FSNbI1tJL/lLMaB2L8TRyAfNq7v1fT5Mb25yF BIifqzndfSQMz9hw/WBIVN2zL5vWicEJT9ajxUmcrsdu8ccYh6PXOI5wIoIUuWqOp3GQ JkzfF5SSXLjgPcPnyramRz7uVLwjGqY96Au+4j6eWkQYbOy2sg7NY0H4axWQs00sOKUQ R0rkF2HBUsJTKKaPCQVqbPgTcHDrvUVWxmfZDXMkmCgw9ScSPgK2oDZWuHlIGeOEVbYe Bd4rOpaEGb9zlaS4koWYZahDjboO2L5yMVq6SAvmNjClWqwemAL8u/HHXkWt/iNw5evC QgCw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gIp2uMVN5mv81q9Iyb5sQsdmoL5HbCcqlDOAtq9AoNmUtE4zNcQ xDQHPMxLRaXgYxUm8MLUA58= X-Google-Smtp-Source: AJdET5ex1RPZKJJlaKeDD7qYcRukLT7k0qsLMg4XyB5g7tGiLYa825nqJYfWXk/8PJh62JpdpoeeSA== X-Received: by 2002:adf:f5c6:: with SMTP id k6-v6mr10769wrp.5.1541609644301; Wed, 07 Nov 2018 08:54:04 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:b6c1:: with SMTP id g184-v6ls2740748wmf.9.canary-gmail; Wed, 07 Nov 2018 08:54:03 -0800 (PST) X-Received: by 2002:a1c:c50f:: with SMTP id v15-v6mr222512wmf.23.1541609643611; Wed, 07 Nov 2018 08:54:03 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541609643; cv=none; d=google.com; s=arc-20160816; b=UxUr+EHBXla5H49ZlhwYz3MCgfA0Yaz+7WqwRwbcRzAfmtgu2cpqk+UMeJ7jCCp+4P XeGDqlDi3Se+G2rw4pkN2LBSMX9CRr5D5P9oEcIQTbJ/EUsDQbI3L+tt14lebLLLsDTl 9wqTzxU24bAK7ky0uBCLhLvBWCju95BVSZZm5POpcUeLNhPgk/8D3Cmez1FV8XoqLGm7 T+Y1iHqrSxuWDftyZcAaL/YoKsm95xGvhQtyHHKSh34gehpp7nF9Q1sFiTUgf10Z1ejG IVkoFampmSstWEOiPxN1WkVKl9jV6hEdOx6ALAnzo4ugK0sJeqMWwNCPVMyyTgniZLbF +sUg== 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=EUGbNXoNp6G+Z9/sCPG26yYY8aj+tbZJUpDcP4UiSg0=; b=jhV95S7BjISmz/X4f2mpyHgpdsSHuti5p9AiZHJyRVuwPrgiMjnSHc6YqPVeKw7YTH SeTtcWWohlj/ghhCCGXKrKBFsQcWX2MxLvNp/5HJ067AaWARRtYSwbzufYGafqt9eRa/ ShiIQF83yze5/9gheDba94cwsRrGlKPDyN5vsGbFKvy/qlo2g5JFgF46rzPljwe9xEVs f1SV1PGS0U7RQ8PTnWfv7wJ4xM4hLBcWHHRlaTkZlI0ZWthjFRjQYKG+pkWqk4psCLAn ADOm2Zi1Mbag9tPugdJfDDGBf5BQsDkJHSQw/hoPFejUkUu+qDfcACZk8XVfdjeJM8zs OMhA== 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 h137-v6si64396wmd.1.2018.11.07.08.54.03 for ; Wed, 07 Nov 2018 08:54:03 -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 32A202B7C40_BE318ABB for ; Wed, 7 Nov 2018 16:54:03 +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 B7CD62DDB0E_BE318AAF for ; Wed, 7 Nov 2018 16:54:02 +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 1gKR5e-0007IW-GP; Wed, 07 Nov 2018 16:54:02 +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:54:02 +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:54:02 +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:54:02 +0000 Received: from EUR03-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:54:02 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB5664.eurprd06.prod.outlook.com (20.178.122.86) 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:54:01 +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:54:01 +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: AQHUdoWaEWRL1VfTr0qqVzzaadLFAqVEJ8sAgAAJYQCAACergIAABn8AgAASxQCAABXOgA== Date: Wed, 7 Nov 2018 16:54:01 +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> In-Reply-To: <20181107153556.GC26970@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;VI1PR06MB5664;6:K5J5bv7lMseB8cTjSW7Cb734Oj7Zde8urTZMvfuBYHFlHozpeq949JizdvTf8ZezyD5i0HaOr8nlZq+tWJ8Pt+g5FsiPKX0/WX6e6/GtJ63ajbicsCrD1mj89XvUbqn09c/P9niJRljqTJ8f37/v8cHxGTQ3lWuEVR8GXB896kfVmWjuwvollb/XmeN0yBiJhYKVsLCSOZDFPrQ+SQvP9v07xcBt0KREo6aaSZvOXUzsUu96ugbfWmTyYHALWeFuT/gQ67z2MmcaM3xBGYI4ITeJ2vTRAC3QAi0cYRCJFaqWnr1TVtab9tWf6pK/Tv0UY7LDKmfB48HJ/L92nujn5NgPt0oJ53QXLd/fSN5c5+QCgSfbYEmQ0htnCfIoTqbb1DiQyKJwMmwCn4Sx/Jzaf/8xcSJzQ4KCmFKkiTdm815qSeByx/QmvVZpAHqYl0CL6Q0axrxklPw1Y54+DyHKDg==;5:xd1H5KEFYlDJIiP+h3jXf0PvZbxe1jQYe4H9c8968nI6/qMHtKoOrVrYi521GpeiyNg+3AclkoizNJZho9ONYm1Cvs+Jec+/dJUyDEQV6eKK/IVKKqWpDg3VRlVf9eC9WVSr0Wh4tCCd3bh+u2SHSZPshRd+Lhw+dQBbYep7+Ls=;7:GauBD/NZdijK3w29wPKpWzhUKnJPRSo4ReQ49idBwJ4XiP6pobpGBbcriFaemE++1eg/vTcojaOAps8fwUuUW3v15G/X8OY9Z+5WaSr/wTNWYkZxH4j6tXrlVTRYKt4ec9me9/KSdGcstGKu38kE6A== x-ms-exchange-antispam-srfa-diagnostics: SOS; x-ms-office365-filtering-correlation-id: 7fdb32a4-507b-4df4-158b-08d644d19e34 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(7020095)(4652040)(8989299)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(5600074)(711020)(2017052603328)(7153060)(7193020);SRVR:VI1PR06MB5664; x-ms-traffictypediagnostic: VI1PR06MB5664: 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)(8121501046)(5005006)(93006095)(93001095)(3231382)(944501410)(52105095)(3002001)(10201501046)(148016)(149066)(150057)(6041310)(20161123564045)(20161123562045)(20161123558120)(201703131423095)(201702281529075)(201702281528075)(20161123555045)(201703061421075)(201703061406153)(20161123560045)(201708071742011)(7699051)(76991095);SRVR:VI1PR06MB5664;BCL:0;PCL:0;RULEID:;SRVR:VI1PR06MB5664; x-forefront-prvs: 08497C3D99 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(979002)(136003)(39860400002)(346002)(396003)(366004)(376002)(189003)(199004)(53936002)(14444005)(66066001)(5660300001)(786003)(14454004)(68736007)(316002)(6512007)(6116002)(2906002)(3846002)(6306002)(71200400001)(7736002)(99286004)(58126008)(110136005)(305945005)(82746002)(93886005)(83716004)(71190400001)(33656002)(86362001)(2616005)(11346002)(476003)(6486002)(4326008)(39060400002)(6246003)(478600001)(446003)(76176011)(486006)(81156014)(81166006)(8676002)(97736004)(102836004)(186003)(966005)(8936002)(6506007)(74482002)(6436002)(106356001)(25786009)(2900100001)(256004)(26005)(229853002)(105586002)(42522002)(42262002)(969003)(989001)(999001)(1009001)(1019001);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB5664;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: YP34uzEThaNuWGOgos1iF/ugbZClXjoZY6f/pIpkKO9VcV5gNcDgSu9ZZRxoGPq7RQusMfuvNa8A3ZC9yUvuKllN2ecUUaV/t4VAG+BFfzpdA+ADo1ea+xHFTjHcxxg5zemNuE2fZYfwqo483dh75jU67JdxwEa5mlWShDcr65mK4VaJjmdmvt3GsGCmwkJCcbbjjlwfynLsciB4VcTaFrVQ21qadAhs1B6YRdkWrAFvrtg0xh/gPuVXVEZekMvssrKAmYQmlhtKTH7G5WL8wbPgfdY6Z1kBlTLXuJvE7jV8bhM5DCGHwtn37fHFaen931x6yzuteWVODHHscH22yMc0d4P8rywWSfoRjcsBZdU= spamdiagnosticoutput: 1:99 spamdiagnosticmetadata: NSPM Content-Type: text/plain; charset="UTF-8" Content-ID: <50FC950B495C0240AA4DED6C75D4125C@eurprd06.prod.outlook.com> Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 7fdb32a4-507b-4df4-158b-08d644d19e34 X-MS-Exchange-CrossTenant-originalarrivaltime: 07 Nov 2018 16:54:01.1270 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-Transport-CrossTenantHeadersStamped: VI1PR06MB5664 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: , Meinst Du dass die Homs sets sind, oder? Man braucht ja nicht, dass die Objekte ein Set sind. Insbesondere erlaubt i= uns das die Kategorie der Sets zu definieren (also beides klein und HSet). T. =EF=BB=BFOn 07/11/2018, 15:36, "homotopytypetheory@googlegroups.com on beha= lf of Thomas Streicher" wrote: 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 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.