From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-vk1-xa3c.google.com (mail-vk1-xa3c.google.com [IPv6:2607:f8b0:4864:20::a3c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 6a2db8f2 for ; Thu, 18 Jul 2019 12:21:38 +0000 (UTC) Received: by mail-vk1-xa3c.google.com with SMTP id u202sf12520634vku.5 for ; Thu, 18 Jul 2019 05:21:38 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1563452497; cv=pass; d=google.com; s=arc-20160816; b=lb63rBAhqjUTDwqeb0Q5bAECxLKK7r3kMSEHgTZs5do0blYmJRP9LEX9g6ZW5icgvJ Q8APEyPIfwAhoRmRcvdvSjGwwWdq+P18C2UFAHnSAWITVAQL8PK3SScOzy/DV/9S1Vg9 Hhryo6jUWD7tybQyYtHnbGdjmIrXL1SrE6rTBpjH2a4K7rL44Id0RLL+9/zREXwbzj7J ot9h6R+Yd2dkyj0Tu9+5ugtbqbz4s1/vEKbT+L8WejYXp890nzco68/6tgK7XqnyD61X hc3aIePtXAPE4vShV9RRUPTie10Ui10aYkkwQVdbrxCmpldw8qZV9moDxssYyAYWBw0L FTQw== 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; bh=IQWzGBQdHJPn8AuA1X8WUkLlOVDPVP26LOYcffyd2E0=; b=vktG2LEZ5vHjLhyr0cv1XKOZVMDhSkgNgW+451JEqHCoVA0S0RhvwaIAd0vPpfSTbb BUotYX25h2BYsHei4Kly7R+GV7SOPJvzHxaPSKlf6wPFOw+ErlrpSii1ujN7AjD/L2Pz kizahF4Llw1E0SkpilUhtUF1V0I20HwCS/Zo7FJABj/Ei933OZsYQuGCXqb/oJO/XqSv oIf+t71RRPI8Hxu3XRwIUfkR4OENaW932PX3V9Oaz336gtMXRS5rMu9woffxBLxr4nsU zs8g8cdbN6I2HUdLodgIB/cj5f4N7NMNGuavSqaXs5Li9312Zyq4TENZeOGvgulCQnpk NVdA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b="0QX27/YC"; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2b as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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=IQWzGBQdHJPn8AuA1X8WUkLlOVDPVP26LOYcffyd2E0=; b=Q8dTRw2tbwEYf7Q6Mbr/rBGqqzSwdTIq0/whLRhzRTp2NVoupXjKOs63OqsW/YG3Rg mG8ujPeRdFvbnLKrhCIzD3s7Uy6L0WWYMvb6aQoExiUunv17hZ1fJ8iCcyo9/lrv98Du BU2ro3/tm4l/LQVXV4pNqxIeY6eAaEEUYnqkNV8A9tfDTrbS1R7H739S4SGO1+HQ+ILi xf9WWGV1SSuKLiiCy+i1UXO8Bq63APfFDqma6X6mk9HfpkZ7vlsI0XsNMmb2hP/DccM+ nWopRP4nYCliANHGBs9U90fTovbHHeAp5GIlX7QSAXKWP4DOJKdDosYFAZGgYKY2mah1 X4tw== 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=IQWzGBQdHJPn8AuA1X8WUkLlOVDPVP26LOYcffyd2E0=; b=bVTOyWAhoUgS+jgcDJsgWWoG7tSFvXo3d8Qqlukr5Ej2tKWQyw63sERm2Ccpf+w//7 cTCggMsstv5fSS564qlwkdBPD/4vFbrCpjvOWfPDXb8RxRGwcVe4zjdnouhcdepnPd9S 0OG6CNiU7hNOBM2t+yr4QcyRRQvplB73ySmuUXDfvSDMA3DTtyYPFT23kc8g4dMYKm93 HHWfyzGtYoqMCksAQHXWc7tbM0DEXa5EiuovpNB76ysrQ0pOBCzhZ8FnhlRISGVtrgo6 gVt0c+2SnCJREsaWKdJl55t1Vmq/fQrFznMcwurLBFYrdgJH6mNARS9x70ksYqgcmIhI yUEw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXET95LxFvuGzkKpDPQX44bUfUzUMc/Y+jwfHT/Vs5nNg/R3nyv PMvAui4lLUo1Cp/vE+GdWUU= X-Google-Smtp-Source: APXvYqzeCQmGGgvM2ynzkfvk8NPL/G+vkIf4ca0LR83mznu+wE6Jl4ueXBc9FvVCoVh0WDyS6EWLbg== X-Received: by 2002:a67:f116:: with SMTP id n22mr3691915vsk.73.1563452497478; Thu, 18 Jul 2019 05:21:37 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1f:9dc9:: with SMTP id g192ls951869vke.1.gmail; Thu, 18 Jul 2019 05:21:37 -0700 (PDT) X-Received: by 2002:a1f:acc5:: with SMTP id v188mr18135431vke.16.1563452497052; Thu, 18 Jul 2019 05:21:37 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1563452497; cv=none; d=google.com; s=arc-20160816; b=PJELyq2SsR7zZ8IfLHEBGvyOd42qqCAgQgdsJDuwribH6182U5Bi8b07kQsuFJ1BGH qW9+ar9KED/VOVXPbB+Ig1SyXIKusTPxhi9bsBo/bvPEbaO4HbQ17wzpBherTzyUYLW/ uriOzyjHg075qE3vexe7SOLXXaFaKM0UHt46Yi3G0X+x9zvEbJ/8ThnZP2jhdLCQIUl7 v3IKqRafanhtjiLe3u+1eEMU6waqh3vQK5HUM9zKAyUzCfgcNjCPIEpj21Xd6HcQmEwq K8VPkh8JIPdxSe9eIQzaMSFzc8PTh8DGKs6Q/31aRcGMTE+iLdwQa0yid8JNKEgoi26L 5Nbw== 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=/SgrtdB+Ug9pPby9EbEuvIJiQ+/Nsh1XzN1bz4BrjRo=; b=WiYqCytJXrlxdOfTCeAmFdmqMcuN24TPqblcbZ3z63Trf06/yUfafIYIdAiXHr6F0B +c9KMA3xgLMVfg8384dB6oiE+r5JvCRIRJj3w4MGp7ov004ch/mJ9wIL1T6Qkf+yS9fT lyumX5oNTyNv2CFEDhOn6jtYiXFGH0gp/3CZyY/98abGxylTLV3YLUm0AAV2SyS+dluk ABkstOLxZ9+t5LNZsbEYLdjb1sBNQqSA5sy2x/m5ehmYOBaZXE6Qeut4d/AtSHXsGNxr XL2Dnc3GXKCJ1REV1I070AGb5qO9x9ObsYw+5bg6pwh0KGXno4Glk6cZkMRoIMmNE5Ph shLQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b="0QX27/YC"; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2b as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb2b.google.com (mail-yb1-xb2b.google.com. [2607:f8b0:4864:20::b2b]) by gmr-mx.google.com with ESMTPS id d8si1291860uam.0.2019.07.18.05.21.37 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 18 Jul 2019 05:21:37 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2b as permitted sender) client-ip=2607:f8b0:4864:20::b2b; Received: by mail-yb1-xb2b.google.com with SMTP id a14so11112169ybm.11 for ; Thu, 18 Jul 2019 05:21:37 -0700 (PDT) X-Received: by 2002:a25:a366:: with SMTP id d93mr27970810ybi.256.1563452496506; Thu, 18 Jul 2019 05:21:36 -0700 (PDT) Received: from mail-yb1-f173.google.com (mail-yb1-f173.google.com. [209.85.219.173]) by smtp.gmail.com with ESMTPSA id v144sm6382669ywv.17.2019.07.18.05.21.35 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 18 Jul 2019 05:21:35 -0700 (PDT) Received: by mail-yb1-f173.google.com with SMTP id f195so11121853ybg.9 for ; Thu, 18 Jul 2019 05:21:35 -0700 (PDT) X-Received: by 2002:a25:2cd5:: with SMTP id s204mr29462137ybs.269.1563452495084; Thu, 18 Jul 2019 05:21:35 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Michael Shulman Date: Thu, 18 Jul 2019 05:21:23 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Papers on constructive simplicial homotopy theory To: Nicola Gambino Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b="0QX27/YC"; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2b as permitted sender) smtp.mailfrom=shulman@sandiego.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: , For something that ought to work in the internal language of a category with finite limits, like the first paper on weak model categories, it should technically suffice to have Sigma- and Id-types with UIP (since those are a version of that internal language). If we wanted to internalize more of the abusive external statements like "f is an acyclic fibration if it has right lifting for every cofibration", it should be enough to add Pi-types and a universe. To enhance this to the internal language of an elementary (predicative) 1-topos with NNO or an analogue of CZF, coproducts, propositional truncations, pushouts, and a natural numbers type should be enough. I'm very curious to hear where propositional truncations and pushouts are used (if ever), since in so many places the "for all x, exists y" is actually an untruncated Sigma. Certainly pushouts appear in the small object argument, but I wonder whether those pushouts could be implemented with coproducts in the case when they are pushouts of cofibrations that are sufficiently "complemented inclusions" (the pushout of A -> X along a complemented inclusion A -> A+B is just X+B). On Thu, Jul 18, 2019 at 12:55 AM Nicola Gambino wro= te: > > Dear Mike, > > On 17 Jul 2019, at 18:56, Michael Shulman wrote: > > Most of these papers describe the situation with phrases like "we are > working in the internal language of a category with finite limits" or > an elementary topos with NNO, or in CZF, and by an "abuse of language" > we interpret "for all x there exists a y" as referring to the giving > of a function assigning a y to each x. But wouldn't it be more > precise and less abusive to just work in dependent type theory with > Sigma and Id types, and sometimes Pi and Nat, and use the untruncated > propositions-as-types logic where "for all x there exists a y" > literally means Pi(x) Sigma(y) and therefore (by the "type-theoretic > principle of non-choice") automatically induces a function assigning a > y to each x? That would also allow asking and answering the question > > of how much UIP is required -- do these model structures exist in > HoTT? > > > Thank you for your email. > > Your suggestion of working in a dependent type theory is interesting. I a= m not sure what kind of dependent type theory would be sufficient to develo= p these papers and what would be the best approach to the formalization (e.= g. via sets-as-hsets or via sets-as-setoids). > > Regarding the dependent type theory, apart from basic rules, I guess one = would need: > > - some extensionality, > - propositional truncations, > - pushouts, > - some inductive types (for the instances of the small object argument) > - at least one universe (cf. quantification over all Kan complexes). > > One could then keep track explicitly of which existential quantifies are = to be left untruncated and which ones can be truncated, and then see if eve= rything can be done in HoTT. > > Is this the kind of thing you had in mind? > > Another approach to avoiding the abuse of language, suggested by Andre=E2= =80=99 Joyal, is to develop a theory of =E2=80=9Csplit=E2=80=9D weak factor= isation systems, i.e. weak factorisation systems in which one has a given c= hoice of fillers, and work with them. This would be a variant of the theory= of algebraic weak factorisation systems. We are working on that. > > With best wishes, > Nicola > > PS The first link in my email was incorrect. Simon Henry=E2=80=99s paper = "Weak model categories in classical and constructive mathematics=E2=80=9D i= s available at https://arxiv.org/abs/1807.02650. > > > > > > Dr Nicola Gambino > Associate Professor in Pure Mathematics > School of Mathematics, University of Leeds > http://www1.maths.leeds.ac.uk/~pmtng/ > > > > > -- > 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. > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/D49A1FEA-4CE1-448F-97A8-46065AF9E7B6%40leeds.ac.uk. > 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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAOvivQySjeDQXj_wWt9m1oQbAJj0%2BDn-NQ0yBX__DO1N3NBC_g%40= mail.gmail.com. For more options, visit https://groups.google.com/d/optout.