From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCR53C7ITYGRB27MRPPQKGQEWSOBJOA@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=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-wm1-x33d.google.com (mail-wm1-x33d.google.com [IPv6:2a00:1450:4864:20::33d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 469f1990 for ; Wed, 7 Nov 2018 14:27:55 +0000 (UTC) Received: by mail-wm1-x33d.google.com with SMTP id t130-v6sf11368853wmt.3 for ; Wed, 07 Nov 2018 06:27:55 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541600875; cv=pass; d=google.com; s=arc-20160816; b=fuJ2Qaf+dpmg2xHDAB3vH3Bm8MJV1n9lMmLNSLmWCgCJT9bvIXHQgJFDOOuI4GjdHU f5pWqp+duBHxJL14YCoiejcgzf9KOeUlIiBLrxdqwsi9mWcBk3vXMAiNdpM2mDZn4Wbn eWDATZdRuGVkdAUZI+eZdWiUHERmnBmcNiq1MvVENQg3NvgiLp79alJYYZaUe6giN4wS NkEEABxw9W7SSvEpjx9h8VhvREO6NifbIE4I9eaF6iMBQwwFejpEPiLeoWC99e8abr91 1nNiLWWNOcDLCWE2A/Ro7UuvrntnH4eiWI8BLwbTpdJfOpmQAHEPLqlMLG9cnt1edZ7h eEvA== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=EGPH5CBX+uzfhEG/fIypMQ8ZqbQtNmeBhSRh8t7rK/s=; b=IM2qCHIjGRaKengDCrRHg0UPk335UKOvil+oQw77XtLQouZqBk+3WOTMZBk/BIecrI awzajTvyLwjnGnKKLe/NgIymX5Nps8Y+jIsOeqCefrj9pjnQBXdC+PxKHqty+mWXpRBj 56xYKhGJOYk/KyOAMLZ/jEJrlWyTpwGfULljtVIqNAIZBl8PYO+oqGeHfMvyxYHf7gbe 5a1j6nAmwm8tFxgHNalIvXe9z8xPEPGUZQvssitvoDlhnpyXK7cFzAUZLzpEMSyj9al5 E4gi0t9+eVAevcfO8c/MwEFwpvvAijIu2CZwIKin86w2WWMflOknqu/wHnqs81pb8/6f wIOg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=PWxZjC1j; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2a00:1450:4864:20::535 as permitted sender) smtp.mailfrom=p.l.lumsdaine@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=EGPH5CBX+uzfhEG/fIypMQ8ZqbQtNmeBhSRh8t7rK/s=; b=G2RuFMbU22TyJCpBdGQ1B9+3M+rv+5+nEeJDysO6AW/J5+tCMpeb8/nz02ucFv7zkt o8pdb4IUl5l9DnQN6Uydeql6ntzKGVjR18US0hZlWvxLQyqCbFhmpoCQ7WNXu9j081Wh Gp4FKrVph8UGF0TqcNtrSumM4SWPqxDfB1P0VbEpaMVmYVD994x51/wkXj9GMY23p4st 3xpI+T/YJJTGe2iCqLiC2zrZHzcENRhWsfENKCpNZsEEP4MzkVS6exV5/mNISRbWdRNP xTnAmaGJbV4NY6lmzQgYS+QePVeUiB3PgnrpAaCtDwc66fEECUHfbffq4SQ+Cg6IrwCg HdjA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=EGPH5CBX+uzfhEG/fIypMQ8ZqbQtNmeBhSRh8t7rK/s=; b=mfEYKq73P1iCKkt06ANnztSpQ8OhKhVqRjHYR8Fqgebf3UOsVxOeKObsLAvCW36sZf B5NPievEYNeylqwh1mAhg19yuXudP2ULOxdRiWjOR7c8CxT97zD7JR4OUzzlAM1Lset6 2wBYDZORpQ/oCok0ANcl0ihgxcnLRkX53I11JonpOUNy/yK9C1bdSpiU8A4KfDHqD92B poYnlqf3sRxwtQzGqdu6YWg+w6Mb4vYpR7HSXPXUOKbnn8JXcNGaRKj4E3ur0WR6ajeK LVYrZTEmIOlKJvxIrCRjCThwkg6ywpeFP75/HRvMMVbLkAlMCREgKDWXiWmk36nKoinj 1hmw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc: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=EGPH5CBX+uzfhEG/fIypMQ8ZqbQtNmeBhSRh8t7rK/s=; b=Q1zVnk0a/NTq345g4H9zTqEMp76Dt0sJQYHfd5C/a8WKoeVNdX/AM7A3j3p85oC/rW vu48tckLI7pNI8Y6OwCOh0oMhea8TE0yJETOW5RnknjXbwvmmNjepMldFP+dLbd7afkJ f13nqLXmPgd0Wyk+MCI1d57MuyO3GEoaqvkCAvyLOn5xBJHJNMaGsBotmDjGPuky4J5d Gv65g0ZduqfvgiDbeBCs9cLDzd0yvK8Of5YEENmtck1nlhTwO/f8vBfkYuRqU4KcJgCq Sjjdvd4fn43NwVhSM0r8/ZEuV7sVyOdvAP0sEJLUoXlh6YZmQKdV7XI8dwevLn/menCQ 0TXg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gJDvYYofXMCRYu5/m571KbvxuD8MCaAOW246Dr14262BXgI2GWG V21kUoFW8vSGEqRYBWvz8AY= X-Google-Smtp-Source: AJdET5eWUDOlB6ch9hGI75ByGb6VuO661EGirOmjUCz5z5azxQY/fvb9b6Snrgv+R4kLqCv4i88h2w== X-Received: by 2002:adf:8226:: with SMTP id 35-v6mr5530wrb.0.1541600875424; Wed, 07 Nov 2018 06:27:55 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:d3:: with SMTP id 202-v6ls2189127wma.15.gmail; Wed, 07 Nov 2018 06:27:54 -0800 (PST) X-Received: by 2002:a1c:605:: with SMTP id 5-v6mr87321wmg.13.1541600874774; Wed, 07 Nov 2018 06:27:54 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541600874; cv=none; d=google.com; s=arc-20160816; b=lCvBSPTcaa08e/0TUU8Vscm40KZCfi2t2n5XFEJHfqQT/ov+XFF6WB6Fkg8JJOcDie wYLYpPXg33NNqpEEExRg7chlyY6MTk5rlogukBot2VeSmEXOon0Tzwus4WkgBeldWNkJ KCem7HxhqI9vOOyUuaakaOR+pn6UnRbvYegwUDFBvPanhNxhOM8Wss2ykdNgVzpugdwI AXPjSlEPItf1IflQnzVxm7cQw3pYztk71uaKuVF0rwkti1CfKtOr0qDqPzpanEk18Tbv eYWUBqXjjdTwNgfkQaX1gB/5LrdfCOTZT/C9uGg7O1jbuCvve+/jOX9YYhBA9VhFahKW BHwQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=pTVeFF3dtfZqkVttytn47HIMjQpUIzTxBEKFXB03V+Q=; b=fSq6oIg8ySqzyyXiLE/iZWrkSp1NfgEBnhSpIaWtVTYSg95HtxyHKpcVknoM2c/C/3 koQ6HjT/zPbxMrP2grUuUqQzDcZCWV09QFBUXeLgswS/Bk8/daIQyARUaKJJW+Rh5oc3 ItuUru2ZxCBCQIQ5GoxhLH9i2XF8/8py0gEhNDgHzJBhB8HC+twXIdS9S2/Hak4pJygU PO28G2O+DPbWN78hh1SCyfypSZ2d7vqEHVtusHa91Oh148m3uHG50l8jxDVVNKaE7QFq toAGKItzx+C4ZqcQ61S7hrY43ZS/pCSmtoZEmit1NVJq15AnptdqRM6OeAGZeHuUAsFm GB8A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=PWxZjC1j; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2a00:1450:4864:20::535 as permitted sender) smtp.mailfrom=p.l.lumsdaine@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ed1-x535.google.com (mail-ed1-x535.google.com. [2a00:1450:4864:20::535]) by gmr-mx.google.com with ESMTPS id u13-v6si23644wrn.3.2018.11.07.06.27.54 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Nov 2018 06:27:54 -0800 (PST) Received-SPF: pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2a00:1450:4864:20::535 as permitted sender) client-ip=2a00:1450:4864:20::535; Received: by mail-ed1-x535.google.com with SMTP id c25-v6so13545644edt.8 for ; Wed, 07 Nov 2018 06:27:54 -0800 (PST) X-Received: by 2002:a17:906:71cd:: with SMTP id i13-v6mr284012ejk.37.1541600874417; Wed, 07 Nov 2018 06:27:54 -0800 (PST) MIME-Version: 1.0 References: <3c553ba0-2181-44ec-b790-969a8115ea1f@googlegroups.com> <1a3288ec-ca0e-48ce-80ad-9cad01f56845@googlegroups.com> In-Reply-To: From: Peter LeFanu Lumsdaine Date: Wed, 7 Nov 2018 15:27:43 +0100 Message-ID: Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories To: Ulrik Buchholtz Cc: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="000000000000815318057a13ec5e" X-Original-Sender: p.l.lumsdaine@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=PWxZjC1j; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2a00:1450:4864:20::535 as permitted sender) smtp.mailfrom=p.l.lumsdaine@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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: , --000000000000815318057a13ec5e Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Wed, Nov 7, 2018 at 3:14 PM Ulrik Buchholtz wrote: > On Wednesday, November 7, 2018 at 2:58:28 PM UTC+1, Thorsten Altenkirch > wrote: >> >> As I tried to say, I find that precategory is the novel concept, and tha= t >> both strict category and univalent category should be familiar to catego= ry >> theorists. (They have a mental model for when one notion is called for o= r >> the other, but we can make the distinction formal.) >> >> >> This is too clever! >> >> >> >> If you just transcribe the traditional definition of a category in type >> theory you end up with what in the HoTT book is called precategory. This= is >> confusing for the non-expert even though you can justify why it should b= e >> so. >> > > No, you get the notion of a strict category, which in some sense is all > that you directly have in set theory. > No in turn: you can arguably get either strict categories, or precategories, or what Thorsten dubbed =E2=80=9Cwild categories=E2=80=9D ab= ove, since =E2=80=9Cset=E2=80=9D in set theory is the (na=C3=AFve) interpretation of both =E2=80=9Cset=E2=80= =9D and =E2=80=9Ctype=E2=80=9D. (Just as when you transcribe classical definitions in a constructive setting, you sometimes want to read =E2=80=9Cpredicate=E2=80=9D just as =E2= =80=9Cpredicate=E2=80=9D and other times as =E2=80=9Cdecidable predicate=E2=80=9D =E2=80=94 all predicat= es are decidable classically, but that doesn=E2=80=99t mean that their constructive transcri= ption should include =E2=80=9Cdecidable=E2=80=9D by default.) =E2=80=93p. --=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. --000000000000815318057a13ec5e Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Wed, Nov 7, 2018 at 3= :14 PM Ulrik Buchholtz <ulri= kbuchholtz@gmail.com> wrote:
On Wednesday, November 7, 2018 at 2:58:28 PM UTC+1= , Thorsten Altenkirch wrote:

As I tried to say, I find= that precategory is the novel concept, and that both strict category and u= nivalent category should be familiar to category theorists. (They have a me= ntal model for when one notion is called for or the other, but we can make the distinction formal.)


This is too clever!

=C2=A0

If you just transcribe the traditional definit= ion of a category in type theory you end up with what in the HoTT book is c= alled precategory. This is confusing for the non-expert even though you can justify why it should be so.


<= /div>
No, you get the notion of a strict category, which in some sense = is all that you directly have in set theory.
<= br>
No in turn: you can arguably get either strict categories, or= precategories, or what Thorsten dubbed =E2=80=9Cwild categories=E2=80=9D a= bove, since =E2=80=9Cset=E2=80=9D in set theory is the (na=C3=AFve) interpr= etation of both =E2=80=9Cset=E2=80=9D and =E2=80=9Ctype=E2=80=9D. =C2=A0(Ju= st as when you transcribe classical definitions in a constructive setting, = you sometimes want to read =E2=80=9Cpredicate=E2=80=9D just as =E2=80=9Cpre= dicate=E2=80=9D and other times as =E2=80=9Cdecidable predicate=E2=80=9D = =E2=80=94 all predicates are decidable classically, but that doesn=E2=80=99= t mean that their constructive transcription should include =E2=80=9Cdecida= ble=E2=80=9D by default.)

=E2=80=93p.
<= /div>

--
You received this message because you are subscribed to the Google Groups &= quot;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 http= s://groups.google.com/d/optout.
--000000000000815318057a13ec5e--