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-x537.google.com (mail-ed1-x537.google.com [IPv6:2a00:1450:4864:20::537]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 4dc80164 for ; Thu, 18 Jul 2019 07:55:42 +0000 (UTC) Received: by mail-ed1-x537.google.com with SMTP id f3sf19436325edx.10 for ; Thu, 18 Jul 2019 00:55:42 -0700 (PDT) ARC-Seal: i=3; a=rsa-sha256; t=1563436541; cv=pass; d=google.com; s=arc-20160816; b=cVvG4BCZP68qSGbi+TJLcWT40XhP75cy0t9mK/xvSGMQuJThmjp8UQuK/25i+dFQ+I uyUfbMhhKT2I4SEo0VmPeZg3gOB0iSrjdYA37Z/dzPsMbKzMSONE/BUD+/tAEsoHEG00 W0+4NTSf/psV4t5lAUFN9kaUQU0Z3MSB7exs09uePR43ev5I0ED5vXMbfuCo86qAc75b DqVG2ZsWxspFvdkvLnMhoZY+4ZTUOpKmBQNqoy8oTjwrW/7Ap5sk9z1fMC26150a408Q 0GG3CymIMGe9nxgpHTwmFZBGnlflxsHPjIt+/TFvBygW2F3bMXlfDapElOcCJQiAuf36 oVgw== 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:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from:sender:dkim-signature; bh=HtjL1t/mvX1v28BQ7wQf39/v+KMyvxlkbCHD7tRBu0k=; b=VX91bvSsRBVZAdpBMSsYJYSOzbwawiPbGf+1GpfUQslj/eNB0/osTgy7dOgz9drGyN a+uLarFuWkXVUpmZCM0eJPkz8wvfNsBgxQtiMi11CYLuKUlEJoZ1p43diGky+i5tVi1X DgPjI2SL03U7r/VFmg3fhwPWBFpQ/WM4HOBUyj9lpe5re3Fcyrrna55tIfiXU1UhHwdR svBKshdq3clUGT+9ZnIGrFtGmeY+xwIZ95rkRNuNS3Z7n5+A5/ROaaB7NB6pNgxHsmPT zyzgfQm+O6/wQMEQigkJ8nixYUPcNQ5cxjysTIyqUjmk1S7X4HCcHzBHDueZfnzmX9FV kXrQ== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@leeds365.onmicrosoft.com header.s=selector1-leeds365-onmicrosoft-com header.b=Kl+6wlbs; 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.76.154 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:cc:subject:thread-topic:thread-index:date:message-id :references:in-reply-to: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=HtjL1t/mvX1v28BQ7wQf39/v+KMyvxlkbCHD7tRBu0k=; b=OtGjzsuzEXtKXmqIuh++GIxlHMj+ej7qnu4yidQFKdgGJSKAphcd2gaiiVZqbDoODy xdtFOsLR4xTfNkr/TS7w6TLbAnzq8PJWL+sPzb6GdqQ/tHBihHVYxLXEYJiJXIoEsn8p Fv0nSfHE2mr8y1g7SgNmTdVyupUv6dRZsxBSTqNOumv9eyVhbdZyhhd8723zVYH5aylz OSIYlwVWe0yygcf795lzFMvbUQ5UuOOUkmSxTmD/8CeHgacbeYcR98zjAsbwZDTAUtv9 6OVvuvP0mEpzXI1clWdowLgppIXw/+s3aXvwd335lP7EXCM1nvIW4+0vUE51SITi7zWC 3q1w== 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:cc:subject:thread-topic :thread-index:date:message-id:references:in-reply-to: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=HtjL1t/mvX1v28BQ7wQf39/v+KMyvxlkbCHD7tRBu0k=; b=jGeEm7gu7T8iGx5p7aOQ/AUGQdD1d+Q9OtkndsTBORUnu475C2uRk0lUJVnLvu4jr5 9Hgk+QWVbzHRhlkCHfSqtHd9BJL7LInUNRhX/tLGcx85Id63rRHVrjIMN0XRK1qHrEki BXEde+ONYN9CzrJq/HWutsYWd77xwOouHBBp0zgMeS1c5wYsOgR7pNpvj8hsbsK1wAGB /o1hzkgDR8zz174aOX2xZGOEKcej2sz3K3Pa5z9RWi4XA55YhKAm5W8pmuT53+oOK2Oy HjxhAB5WbWbwcdsBuVTRRlpo9yhdrUASQDvGjfnRU6M+Co+xoXkQSP54ZNVBJC5tPktL W7Ig== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUZ3lLAkxsCBVxVU97CZsheCLxx2LXaiQJiVAwKfRNJBagvRyLN 82IrP8VUsMBI5H3zYy0Q6FU= X-Google-Smtp-Source: APXvYqwXbiZU9iOsrwRSpNQPeAgzJ5ioylcI+SAMBJFBdfL8SHC8z/CHTPWo98ozMQgo1HevToFcHw== X-Received: by 2002:a17:906:5ad0:: with SMTP id x16mr35325984ejs.23.1563436541510; Thu, 18 Jul 2019 00:55:41 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:f4c3:: with SMTP id v3ls6413298edm.11.gmail; Thu, 18 Jul 2019 00:55:40 -0700 (PDT) X-Received: by 2002:aa7:cd17:: with SMTP id b23mr39381877edw.278.1563436540932; Thu, 18 Jul 2019 00:55:40 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1563436540; cv=pass; d=google.com; s=arc-20160816; b=Hm5hECwWMAYKN3bHq04IamG9ebiw8kRTGg2PHYKVfKrZl++jPaoNYJbZk6GfcRbmD8 V6AtNcquj2i3xXIUsM2WoWgoKr4itp7hk/Gzk65ry+c1b++u9Hp50mkHviYQ3LW6MbIx xmcdW9zpsps+k2WsLoqwxjtmx1pBIRa4I6e8ThUYZovTJUSA49ViLo1bfHw0/vkbO6kJ G84dRdb4ZJEzDwDAdapsiJmFmzP4l5Y0A/alz+xifszdyszP2zLwXOjg4etgtyauz+tI +/lBNdbtq8I6waQLZMJPDVJMEeBVNSOQOAB8Q5NxRNWMOXumhnPswUOGa9Sp+jVDDeWn QlyQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-language:accept-language:in-reply-to :references:message-id:date:thread-index:thread-topic:subject:cc:to :from:dkim-signature; bh=e4X68Yn1yOJnMbe77w6Vdzna+CharAb3jVD2rGjaSlo=; b=BNwQBPjxQiZcpV0XsDducLXm3GCWJ9WyULIQxFiItEuY6lc7xvaBl0CXS8PjCAeiwU DJcpqKVygFn0tCy/bBdSosc40k2tUDH8Zctoy11010/0K+7kwNCIfZF2XO24CaLx/b7S 6a7lHSiTaavq9yxScSpSytpqwQsXwgkm9li1wj/syZl+gxkBT8lr4Zh2dAHe74I1VH4K Tsg8Yx49rp/E0yleUK0tJqd5lkAZZuorORcu+yUn1ohyL7X89HIsqVdNdVuJw/9/xzTq bQlovsbGAGUxO6XtAdmFExFtPxrJitU6VJZ/UUrdqqveVsBnAqJOHhZAWbYbX/ziwq+c cMbw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@leeds365.onmicrosoft.com header.s=selector1-leeds365-onmicrosoft-com header.b=Kl+6wlbs; 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.76.154 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 mhost02c.leeds.ac.uk (mhost02c.leeds.ac.uk. [129.11.76.154]) by gmr-mx.google.com with ESMTPS id h23si1473030edb.2.2019.07.18.00.55.40 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 18 Jul 2019 00:55:40 -0700 (PDT) Received-SPF: pass (google.com: domain of n.gambino@leeds.ac.uk designates 129.11.76.154 as permitted sender) client-ip=129.11.76.154; Received: from APOLLO1.ds.leeds.ac.uk (apollo1.leeds.ac.uk [129.11.5.4]) by mhost02c.leeds.ac.uk (8.14.4/8.14.4) with ESMTP id x6I7teOe014342 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NOT); Thu, 18 Jul 2019 08:55:40 +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; Thu, 18 Jul 2019 08:55:40 +0100 Received: from EUR04-VI1-obe.outbound.protection.outlook.com (104.47.14.50) by outlook.leeds.ac.uk (129.11.6.119) with Microsoft SMTP Server (TLS) id 14.3.195.1; Thu, 18 Jul 2019 08:55:39 +0100 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=WVgOpCfQO+/YDKJSEdw8TXv0HlAj2FKZCKNOlQLpogP5A0lPj8jwTUZrClWqD+rMcRsvzRmRjhZ+vNYHRYRVxxcpIXH8FV7W6W3Bahtip057Udzu/XzhPieAcUykW992/TEMpyhY9ckuVhxb4Ia7HM2JCPT7CT3bACgaYQJ1T8gCCwDw2sc9WOaHM4dS7SLwJX0LOwSJ+WTdjVSICuYGs080TJ8fcxREAdZhoZSpo3SKQdXdiKG0eFZmYLJD2VrmJdDV84Go586HiEJQ9WnOV8cY9RVaMjG+8pN2cciq/1AasvvYCBhS6P5YuUEqJ9cDyhp43Zcp0TuZnUQRZtjdwA== 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=e4X68Yn1yOJnMbe77w6Vdzna+CharAb3jVD2rGjaSlo=; b=VsKcM1CsiOEl1oStmGybJg6pujNkSQKUt8uka9oNW+gU53lbfWXezCHTr2bYem+oXARYc+r8Y2yREryIYphmU9kkDCDuNdSK1k1AD5+YwPHSXC6DZnsMshXFJe1F2uqm/0gb1rTr0gzRjPj2DRLNljcHmUwXwhNP9VxGIarYLeKsMLYBDAaQ2uNJVu7laEd8i23f8YGNqFXQbYioX/E+vu9s1GHd8IMwFHLD6Fc3w3AkzPZaINzIqf80Utae4zA6MXJHhEmv0JHl/u4B75auJoggMEr9we1YjRGDg5osdNxOba1Gq/TiciMR7krviglwAYLvC1taNnkiia582WZARw== 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 AM6PR03MB3640.eurprd03.prod.outlook.com (52.134.114.157) by AM6PR03MB4821.eurprd03.prod.outlook.com (20.178.91.93) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2073.14; Thu, 18 Jul 2019 07:55:39 +0000 Received: from AM6PR03MB3640.eurprd03.prod.outlook.com ([fe80::95dd:66ee:7906:e190]) by AM6PR03MB3640.eurprd03.prod.outlook.com ([fe80::95dd:66ee:7906:e190%5]) with mapi id 15.20.2073.015; Thu, 18 Jul 2019 07:55:38 +0000 From: Nicola Gambino To: Michael Shulman CC: Homotopy Type Theory Subject: Re: [HoTT] Papers on constructive simplicial homotopy theory Thread-Topic: [HoTT] Papers on constructive simplicial homotopy theory Thread-Index: AQHVOvaY6FEJoDZYPkmUqnvlfJhZ9KbPHCGAgADqUIA= Date: Thu, 18 Jul 2019 07:55:38 +0000 Message-ID: References: In-Reply-To: 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: [194.80.232.19] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: 7026f5cd-63fc-4a20-e9cf-08d70b55530a x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(5600148)(711020)(4605104)(1401327)(2017052603328)(7193020);SRVR:AM6PR03MB4821; x-ms-traffictypediagnostic: AM6PR03MB4821: x-ms-exchange-purlcount: 2 x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:10000; x-forefront-prvs: 01026E1310 x-forefront-antispam-report: SFV:NSPM;SFS:(10009020)(136003)(346002)(396003)(366004)(376002)(39860400002)(199004)(189003)(25786009)(8936002)(81166006)(81156014)(606006)(86362001)(6916009)(68736007)(2171002)(6246003)(14454004)(26005)(186003)(5660300002)(71190400001)(76116006)(91956017)(54896002)(6306002)(6486002)(6512007)(6436002)(33656002)(50226002)(786003)(4326008)(316002)(66476007)(71200400001)(66946007)(66446008)(64756008)(66556008)(2906002)(446003)(6506007)(2616005)(476003)(36756003)(57306001)(478600001)(99286004)(76176011)(6116002)(486006)(229853002)(66066001)(236005)(53936002)(3846002)(966005)(413944005)(8676002)(11346002)(256004)(53546011)(102836004)(7736002);DIR:OUT;SFP:1101;SCL:1;SRVR:AM6PR03MB4821;H:AM6PR03MB3640.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: 16MsE8KNiS+8fOB3h8K7NMoXW/WaAgW5ga3q8r9cGtYDJ40pvpJAR6VwGXoV5x5Ys0IMvEzFn1Anm+z9ZtuELUyZulNqSG7sHWiXzP5La0pHsLlklcKIRItQPwhNR7+VI+qtyR+SNWV2w/S5buWTUl/uh/Cn0Xhq4iRwYMKmNdhm2v9zJUdUpLQs3fqh4psntu881ObdsU5q3jD+BViwARnoi22ar/fMYPV95m6Y76vzPL+MNNLhDy6StCnDL99rdDw26LWsNacA8JRbod4ehkx7gIoJ32m/AWqc0bVWRUnATOh9N8JEzMPbvE2BdjEn1XiGNZYaL01Y9eq4Zm8A2/2eu+gs3w6navdSphF28LVsTxuUQjPKiRn2ixY41hc9/N42g4dlQqJsHY59AtE4BziJZg/cPKqfZ1l7cDIy1pY= Content-Type: multipart/alternative; boundary="_000_D49A1FEA4CE1448F97A846065AF9E7B6leedsacuk_" MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 7026f5cd-63fc-4a20-e9cf-08d70b55530a X-MS-Exchange-CrossTenant-originalarrivaltime: 18 Jul 2019 07:55:38.8285 (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: AM6PR03MB4821 X-OriginatorOrg: leeds.ac.uk X-UOL-RateLimit: userRateLimit[a:n.gambino@leeds.ac.uk,c:0.11692512208298449,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=Kl+6wlbs; 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.76.154 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_D49A1FEA4CE1448F97A846065AF9E7B6leedsacuk_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 am = not sure what kind of dependent type theory would be sufficient to develop = 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 wo= uld 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 every= thing 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 "W= eak model categories in classical and constructive mathematics=E2=80=9D is = 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/ --=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/D49A1FEA-4CE1-448F-97A8-46065AF9E7B6%40leeds.ac.uk. For more options, visit https://groups.google.com/d/optout. --_000_D49A1FEA4CE1448F97A846065AF9E7B6leedsacuk_ Content-Type: text/html; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable
Dear Mike,

On 17 Jul 2019, at 18:56, Michael Shulman <shulman@sandiego.edu> 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<= br style=3D"caret-color: rgb(0, 0, 0); font-family: LucidaGrande; font-size= : 12px; font-style: normal; font-variant-caps: normal; font-weight: normal;= letter-spacing: normal; text-align: start; text-indent: 0px; text-transfor= m: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width:= 0px; text-decoration: none;" class=3D""> an elementary topos with NNO, or in CZF, and by an "abuse of language&qu= ot;
we interpret "for all x there exists a y" as referring to the givin= g
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 am not sure what kind of dependent type theory would be sufficient to dev= elop 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 o= ne 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).&n= bsp;

One could then keep track explicitly of which existential quantifies a= re to be left untruncated and which ones can be truncated, and then see if = everything 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 fac= torisation systems, i.e. weak factorisation systems in which one has a give= n choice of fillers, and work with them. This would be a variant of the theory of algebraic weak factorisation systems. We are work= ing on that.

With best wishes,
Nicola

PS The first link in my email was incorrect. Simon Henry=E2=80=99s pap= er "Weak model categories in cl= assical and constructive mathematics=E2=80=9D is available at <= a href=3D"https://arxiv.org/abs/1807.02650" class=3D"">https://arxiv.org/ab= s/1807.02650. 

 



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/D49A1FEA-4CE1-448F-97A8-46065AF9E7B6%40leeds.ac.uk<= /a>.
For more options, visit http= s://groups.google.com/d/optout.
--_000_D49A1FEA4CE1448F97A846065AF9E7B6leedsacuk_--