From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCQ657FO5MEBB3GZRPPQKGQE43DNGFI@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-oi1-x23e.google.com (mail-oi1-x23e.google.com [IPv6:2607:f8b0:4864:20::23e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 8d86aa21 for ; Wed, 7 Nov 2018 13:47:26 +0000 (UTC) Received: by mail-oi1-x23e.google.com with SMTP id b11-v6sf10874577oii.19 for ; Wed, 07 Nov 2018 05:47:25 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=wytCR6MPyNM0i9VY7gcAgggBathOhqEX/Ubv2K6JH+M=; b=jEBmrBidxD3QOPiUWwirtFb0jWiy3yuTdO4LUCxHEDmhTn+s/jX1fqwkhLAXRAPTI4 RyorENQ3l5kHk/uMCT/4yrh+gkiLgjClqo3NE4ejOQY9QWFV55jsYdHWD/q9cMtDacLT Zibvd+NPefJLAiOSbrfv6eapsoA0U7Efgb7nXBCzTrfVLUUH2hz75k4z3HceuZp7w7bw x6ABBSJdm6tQQbKDLLcupjH5O3rLYZzZlRuFYJwjtIcseYhcdEWvuB6jWv7BSCb/x99p /in7iE6NRpPUlL0TTcWKm4goyxI4ZFYKBWOhth6Yx/wOR5bkZw+NQk7UwIMUvfdCSlOX ghnA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=wytCR6MPyNM0i9VY7gcAgggBathOhqEX/Ubv2K6JH+M=; b=Z2DlFWg2duDBE+flplTY+xi9ylUtxEvoHGimVQl9wg9m/VGTip4c/xMhkA6dGuHk2d +2bdUMa+TUACCZxlE7LK9mr0iznCk8CJSQWeP/Wkd6WfW7sgCJJ+hyShWD2vis+YwLuu OHB5t4CGA1LMoW9dIz7F2X3nH1X1CDG9mEs+RXKC2/LKqzZDrQ6AoeS/S0U0Uc95Jtg0 CW6KvLDJPnF+7rg5jrdJK69G2WnjSaWmHIm0npWUWjXVFT2kDO15jTlopoAYKEGtE3cQ F6VEohZ9VhaDbydmIwJ1RKQaQXKR06TsNDluySKJlAOFPPj89OnYxPTVsKk0iNKYQoJ/ VHSw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=wytCR6MPyNM0i9VY7gcAgggBathOhqEX/Ubv2K6JH+M=; b=Htq3fw3WBZppAxzL32m0ayXpreMDwQ+NycevruZlaJguaxGr/feb7/t1RilISitz4V qPgAWaxar4Mw/VFDj6w2IF/5tUnoKzgPowYrUJnidQ1UdW5UP4fD0JYyfpybamo4ZQ1B 6DDnvqDGthYfcq/rwug1Yb0ZgGaEhePgmrsCX98lyfymZHGCMqf1Gm0ez0Au9LStuEgy 7P222MyJJpRS5faCHH/CpIESoUCIWjglrM+m9UJfvT/Zb00C+uE6VBKUYc+9f4qpv+/v oNUls1n0yetFKbP9Ad4WqswYnRn3+LG1aog2rEcBxMTRGRyfviNiRxpOMU3R9Z9w+12s VoAg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gJSiTUtnEwZK2YXTCMACj7G3P3BaOgubzFqgMLGoy/tGH/9VRco RJdczliDkHa2gksLJfQtebk= X-Google-Smtp-Source: AJdET5fo+wEgGjFyGyq1JSMK8kK/h6mF+JOuztc3CUOnmFlPV7jaHsSl5ZfbFNNvyzJIZH0i0YqeVA== X-Received: by 2002:a9d:3d06:: with SMTP id a6mr4031otc.0.1541598444632; Wed, 07 Nov 2018 05:47:24 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:308d:: with SMTP id s13ls6843272otc.16.gmail; Wed, 07 Nov 2018 05:47:24 -0800 (PST) X-Received: by 2002:a9d:24c3:: with SMTP id z61mr3894ota.1.1541598444029; Wed, 07 Nov 2018 05:47:24 -0800 (PST) Date: Wed, 7 Nov 2018 05:47:23 -0800 (PST) From: Ali Caglayan To: Homotopy Type Theory Message-Id: <9c59c31d-3277-4dea-ad28-5679612529cf@googlegroups.com> In-Reply-To: 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> Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2923_674965728.1541598443509" X-Original-Sender: alizter@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: , ------=_Part_2923_674965728.1541598443509 Content-Type: multipart/alternative; boundary="----=_Part_2924_18271654.1541598443509" ------=_Part_2924_18271654.1541598443509 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I wrote the "category theory in HoTT" articles on the wiki. They are=20 nothing more than what is already in the book. Part of the reason for this= =20 question is to make sure there is some agreement on what I am writing.=20 On Wednesday, 7 November 2018 13:03:03 UTC, Bas Spitters wrote: > > We also have a wiki of course:=20 > https://ncatlab.org/homotopytypetheory/show/HomePage=20 > On Wed, Nov 7, 2018 at 1:21 PM Mart=C3=ADn H=C3=B6tzel Escard=C3=B3=20 > > wrote:=20 > >=20 > >=20 > >=20 > > On Wednesday, 7 November 2018 12:03:31 UTC, palmgren wrote:=20 > >>=20 > >> Setoid hell? This sounds like a sermon ... :-)=20 > >=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. Perhaps this is=20 > justified by his very own name.=20 > >=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 argument,= =20 > which tries to avoid confusion, but I think in the long term it may cause= =20 > even more confusion. Maybe Ulrik's remarks should be added to the HoTT Bo= ok=20 > and blogged at https://homotopytypetheory.org/blog/=20 > >=20 > > Martin=20 > >=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, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_2924_18271654.1541598443509 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I wrote the "category theory in HoTT" articles o= n the wiki. They are nothing more than what is already in the book. Part of= the reason for this question is to make sure there is some agreement on wh= at I am writing.=C2=A0

On Wednesday, 7 November 2018 13:03:03 UTC, B= as Spitters wrote:
We also hav= e a wiki of course:
https://ncatlab.org/homotopytypetheory/show/HomePage
On Wed, Nov 7, 2018 at 1:21 PM Mart=C3=ADn H=C3=B6tzel Escard=C3=B3
<escardo...@gmail.com> wrote:
>
>
>
> On Wednesday, 7 November 2018 12:03:31 UTC, palmgren wrote:
>>
>> Setoid hell? This sounds like a sermon ... :-)
>
>
> This theological aspect seems to be an attribute of constructive m= athematics. We also have the Limited Principle of Omniscience. Both the Set= oid Hell was created and LPO was named by Bishop. =C2=A0Perhaps this is jus= tified by his very own name.
>
> But seriously, I would like to have the terminology for the variou= s types of categories settled and agreed among ourselves. I agree with the = mathematical argument given by Ulrik. I sympathize with Peter's argumen= t, which tries to avoid confusion, but I think in the long term it may caus= e even more confusion. Maybe Ulrik's remarks should be added to the HoT= T Book and blogged at =C2=A0https://homotopytyp= etheory.org/blog/
>
> Martin
>

--
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.
------=_Part_2924_18271654.1541598443509-- ------=_Part_2923_674965728.1541598443509--