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,HTML_MESSAGE, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ed1-x53d.google.com (mail-ed1-x53d.google.com [IPv6:2a00:1450:4864:20::53d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id fa7e0051 for ; Mon, 15 Jul 2019 10:18:23 +0000 (UTC) Received: by mail-ed1-x53d.google.com with SMTP id y3sf13271845edm.21 for ; Mon, 15 Jul 2019 03:18:23 -0700 (PDT) ARC-Seal: i=3; a=rsa-sha256; t=1563185902; cv=pass; d=google.com; s=arc-20160816; b=YBy1O/5+cY5wwo1m8BRhz9mT2+See79Bng7icotdSeHngaZrM5texhHSghuWFyzdiZ fOA3qruLtG1ytDWTocCAN+A7eCelrCYpSfa6fGLPAjfSNYGTZ2CDt3pg+/b6Q8G9sglw DLbfDeLq4fUEin+Jtk7ZuMAgXgLh7kovp5eLcqTiquWEkh/Qw9A79n2Vc9W7q246rt8C ZhHTuyhcC699K1ikeEWdljbxsi8Xu8R66K32uM8Liw8U/iMXO7XHsyx/XTfx2h7PdE5T ehWiw7H6ldXJ68DvE5uF0YMoJA7e2fberpgS/G8J/B3SHu0A/GILBF2VItfa8AfEXaca fcSg== ARC-Message-Signature: i=3; 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:mime-version:content-language :accept-language:message-id:date:thread-index:thread-topic:subject :to:from:sender:dkim-signature; bh=DRgfumknVOIhJlDjG59P8A84SIoOg8lApAePKOqaytI=; b=bcExTreezNdHPkHFiBAFjWFjD0Ja1mKkuo8WpldmmPq4GxPi0yXIDGEOEsxqw1/hXu BZF9G1RVswBaZtgFxWXxen6zLcq4+fBPMmNVhDcV+NLL8Uv/QMQQUxUPT0ciwmq0tQM5 GdYjsSRsLxBEuBxswNsl7M6HbEZm3n2Y++k7XdMJEy8cSYWeVg1omw6Bt2Ta/m16ZV4o 10ncqlU205f9sxUK88dCCADB84KNVvL8bQDSvIYU+njim1e/0YTSIC6lG1iY+ds27plb Og1eeIRMewKKEGKK1Cs3x0TEY3qQpH83I8Cofij0sAAWzt/aMclOG0iK1afObGTLndGM VCmw== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@leeds365.onmicrosoft.com header.s=selector1-leeds365-onmicrosoft-com header.b=gwlGeGcE; arc=pass (i=1 spf=pass spfdomain=leeds.ac.uk dkim=pass dkdomain=leeds.ac.uk dmarc=pass fromdomain=leeds.ac.uk); spf=pass (google.com: domain of n.gambino@leeds.ac.uk designates 129.11.77.151 as permitted sender) smtp.mailfrom=N.Gambino@leeds.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=leeds.ac.uk DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:subject:thread-topic:thread-index:date:message-id :accept-language:content-language:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=DRgfumknVOIhJlDjG59P8A84SIoOg8lApAePKOqaytI=; b=rdy6r9isvUbHDd+aJPLeD9Bnx+zuzQvqCvUo4SZ9iO49pwJ927+iIJrL7WDP5lY7kw F3Hsn33pZOS7ljFxyhKnrqKeDxrDKmsqp8EWOqHrHbtqBEBQVXJYUG3wHTEI/srl3C4Q O/MfUEhLxGUgxj7DTS2iRhTnImCAtez9gSPcDfF3E654hubMz8TSEOhpwJurrdZBfdqA mIeOJrZ3/LB1p5T7mBhfpN6yrwS3+V6cKahvrh5e6g9vBYWkmqCWn2IjsghAyYDOFLuO aOfUV5AizI3X235V+nnKgfbc5UGZ8cAx74lWckdFWTz6R6QS4zttHH5ISmWDsqR/uZvw FpVQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:subject:thread-topic:thread-index :date:message-id:accept-language:content-language:mime-version :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=DRgfumknVOIhJlDjG59P8A84SIoOg8lApAePKOqaytI=; b=CXRAeC3jJAJPlLuxwrXfZ5I5IpvedfJzUJD7EBimhqn0Rm3Yo0em6qBu9SyKY6ipS+ /CWKlb3op8oLT9yoHK/5kRCpwsV7tnTdEkiqQCjFCaGBhbJfyRIHXP4w3pE3ZBwPL+0y dnrrE7y/Eg72rcIXYJ/RlX5MvbLFpQAjSx2xGXXDgrGiXZIiH/G2tUYoVT+oQZxmL/8y E2zOdMT7KN63zKhVh1OKehIgP9TltNS4WpCmAwPmGtVIR2iovDX9+USX30/ebds20LjG /C6bAevODW61DHzPDmUE/NhDn2QPob0fFJBsFMPJmBM74MrhQXjB6CnWwpERVC3fVTTZ Klfg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVmBsBMpaqThBgOQKt+fz7E2OyR3T++yfYWEKo0npHul1J2HY3k RgipRFzYllhDVaSXSWlGCuk= X-Google-Smtp-Source: APXvYqx2GNyUGHwIPsnuloqThmeo9DhVVDhZlbzSsCKUpALNA8YryQM3dZwLT3iO0w0PIAm71lVv+A== X-Received: by 2002:a17:906:1496:: with SMTP id x22mr19922905ejc.191.1563185902444; Mon, 15 Jul 2019 03:18:22 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:ac62:: with SMTP id w31ls3940309edc.10.gmail; Mon, 15 Jul 2019 03:18:22 -0700 (PDT) X-Received: by 2002:a05:6402:652:: with SMTP id u18mr22313251edx.85.1563185902008; Mon, 15 Jul 2019 03:18:22 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1563185902; cv=pass; d=google.com; s=arc-20160816; b=SomkqfxysT5oW4LUxEvgVVcSE4BI0o/ZNgniJushYvjgg5wFf4tCSYCpPKY0bbIms7 YNHGzIqMPZPRD1CusIpYBfjrNONMAjDJPjcf+0IpzpY19PjLdQe9xyknZGBxk0Q9/B2V u7xSwsZSoKSFqz6HUTdbSOUTL5YdBWr3nh0iAnHumcxM/znq56hq2Qhhrjd+ZJ0aEgzT 3yxjAMfpye7DNepg7pDDGdDdcx8OLK9KjNS4hSBwYq6emYrJMf3LpJA/Z7Nx/8XYDdOe XFJEdAR4EytpXmAwq0u4s8IhsrR1JJgo9AzytCLWnkfCnfR8OS1/IvUrQ76BbaYyJcft Kq6A== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-language:accept-language:message-id:date :thread-index:thread-topic:subject:to:from:dkim-signature; bh=VDhoiNTLSfTaCR90YG9UAJz+GUp4FN692qq8qOR+dCw=; b=KOMKsThq7qB2HNaD2bwKcEnyacnzdaxO0iPReRSfF4Q4B5wwTdem7J8ysKWN8kzuhz 25qdptlg+54RkY83mZ1kA+kZ4AyFUFXFPekdl5FPI7myqBf84/SZo6fO9AxXdi0d/gMQ weD/MUdWbYFRIHqaIzw7sawWqAWGUOuUSERy3E3TbZuG1elMwqRjxgX9cT+/7106mk1Q 6diHH0Z3JHfirQPGSQq2+m8XBVvLl6gyBhuBEXX78FT7lb/kuYxjyx6bViuMkuvptjGj Zyb1fkCNW85yHfcbWhsLbxrEqaB9rr705sy/4yMsGqdc/Y3RPJE+CbWjmvlT8jguQ1CO hWJQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@leeds365.onmicrosoft.com header.s=selector1-leeds365-onmicrosoft-com header.b=gwlGeGcE; arc=pass (i=1 spf=pass spfdomain=leeds.ac.uk dkim=pass dkdomain=leeds.ac.uk dmarc=pass fromdomain=leeds.ac.uk); spf=pass (google.com: domain of n.gambino@leeds.ac.uk designates 129.11.77.151 as permitted sender) smtp.mailfrom=N.Gambino@leeds.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=leeds.ac.uk Received: from mhost02h.leeds.ac.uk (mhost02h.leeds.ac.uk. [129.11.77.151]) by gmr-mx.google.com with ESMTPS id jz14si843754ejb.0.2019.07.15.03.18.21 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 15 Jul 2019 03:18:21 -0700 (PDT) Received-SPF: pass (google.com: domain of n.gambino@leeds.ac.uk designates 129.11.77.151 as permitted sender) client-ip=129.11.77.151; Received: from APOLLO1.ds.leeds.ac.uk (apollo1.leeds.ac.uk [129.11.5.4]) by mhost02h.leeds.ac.uk (8.14.4/8.14.4) with ESMTP id x6FAILbl010531 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NOT); Mon, 15 Jul 2019 11:18:21 +0100 Received: from APOLLO8.ds.leeds.ac.uk (129.11.6.119) by APOLLO1.ds.leeds.ac.uk (129.11.5.4) with Microsoft SMTP Server (TLS) id 8.3.245.1; Mon, 15 Jul 2019 11:18:21 +0100 Received: from EUR03-VE1-obe.outbound.protection.outlook.com (104.47.9.58) by outlook.leeds.ac.uk (129.11.6.119) with Microsoft SMTP Server (TLS) id 14.3.195.1; Mon, 15 Jul 2019 11:18:21 +0100 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=mPdCUclgci5BWNmb1hBETE9F/r9XN5+SBtzJte+EbUDa5AbtlSjrVIo58NuEdT/L8U9Llye+gKgGCTvg9ioFslIWI6OWrAhCg78PjcUm2iDgLhgH50WcQaJyjQssRc1P6ImhT3myA1ZCH6RfsRjik0Qe3ZRJQcJ2NtXPuRNGQk6GBwuAR1CH4Kuil/08w3ao7378l3ii8FYDXQcTnl86Z2RrrpYEVZTfqJa6kYT0uq4dxYLpmpzpS8CfELq/bl3oEy24uhwk46ZphTNCUUNe1wrbrVVHtDkkrsbuMlPBvzVtGK97qvuc+Cneei7NfYWpZCBOcezqzG6YJtAkvCjdCw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=VDhoiNTLSfTaCR90YG9UAJz+GUp4FN692qq8qOR+dCw=; b=DZffU6An2+d3i2xyBHzLac+D8HgCGw2ygDbE4aeRP7ceOyRcnjpsk6Ijp0TtbcdA0028OZwtf9aZnMN28DMI9U8vh/t6jDwJGN1TZjNnZOchizQsFQBwqSLqJ+8fUlOLcN/5PYBRlPtHNplg/cgV0GuW7n+2vQHvRU4EVngOtXjthZ2jBQkUJXN9YSsGpx6Hgf9QIpbllSdHqU49+pHJmXTsFK1lT+JoDCFNV/zVcL6RJHELPdQjTPsuH9S+XbK/ZtvlIz87gH9oAJ/KwO4UNQj5bjONEgiXayf0uptOkJrpSukB6E6mD3KkLv8liqpBJ2mByjDvrgPVtnrAE0Xo+g== ARC-Authentication-Results: i=1; mx.microsoft.com 1;spf=pass smtp.mailfrom=leeds.ac.uk;dmarc=pass action=none header.from=leeds.ac.uk;dkim=pass header.d=leeds.ac.uk;arc=none Received: from DB7PR03MB3641.eurprd03.prod.outlook.com (52.134.98.154) by DB7PR03MB4217.eurprd03.prod.outlook.com (20.176.232.218) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2073.14; Mon, 15 Jul 2019 10:18:06 +0000 Received: from DB7PR03MB3641.eurprd03.prod.outlook.com ([fe80::2daa:b11:62f6:71a1]) by DB7PR03MB3641.eurprd03.prod.outlook.com ([fe80::2daa:b11:62f6:71a1%4]) with mapi id 15.20.2073.012; Mon, 15 Jul 2019 10:18:06 +0000 From: Nicola Gambino To: Homotopy Type Theory , "constructivenews@googlegroups.com" Subject: [HoTT] Papers on constructive simplicial homotopy theory Thread-Topic: Papers on constructive simplicial homotopy theory Thread-Index: AQHVOvaXNQ6NSoHaLkuDodz7rXqBpQ== Date: Mon, 15 Jul 2019 10:18:06 +0000 Message-ID: Accept-Language: en-GB, en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-mailer: Apple Mail (2.3445.104.11) x-originating-ip: [95.150.83.210] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: 575eca08-74e7-4cbc-d0e5-08d7090dba89 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(5600148)(711020)(4605104)(1401327)(2017052603328)(7193020);SRVR:DB7PR03MB4217; x-ms-traffictypediagnostic: DB7PR03MB4217: x-ms-exchange-purlcount: 4 x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:6790; x-forefront-prvs: 00997889E7 x-forefront-antispam-report: SFV:NSPM;SFS:(10009020)(39860400002)(346002)(136003)(396003)(376002)(366004)(199004)(189003)(6486002)(68736007)(486006)(99286004)(81166006)(316002)(3846002)(8936002)(6116002)(50226002)(66066001)(81156014)(413944005)(966005)(478600001)(786003)(6436002)(57306001)(36756003)(450100002)(25786009)(33656002)(476003)(2616005)(606006)(6506007)(102836004)(6306002)(2501003)(2906002)(236005)(6512007)(53936002)(186003)(26005)(54896002)(66476007)(86362001)(14444005)(256004)(8676002)(7736002)(4744005)(71200400001)(64756008)(66556008)(91956017)(76116006)(66946007)(66446008)(110136005)(71190400001)(14454004)(5660300002)(66574012);DIR:OUT;SFP:1101;SCL:1;SRVR:DB7PR03MB4217;H:DB7PR03MB3641.eurprd03.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;A:1;MX:1; received-spf: None (protection.outlook.com: leeds.ac.uk does not designate permitted sender hosts) x-ms-exchange-senderadcheck: 1 x-microsoft-antispam-message-info: iJJT4ZwrZtJSWxov3Hz/URHVtnKS2o8hvXBE7+gSwuPtHnctGHZijGKcBpqPMk2fupfxBM6dZDbOWtmqsi/kKncS0b84NAtiqc83H4wM4gEphvAq2TJmxin+c/QU4G/8sNXk2AUhpwJch8F4IxNSKgwFTQPAk7UBwFHhy/ZrK3DZdQVWa0zYAznDgzx8j3xECPnEYUuVFu7szKZxk2aTO0WWzMXFh/5qPeRlNkiRB/kAr/7LgFHNAM+thDAI7k4pB9B0w3Ud9y20i25BUT5hT6U4eCOULImTGqXRw32+N3IGpV95VGfMnuJBR6tzRE9Duins6scjBnuErd4g/lFs+VxE9B/Ht/ywNavHWi5Q39TNeTNpnApYJ/WWCBeLvKFV7norh0mjGTUe+RqAPMNkec2CFSR60TGbvgtQYwTOmVw= Content-Type: multipart/alternative; boundary="_000_D3003278EEC546A0A07AAD260A830DB2leedsacuk_" MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 575eca08-74e7-4cbc-d0e5-08d7090dba89 X-MS-Exchange-CrossTenant-originalarrivaltime: 15 Jul 2019 10:18:06.3874 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: bdeaeda8-c81d-45ce-863e-5232a535b7cb X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-CrossTenant-userprincipalname: pmtng@leeds.ac.uk X-MS-Exchange-Transport-CrossTenantHeadersStamped: DB7PR03MB4217 X-OriginatorOrg: leeds.ac.uk X-UOL-RateLimit: userRateLimit[a:n.gambino@leeds.ac.uk,c:2.4715289924487083,l:500.0] X-Original-Sender: n.gambino@leeds.ac.uk X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@leeds365.onmicrosoft.com header.s=selector1-leeds365-onmicrosoft-com header.b=gwlGeGcE; arc=pass (i=1 spf=pass spfdomain=leeds.ac.uk dkim=pass dkdomain=leeds.ac.uk dmarc=pass fromdomain=leeds.ac.uk); spf=pass (google.com: domain of n.gambino@leeds.ac.uk designates 129.11.77.151 as permitted sender) smtp.mailfrom=N.Gambino@leeds.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=leeds.ac.uk 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: , --_000_D3003278EEC546A0A07AAD260A830DB2leedsacuk_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 mathemati= cs, https://arxiv.org/abs/1807.02650 [2] S. Henry, A constructive account of the Kan-Quillen model structure and= 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 m= odel structure: two new proofs https://arxiv.org/abs/1907.05394 [4] N. Gambino, S. Henry, Towards a constructive simplicial model of Unival= ent 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/ --=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/D3003278-EEC5-46A0-A07A-AD260A830DB2%40leeds.ac.uk. For more options, visit https://groups.google.com/d/optout. --_000_D3003278EEC546A0A07AAD260A830DB2leedsacuk_ Content-Type: text/html; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable
Dear all,

Readers of this list may be interested in the following ser= ies of papers:

[1] S. Henry, Weak model categories in classical and c= onstructive mathematics, 


[2] S. Henry, A constructive account of the Kan-Quillen mod= el structure and of Kan's Ex=E2=88=9E functor, 


[3] N. Gambino, C. Sattler, K. Szumi=C5=82o, = ;The constructive Kan-Quillen model structure: two new proofs


[4] N. Gambino, S. Henry, Towards a constructive simpl= icial model of Univalent Foundations


Apologies for cross-posting.

With best regards,
Nicola

=3D=3D
Dr Nicola Gambino
Associate Professor in Pure Mathematics
School of Mathematics, University of Leeds




--
You received this message because you are subscribed to the Google Groups &= quot;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/m= sgid/HomotopyTypeTheory/D3003278-EEC5-46A0-A07A-AD260A830DB2%40leeds.ac.uk<= /a>.
For more options, visit
http= s://groups.google.com/d/optout.
--_000_D3003278EEC546A0A07AAD260A830DB2leedsacuk_--