From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCT7X5N5SIBBBE5JRPPQKGQEKZJQUAQ@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-lj1-x23c.google.com (mail-lj1-x23c.google.com [IPv6:2a00:1450:4864:20::23c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 91549223 for ; Wed, 7 Nov 2018 12:03:31 +0000 (UTC) Received: by mail-lj1-x23c.google.com with SMTP id f22-v6sf355734lja.7 for ; Wed, 07 Nov 2018 04:03:31 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541592211; cv=pass; d=google.com; s=arc-20160816; b=K+nA7f/77Aq7gikL7PGHfSjAgoL2b7YazAfwK0f3VOUKC7jksGsM4h9TP3bztx/JlX ieAWqNn0d79c5s1wpU6RjMzKTjJsnoQoZoj536i+RGLb8nijx4oB6oY3YUmRNKrSEXY2 Op+FZbUDI7vF8AFD+4NvH87hmu2z9e2OZKnh8yjtRaB9g36pWISFcXOVHHd+tRgl8SdK 9i92KmHXQibS3TyT/sP3Kt+5HTjkYOnsnf5FrDsKlhkjJqaujkN1m2WCKdkqIByTHiR4 Kd2o1C34PA3AGANv2/1HKGYeRpMEG8mlTsxvLzfvc6Bm/ijCPlW5AHQUI4oLCLVVb4L1 /z7A== 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=MxC/G5sp7tPunfafzjhp65bW6b8rSEsRJ+vfRPFJrds=; b=ig5tDDMwNFsGLIIyaVnEWIKNoZIEFVCTgTws7/H8t3nf+P71D1tLI6rOSos4AB7k3O 3W2A0Kza2zcuubLX77I5NQk7vE7/zlZ61bDr0qnd7ANMjHU1XHPzNn/6TAqVwhGPyc1i O2Dkzve5qGq7NtZuI1kchjWPhMtnFVUL7WRVqXiK8avjGF685xclPgnYjq/BH/66+xoM elOi6SnI+YkgO1jT9B2bHotRBNxf/SNBvUphlP6itvO1cdawa9ft9Vgzhnqct57VuRwm AUFw428sDjh80muDow0fuMtKH+HgT7atHUNNmS2XANAwVtX9UhOABe6/EIQLmPDuOVCG yUVw== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of palmgren@math.su.se designates 77.238.35.140 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=MxC/G5sp7tPunfafzjhp65bW6b8rSEsRJ+vfRPFJrds=; b=RQUY1KwwAyfyZh4fwWA7fqZZPk983SNlwLVvTupzacQYgpyAQ+lOA/4xD+iA6XrmYb KkQRknmkEl54x3SULm36YRbU1fMiwvAIogKXkH3d5dJcHXnBMsK2FtdvLwTbugHymQdb VcuRvx/a+l/pR6lLFiA+D4TmDMPMavhgeywCe5QAR8skRGEAChPqx6MblNOuj9O92x7i kBNLBt2Asy9PnTRgzter9NtJWJfvBo9KbR7DZ0O+Ha5HwA2ROody3/v7B3UiWMaWC62g 2dQwNmJoCCQjzJU496skuGEb6UNAGMs7FnjQmMB7eHed/mR+NjBK+s3kzB0hFsOraFSe wMMg== 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=MxC/G5sp7tPunfafzjhp65bW6b8rSEsRJ+vfRPFJrds=; b=fZXlSR4+2p0Cdr8adpPMBdrl/2kVT8Ib3ACqOAyFgW+YtiIR3UCzNSKowZ7XHZR/Ez aRR5Y7XQPXcFLry0w/47g15Nf+5Vqzwf7dgBaVtfVy2s35q7W0q49dMkNVsCQlh2xyku GMrZN5/wGTuqAdPzfdKMlwFURwAlpzQY+Mob7TfhtHmJF8ypORHjG1eqOBuw+r1cRB7W NHtJ8dwVeLlJXuvyGe5hwf/J48Hneeg6AmHdbMZfIZw4GTXKy5EaRFwxrVD4be+K9yU1 aWg3VOnN+L7eWfVnJA7l8nyvYKZMCbkdWo93KFWq5LM6mc16ybdvGjXCfYU/u9dICdEz X/HQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gK7ucB6TVTh27coRrxT/KzH7VdVVo8KQPZTMYZFLMw6gB/ZvuKt Kgzrp4vh4kjWWkLyeFwRNzY= X-Google-Smtp-Source: AJdET5d9Evi6+BqrbQs5oknqJqQ7ZIlDzZtxxaG5MffOWDmLpRdwKmWmN2g+DXcBy4lGVpLYqnRaRg== X-Received: by 2002:a2e:9ec8:: with SMTP id h8-v6mr6389ljk.5.1541592211347; Wed, 07 Nov 2018 04:03:31 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:2a44:: with SMTP id q65-v6ls838466ljq.1.gmail; Wed, 07 Nov 2018 04:03:30 -0800 (PST) X-Received: by 2002:a2e:98cd:: with SMTP id s13-v6mr170224ljj.30.1541592210681; Wed, 07 Nov 2018 04:03:30 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541592210; cv=none; d=google.com; s=arc-20160816; b=SMEdTt1OiaCR0a+oXV7rAMh479Xw2LXTZdid+EoA5Xir4mH5/zdFomSxVSGlmEFYon Yi7cSeqeVIasIG+kKpEge4/EMotxDDUxCJPTK2MtJ7UonYDQQt60dd8euf/bDj0FOrzq vxw3NHEo5SCoID9gFUY1P53fbb7iR9VRcja2m29NovbmcRYtGG5TRGq0asHxhCP5mJB9 5lGQSVPPQyEKswSjtIE+gSHYIaU2/P7gJGB01+xFUElTWB8vkDU+GS8Q+d1j0Fgb6BHF fPup0ALxDXvubOCIctTL5Qm7phZnAGEtTaGg3qkTCUzJGWay06AQjYIdOFKPkr/fqVec KHbA== 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=xOZr1hwcAPs216jm+AK+tLTzGdIA+abAOQZDyR9ZK+0=; b=Csv5ki7f/siyFO3ML8ABzLcxDTzH2D4akO9ATlae5I2Dd+6T1AY3m4eln9EBj6x6ec l/OipcJ3yI+Lp1nS+TNukjpTzkJaF5MwtiH4DJHRMYZ/yAHJK7nfjlDTr5uv6rc0LYnD hPPgUyTnCxZtL9Nztg0OAWL57dPv3O1fdm7+M28qjCGw8sAb4eePehODq8N/UdaHx3d2 Od16aTQ11cIWb+HQGVlHKLDY/UCyp4EYedPuV/BKoPcGZJxu9iv+p00u2islvQBNbm+4 054T+ezdlAoMzQKdRR/jOTTMhs6LorrtMBcp31z1uKwLEoZq2i3PFsjzNeHZAekuSVJ/ 9wWw== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of palmgren@math.su.se designates 77.238.35.140 as permitted sender) smtp.mailfrom=palmgren@math.su.se Received: from mail-prod-route02.it.su.se (mail-prod-route02.it.su.se. [77.238.35.140]) by gmr-mx.google.com with ESMTPS id l5-v6si15018ljh.4.2018.11.07.04.03.30 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Nov 2018 04:03:30 -0800 (PST) Received-SPF: pass (google.com: domain of palmgren@math.su.se designates 77.238.35.140 as permitted sender) client-ip=77.238.35.140; 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-route02.it.su.se (Postfix) with ESMTPS id 42qlS22JLVzxrx; Wed, 7 Nov 2018 13:03:30 +0100 (CET) Received: from smtp.su.se (mail-prod-smtp04.it.su.se [130.237.181.99]) by e-mailfilter01.sunet.se (8.14.4/8.14.4/Debian-8+deb8u2) with ESMTP id wA7C3Tju192913 (version=TLSv1/SSLv3 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NO); Wed, 7 Nov 2018 13:03:29 +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 42qlS12TFKz2ytn; Wed, 7 Nov 2018 13:03:29 +0100 (CET) Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories To: Ulrik Buchholtz , 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> From: Erik Palmgren Message-ID: <8fffa0be-9bf3-8a7c-ad75-ae2249f2ebd3@math.su.se> Date: Wed, 7 Nov 2018 13:03:30 +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: <706ac90f-ebd1-49f8-bd0c-2029549373c3@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=130.237.181.99; country=SE; latitude=59.3247; longitude=18.0560; http://maps.google.com/maps?q=59.3247,18.0560&z=6 X-CanItPRO-Stream: outbound-su-se:outbound (inherits from outbound-su-se:default,su-se:default,base:default) X-Canit-Stats-ID: 09WV03tyR - eaee97d495e9 - 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 77.238.35.140 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: , Setoid hell? This sounds like a sermon ... :-) I think the critique=20 needs to be a little more specific. Den 2018-11-07 kl. 12:51, skrev Ulrik Buchholtz: > Let me add one more point: in agnostic type theory, we can't define the= =20 > type of (Cauchy) real numbers, so we make do with the setoid of Cauchy=20 > sequences. Likewise, we can't define the type of (univalent) categories,= =20 > so we make do with the 2-groupoid of precategories, equivalences and=20 > natural isomorphisms. >=20 > In agnostic type theory we are both in setoid and higher groupoid hell.= =20 > In set theory/extensional type theory, we can escape the setoid hell,=20 > but still have the higher groupoid hell, and in HoTT we can finally=20 > escape this particular family of infernos :) >=20 > On Wednesday, November 7, 2018 at 12:43:32 PM UTC+1, Ulrik Buchholtz wrot= e: >=20 > I'm a bit confused by your message, Peter: HoTT doesn't have a naive > set interpretation 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?) >=20 > As I tried to say, I find 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.) >=20 > On Wednesday, November 7, 2018 at 12:10:10 PM UTC+1, Peter LeFanu > Lumsdaine wrote: >=20 > 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 b= ook > terminology, with =E2=80=9Ccategory=E2=80=9D meaning =E2=80=9Cuni= valent category=E2=80=9D by > default. >=20 > For my part I lean the other way: I think it=E2=80=99s too radica= l 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 > interpretation (or under the addition of UIP to the type > theory).=C2=A0 Choosing terminology 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. >=20 > Based on that criterion, I strongly prefer taking category to > mean =E2=80=9Cprecategory=E2=80=9D.=C2=A0 A big payoff from this = is that if you > formalise something 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 category theory, with all the > terms meaning just what they traditionally would. >=20 > 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.= =C2=A0 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. >=20 > =E2=80=93p. >=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.