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=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-pf1-x43b.google.com (mail-pf1-x43b.google.com [IPv6:2607:f8b0:4864:20::43b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 1a7ad863 for ; Thu, 18 Jul 2019 08:16:10 +0000 (UTC) Received: by mail-pf1-x43b.google.com with SMTP id 145sf16207144pfv.18 for ; Thu, 18 Jul 2019 01:16:09 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1563437768; cv=pass; d=google.com; s=arc-20160816; b=kD9IuSgiSrJtZlJJibqDyHGcVLOqL9x2ckxn1pOkY2IW7DPg5+OT+1UpZXsRxiL/WG 1HGCcBCd0c9MeoeNbZuLz+gM8kWIaELIwDMk9dznw40x6yzrR+qyWyfooDbfLD2/re5Z vCXzv+pdtvjpV8IQ9ErcFbuxjCXy8uBQS4wdIjzGObIp85smea21IM7XalPBRxzuUABc 3bP3+9a0inV7CQIPLojcdlGEQlbUEOCWIWPs8urI20FMAbJ7ja/g5+vO0HxK74Dyt3iG 6L70Kmxc4iHohchA0D4mc3R3+WVZSaT8wIgQoXVuORko3yYANCBdVo1G+rhST2+5AzJC o8Zw== 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=pITXLhR5pAqcV+sJvk1k9/5Bz1N4VPaxhWACfIBbEJM=; b=06vqME99rge4vb3yKx66ko93KRk5qXTDxGj9UtCaGSQsEqImJ73GOMaqYQfTXMSpTS W5P96PTnP845YB0aDvAHXiKdUiLiIYIasMdKywQeRGsA6u9xj+/idmL2N458yMHYG97S WYEc8lr44SxyLfpz/Z40lBpertKFHJxtG4y5ejC9TxLTT4zfyZZQkCaqf2AQhq9z8l1N On3KMjfo8QRt261/jq3cdnUjdHt6gEfgL1gnGdcHX0RHbDoSQIVaBb6iNm5B0HV96BYT DbRDD+wUK5F6zwuxCTvpWt6OmURSyV6DnuZvE+31P2I3ufX8FfITr2MpR5T0/KMlFe3z nXYQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=WeHNydKg; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b2f 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=pITXLhR5pAqcV+sJvk1k9/5Bz1N4VPaxhWACfIBbEJM=; b=Xw4qrCAX0Boz/Uw4GA6fzOkUhS9cYVAYyWsFe6LLLzS/pt+Nqfi1NnXh9Ht59FEj41 5SOLsZK949H0iw8p90Wf14kiFuK8FCR6OG3Msc0WFRgkMjTxFQTArnHlgT6rgEkCKaxY IHrTNfOvtsq0GF4vynwY84twbDHYuNqHWsiiIjnNhC19Sg/KvyheGALFHtlQNBuVfDaD 5gC90O+DwcblPLfK6ta4NeOW4LG4IfUEKIFdN4V1M4RLy5EHacbW2T1od2BAo694bQI/ cpDbuWPVmYeMJHzbD1graq1HIG6XA5zgh3q4hiDtRcAXnjNUB2uuVFDOlSY8eTV/U/qY zxZw== 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=pITXLhR5pAqcV+sJvk1k9/5Bz1N4VPaxhWACfIBbEJM=; b=Trc3h09wmSAYzrTWBXHs5du+qpjWBc9j3k+LnJjb5Kj1/B0GcDSRhHEax8x3lrSD1j Y+1iE8GodSh5YQrmC/qgqqaIymgkR1DIFff9ZRcKMg0vPvC68nUg5WZcjMCTMFq2KAxE ArGLbn/coFu6d5NvD+z1F8jW/PRi8O35IX9O7YwkvIMMrWxL+NNEoVMeOBbDqk2ifnrp TpbuIfzRirRFz68mnqZ+8ejyr08893KygRdzU1DPwtOsvlZAnOh72Tf9iKXyEISCa8lo /+l+Og9eV4lmEZo7X5RWcvRwUri3DpAg4WrLt4NxEaJf2eKy3+95ZRZvSSyW3hrueTuf Cuzw== 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=pITXLhR5pAqcV+sJvk1k9/5Bz1N4VPaxhWACfIBbEJM=; b=Kba737sQFvdsiP7itGH5xaGtyO7utK2CbZYSixU4xbXgxQvdU5W5wztltSqi1X8xIo +lgIaTMXYkR4WXpUqbYHdiYi3j+I/yfl/OzcaOXQdeesTGDs6RRABotYWefNmxYye3Ql 63y2H4cFyO7ok9+oXpQKqhxv5ERQSyFBa90XIkML52S2FVJ6HMqE+tR8eB1e3S+H8sRk eI0GJAujdk5X6bc3y4dwHuN8PCm63qb6D8jPZjGFx5K98r+FGdPAlO2vODTHPKLbjzme AhJWr7hMJB83c9g55Du6N4yBy6vZ3HsEKRl3S9Wwo8+HkBEGg5syOtz01UWaL/xDKGUM 9w9Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXZIgyQcY5vWyIDF5wnewEttfTDgc/kOyTpZVxrltq9Al0bNQMO YWrrND9wU1g/Vl5eqW2e0iE= X-Google-Smtp-Source: APXvYqxSgX3Qc3sAtDUwmC7k0QrsSD/qtQkST5I6u6DVMo63zwBV44i9o291UusndOVVAIXmQbDzkA== X-Received: by 2002:a17:90a:fe5:: with SMTP id 92mr50228951pjz.35.1563437768578; Thu, 18 Jul 2019 01:16:08 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:740a:: with SMTP id g10ls7320552pll.0.gmail; Thu, 18 Jul 2019 01:16:08 -0700 (PDT) X-Received: by 2002:a17:90a:5806:: with SMTP id h6mr48247304pji.126.1563437768147; Thu, 18 Jul 2019 01:16:08 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1563437768; cv=none; d=google.com; s=arc-20160816; b=wf2KCJK4xgUElbxISBFzYvmJm+HODsU/0xRHtnHoFZjmr/lm96u2vV952LNq+NOy46 KtWAoJJHgybnpzH4D7m4tNnor3DftqXdpjCvju+JfmA3ugm/DmTNS7uwIqk1ziOL0+CD Qd4CS2oK3xUNx41TjsreRpdkTbZ8i/EK4abl0EOyAFmf1zJCOhfiAM1BRoA1XvoR6gMo ROYK5Qnz//8MDViH3p2ujNE7TgKrJiti1hxsc7ZdYkchvBlU4ZZnLfq1Ow7Dk7STB2cg Fbq+tO0nMJGZPKy3nxJeMPmXrRXn23Ebn1yZDToxyK2U5NkMA+0Z90QwsIfqy5HXfiE0 pbkA== 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=Gfh/AUPNm1sAsVUbB2c2WHfQJ+hm92T6uneYXVquQ30=; b=HKaOHnRkPn7BEszSqojEVfLOQKaLRqjJFUqkMEn1gHiutPcdbCtaJMy5IGieRiP7D2 TQNFpOcjzJPFsx30OujCdQvDRmRebhq8Yw/KicQXAVrfTNZVB9soJhbGsuDa4NGb8H6r slMQHR/IfpqAfjHaTfTvXi7fXt6SUMtEK2EPN2iVERP9dkcEaDbH7wusLITLa/SFdZno Vo8yVrcPYjidgAYbEsde2GiBQE01becEILLzesuad1hgFeiUKN1bQyfD6Ap8y/hbAOMk WccJPtpDsxBpRIlGkMVOWOb/dNSd4p+IqtKF9rvIqQt1fhJBy3nX4GlQ3tUTa6l/yqYV ncUA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=WeHNydKg; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b2f 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-yb1-xb2f.google.com (mail-yb1-xb2f.google.com. [2607:f8b0:4864:20::b2f]) by gmr-mx.google.com with ESMTPS id 85si35570pgb.2.2019.07.18.01.16.08 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 18 Jul 2019 01:16:08 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b2f as permitted sender) client-ip=2607:f8b0:4864:20::b2f; Received: by mail-yb1-xb2f.google.com with SMTP id c202so9572014ybf.0 for ; Thu, 18 Jul 2019 01:16:08 -0700 (PDT) X-Received: by 2002:a25:b947:: with SMTP id s7mr28610754ybm.349.1563437767303; Thu, 18 Jul 2019 01:16:07 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Bas Spitters Date: Thu, 18 Jul 2019 10:15:55 +0200 Message-ID: Subject: Re: [HoTT] Papers on constructive simplicial homotopy theory To: Nicola Gambino Cc: Michael Shulman , Homotopy Type Theory 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=WeHNydKg; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b2f 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: , In our work on GCTT we used the internal DTT/DPL of a topos. https://arxiv.org/abs/1611.09263 (sec 4) There's a convenient presentation of this in the work of Phao (appendix 1) www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208/ and the elephant D4.3,4.4. It may not give you everything that you need, but it may be a start. On Thu, Jul 18, 2019 at 9:55 AM Nicola Gambino wrot= e: > > 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/CAOoPQuS3E%2BdK8FPigSd%2B6KDtk9bCnfrwLsbKBR_93h3WBL7jag%= 40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.