From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCT7X5N5SIBBB2ODRPPQKGQE6EOOIIY@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-ed1-x53b.google.com (mail-ed1-x53b.google.com [IPv6:2a00:1450:4864:20::53b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 8f8ba55c for ; Wed, 7 Nov 2018 13:00:25 +0000 (UTC) Received: by mail-ed1-x53b.google.com with SMTP id m45-v6sf9471881edc.2 for ; Wed, 07 Nov 2018 05:00:25 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541595625; cv=pass; d=google.com; s=arc-20160816; b=J34Qgqs+/8zo3MMh4gVCHOjcqYXOoTDRpvtR4bCOXvnvf3WUfDJyrEpFABjn9DU6Re qQm/h2RWvhVYal2hYaqQAmkBE6RIDWsYZ7yXzWfJBzJlV79P17LGYTuwbgcI29ZKIIJb 6D247FnkO9S7xkt53h3tFeFSobRCrx+bQKNt1TB8iVt70u/xjGBhXMNlivx7EBOkC/a/ qmn/Gg7/WrTmbO6B7PlVRtgODCt6hiB0iMvr2emJvOBO9+wYeAtnMOs7slfgfyB/qTlM atcCEhoBJhVKwJ70oMUw+OZdONFHcpouZT0uZBsJKjKS/x8UDeb4VPbPirSCD2bLi+wZ o3VA== 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:content-transfer-encoding:content-language :in-reply-to:mime-version:user-agent:date:message-id:from:references :to:subject:sender:dkim-signature; bh=5jk4OwLVJsnLSQ3ZNU3wTWBLXBLX2yat4FEsQnlqaFA=; b=BfOEgA6TMs7kbo/UZx+ftrK4XLydEfRnX4gTHTXj75CITRIMEPZ2tpt2REHAz18LQQ /C3mV3lstTZAuosv6IGgB/SfnBsdvh1v47S64L+h4twbXb5YFv2Gfgz15O/iWijTp2/0 L9Se3/2O2fA9eSkxD5FOKe6DKDYpUYSuPqj1OvNheNWFq/NAH+u5wkCBA10uyLmsL12E 6PWQlh0TadKRaatxOK+ILlLELg4vKluu333tNi8hLt1qciT+QF/KeST/q67f9kuh8cCl WTVGBit4X+haaHJkrRwYbrx4ohi3g5sAN79xKmLJ5X7auh+/U/39qFZHjQ/b+34CG10Y 6jkw== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of palmgren@math.su.se designates 2001:6b0:5:1213:250:56ff:fe94:7fa1 as permitted sender) smtp.mailfrom=palmgren@math.su.se DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:subject:to:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-language:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=5jk4OwLVJsnLSQ3ZNU3wTWBLXBLX2yat4FEsQnlqaFA=; b=Hdm5Ilupod4Nalv3uYdOWW9qXelNU/2jHixpD0bddRCCLaw2BZZe3hTB+EaSEeEnFt F4PIJbG3I7Bn/O++nxtE0oT2qZXhvakBT9Ynsx1rgI3EdvNOYvjh6s7fXZREcQBQy/PK OIvL5yY5mZlUzMvHrnIj2l5ysqH9Wltr6n5gP6PlPb5OOS00JRug6m6mqfdl5UZGszaW 7aPXADbSXKJ78KJzrBQaHohDNzb1cXwaO2CxqTG8o7jhEOST101nU7byYum7RNB6fri2 p7TVix2xu8CyrrT0KmNTssP6qN5As2Gd+/uPfjX74ljAjkrNBVLqoEIB+dPCRx/Q4tLT 4HkA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:subject:to:references:from:message-id :date:user-agent:mime-version:in-reply-to:content-language :content-transfer-encoding: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=5jk4OwLVJsnLSQ3ZNU3wTWBLXBLX2yat4FEsQnlqaFA=; b=PTVxuMI89LZFTYHq0V8KEq+mXm5EmiAOLPi9cP4ZPhj5jOCNGcPWmPkgIZxruK8dEo u0h40R8/oCiMzmQUNjeT0rG3MA6KRqR0Yrpc0QrdlRdkZL0C0vxQmfUl7KMO3OamMw0m MQrZV5tLTRmBk4VWrNQfuUTzvbCDXHyT3fyyPSsp6s4pg5+8PyP9aLeq8XG1mHCzHJDH V2Xb+MwC33ZLyG62TFRfj/FJzm65XVO+UHC+N8nt0DY3Y6udZFi+ddViK5wI5QcyASI4 YBBnYnuTOFLIKXFp9myrjuw/r9GX+meSiex0vFAGNWhBEUX7lWdU6yCOWEB/fMoie6M3 f/ng== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gJILr/UeJnIMUYbgTVTvxWMV9j5KuypQq1WPctBQT5yLJIv7sd/ mpeosHj59CN+UBZR2DjRrR0= X-Google-Smtp-Source: AJdET5fdFptLFDh6VCVHkVdpDJXaN3jSpERMrSnoJe8wE3YxjPlTarJss5akjySAPpXaPVYQru0jXw== X-Received: by 2002:aa7:c995:: with SMTP id c21-v6mr658edt.7.1541595625215; Wed, 07 Nov 2018 05:00:25 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:3381:: with SMTP id v1-v6ls3111663eja.9.gmail; Wed, 07 Nov 2018 05:00:24 -0800 (PST) X-Received: by 2002:a17:906:1603:: with SMTP id m3-v6mr21261ejd.16.1541595624617; Wed, 07 Nov 2018 05:00:24 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541595624; cv=none; d=google.com; s=arc-20160816; b=HzM17ZWxcp/2LDaJMwpt0H3SO4nCd623HIMPVKYVOcb9sPkAVdGuyJBreWFL/96AUr yqWWuHCmiUny60mC1hidvI8FCWg7xHgKwpZcuumR8Ye7u0JbNrH1E9pa83gvYt3GP7ki aJsbVTHSk0gtf4GKRLDLo/w2umNJVq3WkwoI7XqUvOPlQoqMnqY+k5WCZgbaBQx7mbT2 8Wn4gOswo/yb9QuQvfvMQ6Pz5A9mdZw3plpre5Ikwz+h8XqCTsEuuX7Oq5/N47S/va4S sgeOaJkJgvRJPdNEHJl1UuvaQX9RpL+rF0hyHhR2R1ciONTpo0MGnfhutp3s4sMfAric kJTg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject; bh=P2rAPYaTI6bjEghJRTYLAkZjX7jXo8O60PsTSGIog9c=; b=X/NFxLIqJBsHKq99FDrWlxA+kIQTkG9ECWJHSiGiKOuNJP+Cc167e7kJ1wKTnWHU3D tJFiEbVaRVm2zp+P2dgNJHWIQYKHF+qfU43LJIQNjYrSQdNfbEuf5dk2tRw3ZoEaVpmZ m7XRkTbourm2KvQEYYOb+sCTZFqNvTTics8QiFjmxkWB+p5HHwFLEjO+4USTY2Tq17t0 AXxlynUw3+GTHfA+tKSSAVkn8QZXUvrWKrs+7SZFVJXSb1OU6ccBPRQo6CpOWmylXtOR 5fa9zhJ4Jfdf09+PL3Z309ErdcDPsMJYkgo1HxCyX3k6F2pMJa3exLay3abfK0mqYRoX M2jw== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of palmgren@math.su.se designates 2001:6b0:5:1213:250:56ff:fe94:7fa1 as permitted sender) smtp.mailfrom=palmgren@math.su.se Received: from mail-prod-route03.it.su.se (mail-prod-route03.it.su.se. [2001:6b0:5:1213:250:56ff:fe94:7fa1]) by gmr-mx.google.com with ESMTPS id m25-v6si19238ejb.1.2018.11.07.05.00.24 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Nov 2018 05:00:24 -0800 (PST) Received-SPF: pass (google.com: domain of palmgren@math.su.se designates 2001:6b0:5:1213:250:56ff:fe94:7fa1 as permitted sender) client-ip=2001:6b0:5:1213:250:56ff:fe94:7fa1; Received: from e-mailfilter01.sunet.se (e-mailfilter01.sunet.se [IPv6:2001:6b0:8:2::201]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by mail-prod-route03.it.su.se (Postfix) with ESMTPS id 42qmjg6KcDzxf8; Wed, 7 Nov 2018 14:00:23 +0100 (CET) Received: from smtp.su.se (mail-prod-smtp04.it.su.se [IPv6:2001:6b0:5:132:250:56ff:fe94:2456]) by e-mailfilter01.sunet.se (8.14.4/8.14.4/Debian-8+deb8u2) with ESMTP id wA7D0NMK050310 (version=TLSv1/SSLv3 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NO); Wed, 7 Nov 2018 14:00:23 +0100 Received: from Eriks-Palmgrens-MacBook-Air.local (c80-216-86-31.bredband.comhem.se [80.216.86.31]) (Authenticated sender: epalm) by smtp.su.se (Postfix) with ESMTPSA id 42qmjf6h8sz2ytn; Wed, 7 Nov 2018 14:00:22 +0100 (CET) Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories To: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= , Homotopy Type Theory 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> From: Erik Palmgren Message-ID: <822765e7-947b-0780-e755-c0d7520418fe@math.su.se> Date: Wed, 7 Nov 2018 14:00:24 +0100 User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:52.0) Gecko/20100101 Thunderbird/52.9.1 MIME-Version: 1.0 In-Reply-To: <795a64b4-f62d-4fd5-9503-20c997b7b42e@googlegroups.com> Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: sv Content-Transfer-Encoding: quoted-printable X-Bayes-Prob: 0.0001 (Score 0, tokens from: outbound, outbound-su-se:default, su-se:default, base:default, @@RPTN) X-CanIt-Geo: ip=2001:6b0:5:132:250:56ff:fe94:2456; country=SE; region=Stockholm; city=Stockholm; latitude=59.3600; longitude=18.0009; http://maps.google.com/maps?q=59.3600,18.0009&z=6 X-CanItPRO-Stream: outbound-su-se:outbound (inherits from outbound-su-se:default,su-se:default,base:default) X-Canit-Stats-ID: 09WV10nTk - 75a944e08cf1 - 20181107 X-CanIt-Archive-Cluster: PfMRe/vJWMiXwM2YIH5BVExnUnw X-Scanned-By: CanIt (www . roaringpenguin . com) X-Original-Sender: palmgren@math.su.se X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of palmgren@math.su.se designates 2001:6b0:5:1213:250:56ff:fe94:7fa1 as permitted sender) smtp.mailfrom=palmgren@math.su.se 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: , Den 2018-11-07 kl. 13:21, skrev Mart=C3=ADn H=C3=B6tzel Escard=C3=B3: >=20 >=20 > On Wednesday, 7 November 2018 12:03:31 UTC, palmgren wrote: >=20 > Setoid hell? This sounds like a sermon ... :-) >=20 >=20 > This theological aspect seems to be an attribute of constructive=20 > mathematics. We also have the Limited Principle of Omniscience. Both the= =20 > Setoid Hell was created and LPO was named by Bishop.=C2=A0 Perhaps this i= s=20 > justified by his very own name. Bishop seem rather antitheological about mathematics in his Manifesto.=20 Anyway. >=20 > But seriously, I would like to have the terminology for the various=20 > types of categories settled and agreed among ourselves. I agree with the= =20 > mathematical argument given by Ulrik. I sympathize with Peter's=20 > argument, which tries to avoid confusion, but I think in the long term=20 > it may cause even more confusion. Maybe Ulrik's remarks should be added= =20 > to the HoTT Book and blogged at=C2=A0=C2=A0https://homotopytypetheory.org= /blog/ From http://staff.math.su.se/palmgren/7.pdf: "In conclusion, the notion of univalent category is too restrictive to=20 cover many familiar examples. H-category is generalization of=20 precategory and is a convenient version of E- category with equality on=20 objects. The notion of E-category is still more general as shown here." > Martin >=20 > --=20 > You received this message because you are subscribed to the Google=20 > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send=20 > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com=20 > . > For more options, visit https://groups.google.com/d/optout. --=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.