From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 9528 invoked from network); 29 Apr 2021 02:23:31 -0000 Received: from mail-pf1-x43a.google.com (2607:f8b0:4864:20::43a) by inbox.vuxu.org with ESMTPUTF8; 29 Apr 2021 02:23:31 -0000 Received: by mail-pf1-x43a.google.com with SMTP id s23-20020a056a001c57b029026369efe398sf17256678pfw.2 for ; Wed, 28 Apr 2021 19:23:31 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1619663009; cv=pass; d=google.com; s=arc-20160816; b=C4eQyqLcos/bJiTRjb+/YvTrXM08V0ZD3PJPsG+rCZj06NX6+fhdKkbrOVRkEJ4k1B 8lpEr0+3JyI/MWNKqA+rgZ+52HqDyWWJxkv4IfnqmTDbUpapaj8eeWWYU+5smqdBpSCN Dic2pHLf8GliehwL2kyLRdNAVvZkTRW0tczfe/g1LsmrYTaoMaiDZkMN/4qIQUKCM0+B hkqCHtIa11JIZ1BM4OMjDbM1YACapowBscRmA2F10NZvu80q0Q7vmR7vkrNP2aiqapEz vqtaKZXwZ30rjnPddAWnd55XuDjLxuzqIYW84hglc+PlCePjqVNhhyYFKvJeALfGPbWk OGWQ== 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:to:cc:date:message-id:subject:mime-version :content-transfer-encoding:from:sender:dkim-signature; bh=0zHZH8jVeNmCO3TXHdiUwGxU6snFoD48gpxHlF6w+58=; b=zwKQZnU+SJC7vDO1BilXU+8YHxUPb6ZjoOgprQkqVdBMLhE6r4tGaNbdKmkN0ml+rS /64uWCAwLRZIjn/XhHR5v4glhtj1ML7hVenXK1El/jtEqY/HAR4uknLuFz4emk5VdEPp zEyxmA5X+OPnz2/MzQN7HZY8eM1BaFFav+U97A+j48oV4zr1FQQRp6Hxp/VyJgsAyCu0 hOhr+qc8dapw6mLXaJcdLM4PKX0WWXaU+ZMAyaxXwiVH4wxBlq1ZFL0a69xzji9d9UlO 2xJA2bkc8ZLqqvB/v9hVr1YLEygxuYsAEoGRfGvPjxueXGbxmei8YuMeoNG2m4/pZ2u6 b/yw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=vU+E9IYe; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::72d as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:content-transfer-encoding:mime-version:subject :message-id:date:cc:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=0zHZH8jVeNmCO3TXHdiUwGxU6snFoD48gpxHlF6w+58=; b=mnEL2WPmYolJ2ubReu0UkONKBCgc5LpzrfSSRw+9ZqpSMDtWhs6RAsgFKB3IcSTecN dqI0Nv6ej4ss29RGRuqfIeyrHj/L3NxRuyLMwZ7TjI2qKxEb5lzPtAGMA2W3t+McWoB2 8as/L11LiBqK7Y/ywDQXhOkwMy2ytkSvbJsMSYmC/RaL1a/TJrorWbrTeVCC9VW+U2jy hy9s2xHf4GRw+3taDH4Db+ROA/mUSCWqRdFO+f0o+Oj5jTyRXgOOVdwfTnfqrjE81qnW mFqI9WKbVPJep7nlFAegoKWyxyE5X3ejfHK62D40u0cGNZtMAcxpDaOx5aCHDNLP7huq HbIA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:content-transfer-encoding :mime-version:subject:message-id:date:cc:to: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=0zHZH8jVeNmCO3TXHdiUwGxU6snFoD48gpxHlF6w+58=; b=kXCKt+fvQYyd9oUD3+VVZUufC9cIkmQ3U8f814d8N5XE4ADVCXiW3Ka0gpBd+i4Bt+ Ds/JaBdB8uRKllAVj9ZRD7k6Yr3wcH6bYiEBHwEsPH//HverGrnvI4oMSkl8pNN49Z0R Oe5Gajhad9OmkikHHXlnjozlsZKj/8w5n2EKCXRvwP0br3ntHEG9VnjW26kNz03vUMAb QQaxjYKCGVLu5vNGmvF0x4Ur5hmZGIDHF62lr8W0ikZiYeThiJm+uecJgC9SRfXTHdsq mChoN7igKWUhC8PDKo+I+egbewLxOsDIzxcz/3vS450zpVKAeO6QNRA/MZ3e3oZTsUBv yByQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM530O5hTDZ31TsoGCGQOHuc1j8NFmOCYKg0MBu++uzCJSb9Oobmie VKhUx4b5fHiVYwaEI0Tk4jo= X-Google-Smtp-Source: ABdhPJxPUUAJgFY4hEZVjiT0hhzrunzVjoznBLR98g6NbHiEnwXoPBM9lCeyoMU3MXCVq4AEiDH67Q== X-Received: by 2002:a17:90a:6e45:: with SMTP id s5mr7159152pjm.125.1619663009188; Wed, 28 Apr 2021 19:23:29 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:144:: with SMTP id 62ls823466plb.11.gmail; Wed, 28 Apr 2021 19:23:28 -0700 (PDT) X-Received: by 2002:a17:90a:c7d4:: with SMTP id gf20mr26306299pjb.106.1619663008337; Wed, 28 Apr 2021 19:23:28 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1619663008; cv=none; d=google.com; s=arc-20160816; b=u8N+tRGwcTKNG6WvKeBxsEY9dnmpbtepGQuSH13hEcq7OemJe44ITT/by3ZOrp7410 4SEHYa0a+g0uumOfdZJD181G4LqeO645nUsCftNyaKFZUEC1HUxLedid2ZrlITbAw70O KN9Y/R5zdb+4qgUwdhzFGoKCNzpkn+IbThbDGp5J9Qyw3xuwM5TycK5wkhhnLRyCfyiC eqduYKMavgI9w267+AZDqRpiYb2dhEHwc42rtkWv61w8AxkF3hareUSERqijLfKonmL3 xLWjy8VWeZ9G0q67hvSCiM3qFCQE1gMQ13+1Avk71BO7twu8j/7quKL/0NB6pGl3PE2w 4Mxg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:cc:date:message-id:subject:mime-version :content-transfer-encoding:from:dkim-signature; bh=co02K9xkdZ4RwuHeDaqSKKDQW4zCmrKJ9RiO8RoauaA=; b=i417ZgkB8Cw4UjsRmlFjSdmorvmkufG3CV6d/xmxG9X5kLV2qBXv0nyJ5J+oK1ioKT o1nWdkTA1lsA+Jy6MBK985PxDt3jz4H8ZXJtaPp4HsPRs4f70SBGewDEbaF5S6/bkt0V 0OX1vSWZ8WHcAjByv1QJlv/Di0I/dNp5y2pywGUciTttQK6ik9MP0zntVLip8DK5cYJ2 ykO9bb+1nkzosr+hUcb+ZMvlV2wLNd93YHBwVTMkfp+RmSY4jmcstdKWN3LHoT3Hdhj5 PcVCnVHh/RYeFCTgw9FntPsickCANYZJzj57Bvc345f05kUBnZ9L5NqGDojApFzfAzRu MQUA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=vU+E9IYe; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::72d as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: from mail-qk1-x72d.google.com (mail-qk1-x72d.google.com. [2607:f8b0:4864:20::72d]) by gmr-mx.google.com with ESMTPS id p18si201048pgi.3.2021.04.28.19.23.28 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 28 Apr 2021 19:23:28 -0700 (PDT) Received-SPF: pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::72d as permitted sender) client-ip=2607:f8b0:4864:20::72d; Received: by mail-qk1-x72d.google.com with SMTP id k127so10217223qkc.6 for ; Wed, 28 Apr 2021 19:23:28 -0700 (PDT) X-Received: by 2002:a37:f509:: with SMTP id l9mr32358592qkk.172.1619663007765; Wed, 28 Apr 2021 19:23:27 -0700 (PDT) Received: from [192.168.1.143] (pool-71-112-154-2.pitbpa.fios.verizon.net. [71.112.154.2]) by smtp.gmail.com with ESMTPSA id m124sm1264480qkc.70.2021.04.28.19.23.27 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Wed, 28 Apr 2021 19:23:27 -0700 (PDT) From: Steve Awodey Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Mime-Version: 1.0 (Mac OS X Mail 11.5 \(3445.9.7\)) Subject: =?UTF-8?Q?=5BHoTT=5D_Bohemian_L=26P_Caf=C3=A9=3A_Michael_Shulman=2C_May_4?= Message-Id: Date: Wed, 28 Apr 2021 22:23:26 -0400 Cc: Ivan Di Liberti To: Homotopy Type Theory , categories net X-Mailer: Apple Mail (2.3445.9.7) X-Original-Sender: awodey@cmu.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=vU+E9IYe; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::72d as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu 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: , ~~~ Bohemian Logical & Philosophical Caf=C3=A9 ~~~ Speaker: Michael Shulman Title: The derivator of setoids. May 4 at 16.00 Prague time (GMT+1) The zoom link is on the page: https://bohemianlpc.github.io Abstract: Can homotopy theory be developed in constructive mathematics, or even in ZF= set theory without the axiom of choice? Recent work inspired by homotopy t= ype theory has yielded two constructive homotopy theories (simplicial sets = and equivariant cubical sets) that are classically equivalent to that of sp= aces, but it is unknown if they are constructively equivalent to each other= . If they are not, then which one is correct? Or are they both correct, or = both incorrect? What do these questions even mean? I will propose one criterion for the correctness of a constructive homotopy= theory of spaces: as a derivator, it should be the free cocompletion of a = point. (A derivator is an enhancement of the homotopy category that remains= 1-categorical, but can still express universal properties of this sort.) T= hen I will give some evidence that any such homotopy theory must have the c= urious property that its 1-truncation contains, not only sets, but also set= oids. Specifically, the ex/lex completion of the category of sets defines a= derivator that satisfies a relative version of the aforementioned universa= l property; thus it should be a localization of any derivator satisfying th= e absolute condition. This suggests that either setoids are an unavoidable = aspect of constructive homotopy theory, or the criterion needs to be modifi= ed. --=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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/BEDBD6A8-A6FB-436F-AB1E-45162A257848%40cmu.edu.