From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBC34PP4V6YCBBOFRRPPQKGQEX2KAQ7Q@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-ot1-x339.google.com (mail-ot1-x339.google.com [IPv6:2607:f8b0:4864:20::339]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 1c07d067 for ; Wed, 7 Nov 2018 12:21:13 +0000 (UTC) Received: by mail-ot1-x339.google.com with SMTP id g2sf10775539otb.5 for ; Wed, 07 Nov 2018 04:21:13 -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=ttNkrk13Ho5EyWf/1RTgBSV63fR1KKShU04L5OvN1sQ=; b=rOwEsa8GvzI3EwJzo15Ehhso7qQvqZyQ3+Pyaaf45w5zsfcxo0M3Ld3u11C2sIOcVJ yXqYc/NlGF9mEUmZqc8Ar3g+k19cvEgnHAL3Vgv3l8a4AQbh3NxW/JOY91MdWmDzBfcz CDsQ6UOXi/E8f0be3Qtf++2fl/NkghQ4RcNPZP/DwFpcxwkQ0ecKWGm/B0BUzwqbdY7b Xavb66HbXIwUCN2owubyLn021s4PRnmkMUClLbGZGRST91lgZrQ5Cj0A4PBS7oEZrTUJ 2sSRTRkAPN2BunaRGVPtx9ANRrkifHeVd7nB288xtQS6wDjrghcmly0BAmsowCPQCRxo gTDw== 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=ttNkrk13Ho5EyWf/1RTgBSV63fR1KKShU04L5OvN1sQ=; b=mn4dTNGT+f+Cnqb1+Sv8/cyQ/9PjaQUKVhheqT4aMJ1WUpWJEAL1P//YZDn6GR7ALB 4wjkKJHIE8O1/J3G+OS+LM7Wqi6srIigpLPSKc4t2dXc0HGwL0gRZ9Q8J2neuTiF8jB8 LiSS1pYwwb/884moSK/V1A4dwq5M++1GKk3f899XvbkKYp/T1kR+cgtFQ6BUkIswCcCG sUazx8cFPM7TQou0A3mUurtOOA8eB1c/B5Gk+xHCqEgAOUMtwrKMkMwH4kxHvo1jRRoP p2Owv3anHe0qLvd+siYeydm+wzBBCjPIRQd8jNRixwegFl04hWbqGvlD+rECgUgWPa7C o8gQ== 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=ttNkrk13Ho5EyWf/1RTgBSV63fR1KKShU04L5OvN1sQ=; b=HfNDjZh6Xg/NPkS9833H7s4dCTSGOgsM7IuPGFk/yU9anaSUBZyzIdvTIW41kZfrsM w1Uy78MWFCZ7P8HiE0jyjg5GYbC0XsUSMXuBTJgm6s8pRxMGHvJmqJ2tZqy4/7ocHmcr 71B0EA4qXZq4UIAZhwbWAEscfCE/h7uRw8xBCV+49mCO35jJctJA1T3XqvzjOIhT38Zl uvtLM3/5yvi169mZ+KFrzvdWLc6dXWOEW7HDuUPAx1FTOnTnVeXGmiKMObJ7g2LTlYU8 aQ6aPCGOBDCsjdVzyXwnzsO0pLDnZxlox6wgnMpfprZZc6re8x4TrZ00KoKIS/j16M9S XqBQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gLTBe6jCzLqrVmbk/bSozXZDCPHVD2LE2G4AVShKNwNcIgHEfVR tvg7G3y/54t7HSCnxq6dW2Q= X-Google-Smtp-Source: AJdET5dRD42N8liyRv7itRkfx73LUbZN0dyIBfZX/Oj1OqSMWhS940eMqOIoYr32YtluOGqGZbJIcA== X-Received: by 2002:a9d:24c3:: with SMTP id z61mr34179ota.1.1541593272918; Wed, 07 Nov 2018 04:21:12 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:3e8a:: with SMTP id l132-v6ls1043832oia.7.gmail; Wed, 07 Nov 2018 04:21:12 -0800 (PST) X-Received: by 2002:aca:5803:: with SMTP id m3-v6mr36802oib.4.1541593272223; Wed, 07 Nov 2018 04:21:12 -0800 (PST) Date: Wed, 7 Nov 2018 04:21:11 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <795a64b4-f62d-4fd5-9503-20c997b7b42e@googlegroups.com> In-Reply-To: <8fffa0be-9bf3-8a7c-ad75-ae2249f2ebd3@math.su.se> 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> Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2974_28984965.1541593271662" X-Original-Sender: escardo.martin@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_2974_28984965.1541593271662 Content-Type: multipart/alternative; boundary="----=_Part_2975_31026131.1541593271662" ------=_Part_2975_31026131.1541593271662 Content-Type: text/plain; charset="UTF-8" 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 mathematics. We also have the Limited Principle of Omniscience. Both the Setoid Hell was created and LPO was named by Bishop. Perhaps this is justified by his very own name. But seriously, I would like to have the terminology for the various types of categories settled and agreed among ourselves. I agree with the mathematical argument given by Ulrik. I sympathize with Peter's argument, which tries to avoid confusion, but I think in the long term it may cause even more confusion. Maybe Ulrik's remarks should be added to the HoTT Book and blogged at https://homotopytypetheory.org/blog/ Martin -- 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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_2975_31026131.1541593271662 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable


On Wednesday, 7 November 2018 12:03:31 UTC, palmgr= en wrote:
Setoid hell? This so= unds like a sermon ... :-)=C2=A0=C2=A0

= This theological aspect seems to be an attribute of constructive mathematic= s. We also have the Limited Principle of Omniscience. Both the Setoid Hell = was created and LPO was named by Bishop.=C2=A0 Perhaps this is justified by= his very own name.

But seriously, I would like to= have the terminology for the various types of categories settled and agree= d among ourselves. I agree with the mathematical argument given by Ulrik. I= sympathize with Peter's argument, which tries to avoid confusion, but = I think in the long term it may cause even more confusion. Maybe Ulrik'= s remarks should be added to the HoTT Book and blogged at=C2=A0=C2=A0https:= //homotopytypetheory.org/blog/=C2=A0

Martin=C2=A0<= /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.
------=_Part_2975_31026131.1541593271662-- ------=_Part_2974_28984965.1541593271662--