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-yw1-xc3e.google.com (mail-yw1-xc3e.google.com [IPv6:2607:f8b0:4864:20::c3e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 9e9eae03 for ; Wed, 17 Jul 2019 17:57:14 +0000 (UTC) Received: by mail-yw1-xc3e.google.com with SMTP id r67sf19200253ywg.7 for ; Wed, 17 Jul 2019 10:57:14 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1563386233; cv=pass; d=google.com; s=arc-20160816; b=Um97DetD+nXdF+mB0kBCc8Bluu3K7iGS9OVFawlr7lYtVUHAriMArqg38+IuZmdRW6 12IGyvEkAp4QcVZk3/ts14BqbBmnZe/ZWvLPhUXqBhOvH5d0iMPtxkUEjIRaXyTcDmdi B7Gd0J3nYANBSh2XrhUqQQ9EUepg+Z/PKlduguS6Y1q2Nv9sgNDnv65KBsFaEb27ynMo RT0Rr2VIeVc75A2fsG6gKmrLXez2BH+e9NnhPHb+9Kwr/GY9+AP3KFYEO1Q9iNWPlbWi IkPUudqKC5MYHGG7vsSqNqkvfXLRNfpZVaUxBTF99neHXapznwhVX4+aP/cmtqHrpMnF AWsA== 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:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature; bh=H2ryqqkIfCRJ1TlaNMZEtGZLwWhzBjtMwYg9KeBAWLc=; b=IWpJG/986CSyWZcQghqszMub4NYz6qX1HGtAiqBCLfxbjo58bVJhxgol2TrmXbA3cn nLnH7xwXTXd2JNWsfs3SjW2/uZAELfH1bQFfrkGmLTnD2hxmbew7DzovxVBPIPYj6GCY HDWwn6U7aZhe7o6Jcnv+d17Ey4xdn8oP+L69K/RKbXtcjMomOkn3FFUzj/4Ufx7vgU/o j4Ml78ntl9+BTCIW4Raxkhi0FM4mquownx5IAY5TZDvnU0N8TlKihKIFSI3LGd7nZ+hd P3czexEbEHndTNNQbdXO5ZGfSJ0aFU/YhtyIjkQebbvVyI3TEwwzAW9MAw9GfGzfb0UF Fc8g== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=nqu1V52Q; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c30 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:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=H2ryqqkIfCRJ1TlaNMZEtGZLwWhzBjtMwYg9KeBAWLc=; b=GdmHxdYCiRfJZ4lvJ1ki2bvzECvPNdOmOpip5DrmOIXWlXCg9TnB8LtUVIZHGtURfi CIv5bYItXYsK5YXcRkS2QFklF45HsmQ8zIlnWDadxYpBLjdfPAkLpvoSVt/qDwbY/s3x lHqaIlqj2mdEgzPlfjfPir8HunQ/jDZ9/F4pSaYk4UpuTbAYnOuYtAn2Y6e89ntI091P oz2W9Qmb+0O70jQjwsevNiOR0tiOTNXItg5NSqv5aBiQGEPlsb8PZWBGLCyZ5I40Mu6N bTxD6rtvmd6EU513buuxWeB/LxeVghN/ZeEmaqTUpsc3Szs8jnF0GCNroWrSj4qnVgaw YTgQ== 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: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=H2ryqqkIfCRJ1TlaNMZEtGZLwWhzBjtMwYg9KeBAWLc=; b=GS+pAHzqGotwc76HeKD+NMzrbnv00roYscTB35RA0PozdymcBpRugoLKRvW8RZf968 uo1utxOlwbycFsnN3UyWes+r9p9ZZZjVEAC7uW1hRuyi3cwbdSpQF+CjRdmsGRCf0UsU RO96tUDEqRIb++0CgwOoTxJBn34XKNsvI/hXJ/43822DgoTn9UVMroLTX4KCJY1G73cW mI8R5/XocfxlcFCg5BGT9fSliQ3eM0+kelSQzgHPhccoeAY2WF+giMueJvhx6bJl2pzy XakFYbO0adjKgAmCat0bfh5dUBGtIzkrC15uryuCEqTnSKPqjOGfvhwaP1Vs4Em7Xtbt 6EDA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUgwy4tF/dZxY0Lhd3KlVLFEDfJ8o2hXd2dYyLf/SsmKqjVl7iO KNa/xQNYTeigcEX/2e+7A8I= X-Google-Smtp-Source: APXvYqzqFwXd/joXBMe+zz0jLe112F4Yzls/nAJmyOWKDtNVDOWRVXO2vONjUo2L+/L+wFrjhz40HA== X-Received: by 2002:a5b:706:: with SMTP id g6mr24921560ybq.185.1563386232941; Wed, 17 Jul 2019 10:57:12 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:2393:: with SMTP id j141ls3303538ywj.11.gmail; Wed, 17 Jul 2019 10:57:12 -0700 (PDT) X-Received: by 2002:a0d:df50:: with SMTP id i77mr24647966ywe.59.1563386232616; Wed, 17 Jul 2019 10:57:12 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1563386232; cv=none; d=google.com; s=arc-20160816; b=0/7ZZBuLKbemn0KgSO542Wi3ilUpqHTF8hOumAYIEZFv9CvA7VxqUYlRRJKE8wuU9x DyJAmr1F7Rkrd+p/7sHNBHLxyVcVnOSQYt4WXQ0b0qI2hi+NDZwGLbPdhx4PoocQ4A16 Y39djAAhdQpuN8qnnMVZC4zGMW3+N7Irod3MZmFC5HJ0uDX71a003JyiKdIVed/wT8W0 S3191X2dKBHG/Tw8KG2mBnvSRXiT3f/HW7wfdeTmeOtF7gdP7C6UIPvfcC/W27XGp4gJ EA9Ms28TZyKyKYtHCTL4VAKdN7K2bpXA9+4FvevvuQJeF6MjjII8QbRVR3vsq2ZHxOJr vERA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=eSVBv88ihhFETDYadKSfxnmNT+prLtGKQkH9Fqk2a48=; b=RDYxlqoAvgGB1Jwe7VmBV2SHuJu+D6VSQnXU9QYWuaW/Gcfjte0x3didNdluaOOz84 Pm4PqEPqQmVYnAjjDey7PtFjFNo2SMACoUcGPD1CEM0wUNi+6uzO37SRlrrgaJ04t8F5 U6gr5vcb9NTOg07Wg04lHS8mk4dA2slj7A8XtjHI1uQrBcK3yN40+mqKf6hPeK2fhmVV v41fepgn/IABsJvRCexZz6Dhkes4hLX2tqBrN6NMOy4O156V0y1BiU0eOWXqX8LaE9ww feL+qdtJ/k+DR1a/Vm9B/uTOqRqKLyqrIfoAY9KzQzFzYtt7L56VQyBOTK2hGIT3j/Ff 1SGw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=nqu1V52Q; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c30 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc30.google.com (mail-yw1-xc30.google.com. [2607:f8b0:4864:20::c30]) by gmr-mx.google.com with ESMTPS id d16si1342704ywg.5.2019.07.17.10.57.12 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Wed, 17 Jul 2019 10:57:12 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c30 as permitted sender) client-ip=2607:f8b0:4864:20::c30; Received: by mail-yw1-xc30.google.com with SMTP id z63so11061673ywz.9 for ; Wed, 17 Jul 2019 10:57:12 -0700 (PDT) X-Received: by 2002:a81:1289:: with SMTP id 131mr24940126yws.19.1563386232158; Wed, 17 Jul 2019 10:57:12 -0700 (PDT) Received: from mail-yw1-f52.google.com (mail-yw1-f52.google.com. [209.85.161.52]) by smtp.gmail.com with ESMTPSA id e12sm6130422ywe.85.2019.07.17.10.57.11 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Wed, 17 Jul 2019 10:57:11 -0700 (PDT) Received: by mail-yw1-f52.google.com with SMTP id f187so11057285ywa.5 for ; Wed, 17 Jul 2019 10:57:11 -0700 (PDT) X-Received: by 2002:a0d:c804:: with SMTP id k4mr12812018ywd.63.1563386230850; Wed, 17 Jul 2019 10:57:10 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Michael Shulman Date: Wed, 17 Jul 2019 10:56:59 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Papers on constructive simplicial homotopy theory To: 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=nqu1V52Q; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c30 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: , Thanks for collecting all those links together, Nicola! One of the aspects of this theory that I find especially interesting is the observation that many uses of AC in classical model category theory can be avoided by working with "fibration structures" and requiring all factorization and lifting "properties" to be instead given by functions. Of course a similar perspective is present in the notions of algebraic model category (and algebraic weak factorization system) that have recently been playing a bigger role even in classical homotopy theory, so it's interesting that the natural constructive approach is also to work with structure rather than properties, even in the "non-algebraic" case when the structure isn't at all "coherent". 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? On Mon, Jul 15, 2019 at 3:18 AM Nicola Gambino wrot= e: > > Dear all, > > Readers of this list may be interested in the following series of papers: > > [1] S. Henry, Weak model categories in classical and constructive mathema= tics, > > https://arxiv.org/abs/1807.02650 > > [2] S. Henry, A constructive account of the Kan-Quillen model structure a= nd of Kan's Ex=E2=88=9E functor, > > https://arxiv.org/abs/1905.06160 > > [3] N. Gambino, C. Sattler, K. Szumi=C5=82o, The constructive Kan-Quillen= model structure: two new proofs > > https://arxiv.org/abs/1907.05394 > > [4] N. Gambino, S. Henry, Towards a constructive simplicial model of Univ= alent Foundations > > https://arxiv.org/abs/1905.06281 > > Apologies for cross-posting. > > With best regards, > Nicola > > =3D=3D > 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/D3003278-EEC5-46A0-A07A-AD260A830DB2%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/CAOvivQzEtgcx15UZrpos%2Bch8TCKsnQSotvpK5oEVO2EVD160eQ%40= mail.gmail.com. For more options, visit https://groups.google.com/d/optout.