From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBC7NZUPX2QPBBBWFRPPQKGQEB3INABY@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,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-io1-xd37.google.com (mail-io1-xd37.google.com [IPv6:2607:f8b0:4864:20::d37]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 4f9afe69 for ; Wed, 7 Nov 2018 13:03:04 +0000 (UTC) Received: by mail-io1-xd37.google.com with SMTP id w5-v6sf19517380ioj.3 for ; Wed, 07 Nov 2018 05:03:04 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541595783; cv=pass; d=google.com; s=arc-20160816; b=rjUCG4F9KWE1LKvGQcxrz12/VxvOJu9e8jxOLsbrEhLs/aBPyzdabN5vRaiM7zSUnE FMy6BsXF5SeqmXqXuUQi1YnAT06ZbDrhENYq7ZPJLIeHh/r/XqRQH91wrAxqG9OBNkSy luFJoBBEo3KHxwIw+RbcwGGtfYtij/zZj/vNnc+W7t09qy1zvymiyS67yAG6kNA3pxBc b3PM2uzAKU7vus5xaZwNCt74HxtYJxuAgnU+lP2rw3b0vBFbCKHSLHY1Jh8ALiYytCrV JVZQpR2E+Hf1FJ3E705lZkwMBxEH2JQ+p55Yh6V504f5u0DYcfN7f2VCg5VqwCato8qL rpMg== 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:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature:dkim-signature; bh=vX35nguf5UPxK9VfHbNetCQVOP4QnoaHYCxkTzqn3ho=; b=S/Nfq+r8bEjybfODGPqJSzIfW1vcyibIOaQiQhb1wQgXlqDOznTANeC0B9W2+mwzmW vEdHBPqPsj4gzmlFiRP+HhslEq/bS2xTkcP0+xBWLaBHCZRvHHjN3WLPrVhOGDVyWVUA N9q9MKI7ZSMMd4n3RJras5cB4gHwwoDOprdKrUerg+AX2Bd/H3FDbcWN2gTApbIyrsdg Q6dk7I9bjq0tz+OLrz6gBbFdY/Z3MdxEFWTzHTbiyOW40y2shloXPo8vCbDP2F+aqJg6 6VKScAOVnod7SkstvhTNrjKDEJllde+lSpAIX8q3A8BWfpzGoxgZn7XaxWnRqmAS8kNj mzQA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=aXIwcEpa; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c43 as permitted sender) smtp.mailfrom=b.a.w.spitters@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:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=vX35nguf5UPxK9VfHbNetCQVOP4QnoaHYCxkTzqn3ho=; b=N4sX1S772UlwK8HeIZGSVrBXdFO3UIIcsEFKbvJbadrzF0DoieC7boXEnl3OHa9cf9 dOP/PtAWPMXv3OSVJYftRkTUJ2mfLrrVvX0I0lKiVAwKsZ2/2OfHjMnXpFVBNZYuzBWf nuQIHZPKUXxjB2P6rtslGRUcm42cTl6eQ8B3NGlAoOPJSAEhedPHGQRSaAjCbWyrNRZ7 cwvixYk1TyMEMKe/AymOhANNT89wIS3Y1xmg3/2p/lxMZDkmh7FFvYAPIF03Ar24EJxh IrZeGBd50ZzrNbyr0fWj12ufD4KrV+4qfp8LC+OG5sZv6AoBBEGjTR1XvKY0e1A2D6Ag cQzw== 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:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=vX35nguf5UPxK9VfHbNetCQVOP4QnoaHYCxkTzqn3ho=; b=S5XKK1MaflgSXPeqt7OO7UcbeJkRJtErl2qVafy0Ji5sikObTwSfLRI70UmDQaLgXk nYRMuZYfrCQfQ5d+51/6ZGX//+k2rQoJ2kUzHKBIDMsAGFyXIIrzckqhpnOus0LZviqb n+pSRMEVVmKwj2U1nbctMA/rcU2t7Mysn+etF2Pn2MpIAcNLJiOT681/AR+s0haCyd5Z N8a3XHWBfaU62UOv7SHYphkapHqnuKWtpqAalLTiSGG6E3ekFHQmkfUQRw9ajk4smxB0 bsCVFhW0aaFMbrKhkcWd/C0eo0JepoH0OLO4GATxMsEoA66D06udJEyUOfDsEVC016tj gOzw== 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: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=vX35nguf5UPxK9VfHbNetCQVOP4QnoaHYCxkTzqn3ho=; b=KldRT4jMaSaAEgDLJJEwShzw4iqO/ppMe0GaLgsLptm1PAcZf0+NkZhpyxhgjg8Aom XM+/uXvaIhAkYTCKw5kLWLf6Za5D9vaTJmlADuct9c796/iRCu+6rzh0YywV8i1YxYHy w3tXOvc6JTtKJ0XuIn+dIreebS/rwCDPG2C6rh6ff0ceqd7PpMVzT0m7pBRCQMW7BhhF SLGzFWPlE249jSq+HSVpOtr0sV1voynSwLibNI5+EEGyfi2c6V2U1+hV5+/K7O1lLF74 skncsjwfF+qD7TmsFh23h+Crscby7AmzszvTGHwpIq11T5Rm38d/Z6HZmFJrBgXtsIdp UMRQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gIf9ljd4sFYU9OL4v35FWafctmnHrQJwUG8Jeq35BgeWXsruTk7 +9yMxbdDVoeye/Ns9olVm20= X-Google-Smtp-Source: AJdET5fLobW5jxt9IaZeI+C+Pq50x4IBcIYhjEDr5XA8skWPB81YsCjqC51BCP/rUf225JNrP54doA== X-Received: by 2002:a02:2422:: with SMTP id f34-v6mr1108jaa.1.1541595782960; Wed, 07 Nov 2018 05:03:02 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5e:8917:: with SMTP id k23-v6ls10245031ioj.4.gmail; Wed, 07 Nov 2018 05:03:02 -0800 (PST) X-Received: by 2002:a6b:d80d:: with SMTP id y13-v6mr81614iob.23.1541595782576; Wed, 07 Nov 2018 05:03:02 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541595782; cv=none; d=google.com; s=arc-20160816; b=GE1pbN3C6kctjIKxvwUYBJbX2MVxpFL5rQd0+9H0vpRdmfpnwMQJvDRU02T59q6S5V VlYmR+gN+6CWDXVyAMl475AgNRFnhT4Rw5GFraV8s0TYjHF/qzMtcyPXBo2eUCm/Ikhj 1vcq3UL3sdtlqMPWQZEDogkqyOV3RvaestX3lgQgGPKsGOBiaGQ3nlazAJtFvj7LvotH u+JrdqPXcxQl3LYn29pzJZb+/uJDspNlnWmxHHxNFTDMeEzUOHFy5qKgr56jgZJHOJ0e ZLlOp5AeBf2wJGEZK4gybpRfKP2L9RT0B9jmcJL6dyhJ9aMJvFQtbWDGpSsOluh7prBA ztlQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=ysIBOwtZ6xl4J+ZjW6tEOSxoD8TRSByiK24sFUSgCzc=; b=K80NtcDusT/p7qSrcZv6usejIsVucnwv35MP2TVsuKzPRd+pWdP9vUQXY3KD8xhsVw nqU4SzrK4um4MZYWKSflmW9rqntqG4qcNzlcVhcaOPn8qh5+yNz2r5NhxTZ5eL2LCxl9 cB33PsD9cVnIRHlzljtWWthWQbEw+uLN127OVGkJJNut2Wjq3QOMr3JqjCkQpnbpY/lE 8B6vqDLmdxYHgFQ72373ezoHsPFtMkqpqnCNuXnAWUmwosknrJKcEPYd5o0AK3L6DT/5 shc/vEdwmpnNM9eYD5XCQLpLdT4BcIbHOar9r1aRlzBSNlSSQv56gynriCH/suil4GjV jNmw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=aXIwcEpa; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c43 as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-yw1-xc43.google.com (mail-yw1-xc43.google.com. [2607:f8b0:4864:20::c43]) by gmr-mx.google.com with ESMTPS id v6-v6si27550iop.0.2018.11.07.05.03.02 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Nov 2018 05:03:02 -0800 (PST) Received-SPF: pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c43 as permitted sender) client-ip=2607:f8b0:4864:20::c43; Received: by mail-yw1-xc43.google.com with SMTP id d126-v6so6538639ywa.5 for ; Wed, 07 Nov 2018 05:03:02 -0800 (PST) X-Received: by 2002:a0d:df95:: with SMTP id i143-v6mr90538ywe.349.1541595782303; Wed, 07 Nov 2018 05:03:02 -0800 (PST) MIME-Version: 1.0 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> In-Reply-To: <795a64b4-f62d-4fd5-9503-20c997b7b42e@googlegroups.com> From: Bas Spitters Date: Wed, 7 Nov 2018 14:02:50 +0100 Message-ID: Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories To: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Cc: homotopytypetheory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: b.a.w.spitters@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=aXIwcEpa; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c43 as permitted sender) smtp.mailfrom=b.a.w.spitters@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: , We also have 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 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 mathemat= ics. We also have the Limited Principle of Omniscience. Both the Setoid Hel= l was created and LPO was named by Bishop. Perhaps this is justified by hi= s 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 mathema= tical argument given by Ulrik. I sympathize with Peter's argument, which tr= ies 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 blog= ged 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. --=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.