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.8 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-wr1-x43a.google.com (mail-wr1-x43a.google.com [IPv6:2a00:1450:4864:20::43a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 1b11c679 for ; Thu, 20 Jun 2019 16:39:15 +0000 (UTC) Received: by mail-wr1-x43a.google.com with SMTP id s18sf1409717wru.16 for ; Thu, 20 Jun 2019 09:39:15 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1561048755; cv=pass; d=google.com; s=arc-20160816; b=MB26QkUExPJZGBLNM9yefo85RusejAiQtO7Xedvoh/PREQMNPm1LAxbJB9lksWSBpE aoUI88frSwSLvVWY5wdu+Xq7EfoYAXxJsK4UxtKYtknaltPhjAsT6IcCnOXHX6uDRBkf YN+r+dF8tNac9Y3nwAVosq5jQ7YdPU/cuEd+EgXysGIAA1bEuSLjUcBZGvbHPd6brwzu eOUyuQ//CjMeMB6DqZR1ITlQpc5k0MJuW7vbeqjif0SZYy6f7DZ5ok1cfvT5SOVdCfDz CHXF67sPYICEGz87l662jFAo9fQVnluyOhZPs44BBjbuJXpXZWhUKHSD4/OQBWMVJ+HI fS6A== 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:mime-version:user-agent:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:to:from:sender:dkim-signature; bh=SaSrogrYu4PECRvDPR8Bxkn30cOMJfBTJoU3ZyPrY8Q=; b=nMfZoCfCRrkr6TVQTIhN/ZSyFD72VjmcubLUNwh8g93Je3LWf8ZRivl45rMB9aD7+L HHjcFcu/4xQ+5ms95ytE5zNxN94Qn4jQyGkL/OnukTO1AlU//0RUCKpRYoQmjg+7mx8k ZbrLi6f15/z4BpkwNJxOUTHzSQwtEcQUxEd2XaGQDELrXOwsD8+sW3UOCTd14aT2okui HjbXYrAXAvfuJlGYocGh6mkScl4OEILwkJDyGEvd3r7XiLSjN3Z1HKwlINahTvKYXNiO V2v11ywQ03EW8Zs0f9X+QtTsXqIlvKaq+Q9J8MStjUyOdINZREofl4FSx2E+uC2TKp6q oVeQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=nottingham.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 :references:in-reply-to:accept-language:content-language:user-agent :mime-version:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=SaSrogrYu4PECRvDPR8Bxkn30cOMJfBTJoU3ZyPrY8Q=; b=RA+YSaDrp+7rBdvjtT6xFbPV/B6HJX9nydJv9k71m+oYe4CobHfYLID4XtIfGMiDD+ WysXPrIWcTvljpepaDDeWlP7MbPuw0nnbNnTG6CJpQN5vP6C3BHrOumi6pQu3K8WbGjX U2PZXUuOnjgrQnFXIzn7dkOxp3lIxq93wAH/o0PKmcg/6JSCKp39BvhyZsWx6iQuebn5 WRyJX5DJdj06LEc+TryoicStEzT7H7J/N18zOt6UgDj9iU+05FGRVL52HR5kuQv/vZMH 34rC40/sLfXyjcucN3vg6j499tOxMD+e0aEuqx5kSpzwb2GyN3FO07FlkTUBCmMHyysT M01A== 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:references:in-reply-to:accept-language :content-language:user-agent: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=SaSrogrYu4PECRvDPR8Bxkn30cOMJfBTJoU3ZyPrY8Q=; b=L35RWGNqE7Cw+vVavb3xMbmjOX563GUdTlIqNGkhcjamfKQyEJani2kaKBCTc7/D6C fe2BM4EF6UCYyUOQK93GBpROwX6NO8fDlqbBiRtMebqy6PKQ3bVFBQ95vVacmmJt/Pxf zZJWAOTQlcfE6nxPa5GadHCwpPbvKSO5FzRQ4gE3Jkspt7Hw2LJKY5ymR4UGZheuI/8c l33uvDhp5O99l6esJx3wLGv3gxda9jzDocVCrE0H7lA79WwWWSjGXyMm/k5a425Al8Cs lghmqw2W7fnt0msgvv3/ncrKdnEljqjHRQIglyeJoJYQsxw/dkhNoLv6eMRhZJQKsQsc F27A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVKqxUaxB5RrdZbXVeQ1usnhMwC1dvO6bQaEZG6QKbnOtjWmKY8 MIGlsAnsCicWmzZDoQQ69ko= X-Google-Smtp-Source: APXvYqxEc3heiqUFiW+yO3+AiutLORwiLKeE5HxZF/YL9UTt1mWFEVLPU9N/cKT75SM+V+O6KxCjrw== X-Received: by 2002:adf:ebc2:: with SMTP id v2mr1381424wrn.331.1561048755151; Thu, 20 Jun 2019 09:39:15 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:2d02:: with SMTP id t2ls1751225wmt.0.canary-gmail; Thu, 20 Jun 2019 09:39:14 -0700 (PDT) X-Received: by 2002:a7b:ce88:: with SMTP id q8mr337613wmj.89.1561048754471; Thu, 20 Jun 2019 09:39:14 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1561048754; cv=none; d=google.com; s=arc-20160816; b=dnisC/clDWg/Vm0so0hFJT0Gmoslibv9bJLedosaVr/Z2EcJU44M3pst/97gUK2zKP Z3scyP/K1noeLI6QuwAk9WxPWz77dh75nzvyFrkOcbcnWXKGx/xL6PpxGwDT1dJo+H7L KGKa0lL7nFrxipRpKYXQ2Qx0H54Snb8qZD0YK01oDByO7AecBMC4P3yIDc4di3CmkFdJ DjHfd+wgsW8kc0JoGjktqi6+GBgQF9XQsJ/nI4fTRqqkuqhH5cGTiT0qQ9hRrm2mRwsO d70bSTiASk2+OCUyWXm0ZhnVitu57Vrak5COMac2iATjddIHQJ7SB3kvkuYWuwALlH92 T8TA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:user-agent:content-language:accept-language :in-reply-to:references:message-id:date:thread-index:thread-topic :subject:to:from; bh=1IG6svQ1dUwFbhkxC2B2/0vNsfhBRbAD4V/78SZ9Gt4=; b=i4QbF1FmrBf0tWJMa/FF8NdYIOFeBsZiAQUrVzNiH1z9UQ1nWCQIwiWTAnbA5C1nvV +40bafyhzJLzIjjc2HPKdQ3D9YqWOWjsMyF89EqlUz/hj+gQxtdreEHv0hENz1LOffWS VpbaxNUZ3wNpPJ3PYLuZBoxbU16HZ9fbZm3d2HdI1S+MjoqEbWupi7RkKQinOY9PJEO9 fcIJyU5mAv125Jboe76nMNPg07rYhryZKUpvo9mXzMOgsTi7vjpdh5C8QBKJT01cI1JM 1+pY0OEFqhRBwxF2laxqS0qxXSsRwkZ7mrfzm2ujXYub71503IPVSWzZ9W499tLCx7Lc K0yA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=nottingham.ac.uk Received: from uidappmx05.nottingham.ac.uk (uidappmx05.nottingham.ac.uk. [128.243.43.128]) by gmr-mx.google.com with ESMTPS id u18si2401wrn.5.2019.06.20.09.39.14 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 20 Jun 2019 09:39:14 -0700 (PDT) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 as permitted sender) client-ip=128.243.43.128; Received: from uidappmx05.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 420BF6D0FF1_D0BB6B2B for ; Thu, 20 Jun 2019 16:39:14 +0000 (GMT) Received: from smtp4.nottingham.ac.uk (smtp4.nottingham.ac.uk [128.243.220.65]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by uidappmx05.nottingham.ac.uk (Sophos Email Appliance) with ESMTPS id CBAE16CDF17_D0BB6B1F for ; Thu, 20 Jun 2019 16:39:13 +0000 (GMT) Received: from uiwexedg02.ad.nottingham.ac.uk ([10.159.172.14]) by smtp4.nottingham.ac.uk with esmtps (TLSv1.2:AES128-SHA256:128) (Exim 4.85) (envelope-from ) id 1he05h-0007qs-PX; Thu, 20 Jun 2019 17:39:13 +0100 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) by exchangeSMTP.nottingham.ac.uk (10.159.172.14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Thu, 20 Jun 2019 17:39:13 +0100 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.1531.3; Thu, 20 Jun 2019 17:39:13 +0100 Received: from UiWexEDG01.ad.nottingham.ac.uk (10.159.172.13) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3 via Frontend Transport; Thu, 20 Jun 2019 17:39:13 +0100 Received: from EUR01-VE1-obe.outbound.protection.outlook.com (128.243.226.54) by exchangeSMTP.nottingham.ac.uk (10.159.172.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Thu, 20 Jun 2019 17:39:13 +0100 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB3216.eurprd06.prod.outlook.com (10.170.230.151) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1987.15; Thu, 20 Jun 2019 16:39:11 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::4c3d:4c42:fc4f:7bf5]) by VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::4c3d:4c42:fc4f:7bf5%5]) with mapi id 15.20.1987.014; Thu, 20 Jun 2019 16:39:11 +0000 From: Thorsten Altenkirch To: Nathan Carter , Homotopy Type Theory Subject: Re: [HoTT] my first 3 questions about HoTT Thread-Topic: [HoTT] my first 3 questions about HoTT Thread-Index: AQHVJ4OTGGYO2qpXGkiu7G2nZ2HN86akzxsA Date: Thu, 20 Jun 2019 16:39:11 +0000 Message-ID: References: In-Reply-To: Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/10.1a.0.190609 x-originating-ip: [128.243.20.140] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: 69bb5aa0-6a9d-4641-ef14-08d6f59dd300 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(5600148)(711020)(4605104)(1401327)(2017052603328)(7193020);SRVR:VI1PR06MB3216; x-ms-traffictypediagnostic: VI1PR06MB3216: x-ms-exchange-purlcount: 2 x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:9508; x-forefront-prvs: 0074BBE012 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(376002)(366004)(396003)(136003)(346002)(39860400002)(43544003)(199004)(189003)(51874003)(478600001)(66476007)(316002)(14444005)(6246003)(66946007)(11346002)(91956017)(446003)(25786009)(2616005)(33656002)(476003)(71200400001)(26005)(54896002)(6116002)(9326002)(486006)(236005)(53936002)(6512007)(7736002)(6436002)(186003)(6486002)(229853002)(71190400001)(3846002)(68736007)(99286004)(74482002)(102836004)(966005)(8936002)(76176011)(6506007)(81156014)(606006)(2906002)(14454004)(58126008)(66446008)(6306002)(786003)(73956011)(8676002)(81166006)(5660300002)(66574012)(110136005)(76116006)(86362001)(66066001)(64756008)(256004)(66556008)(42522002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB3216;H:VI1PR06MB4029.eurprd06.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;A:1;MX:1; received-spf: None (protection.outlook.com: exmail.nottingham.ac.uk does not designate permitted sender hosts) x-ms-exchange-senderadcheck: 1 x-microsoft-antispam-message-info: mtQkJ6LOYD5mfwcTwwb0KCy+SohJW0cn0LBU8UiMQn6iT7FM+2PIl0LNK2Svi9eDToVtXwO9la+roafmcC8/ZTIxw9L/RSXHBP48AuahdzhDB1l7sNGN+O4rASUinAaFDuVpe3Upy2+BIwSe23w9uvkysWqq1K/F0FXk1xfiMztBlFir7XsrnBWrbnUDwcXNt6eO/FK+8EkRUX2zJrkWmn9iey/2HrN2BGLFGmS0SN7uyz4enT3xuShSWI1WM+DfYcppNEoH+hzXhIBBkdnFl6q/PNbKpqsSJyuPfSTbSy2aXdIBujt+Ls5wlPSh3q24e4RkqKRLqWvHla4SXghrHSecc2csRH0zIhTz/62OZ/TCwFEM70UuGQeMvzbFzR0mfXE8e5Q0V1FS0z8jhc8vZ4NBPqyplHPUzMCDYq0lURg= Content-Type: multipart/alternative; boundary="_000_C02F985858684447B0C1D1303A754F60exmailnottinghamacuk_" MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 69bb5aa0-6a9d-4641-ef14-08d6f59dd300 X-MS-Exchange-CrossTenant-originalarrivaltime: 20 Jun 2019 16:39:11.7258 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-CrossTenant-userprincipalname: Thorsten.Altenkirch@nottingham.ac.uk X-MS-Exchange-Transport-CrossTenantHeadersStamped: VI1PR06MB3216 X-OriginatorOrg: exmail.nottingham.ac.uk X-SASI-RCODE: 200 X-Original-Sender: thorsten.altenkirch@nottingham.ac.uk X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=nottingham.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_C02F985858684447B0C1D1303A754F60exmailnottinghamacuk_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi Nathan, I can try to give answers but the answers you get may depend on the person = you ask. 1. Very early in the HoTT book, it talks about the difference between ty= pes and sets, and says that HoTT encourages us to see sets as spaces. Yet = in a set of lecture videos Robert Harper did that I watched on YouTube (whi= ch also seem to have disappeared, so I cannot link to them here), he said t= hat Extensional Type Theory takes Intuitionistic Type Theory in a different= direction than HoTT does, formalizing the idea that types are sets. Why d= oes the HoTT book not mention this possibility? Why does ETT not seem to g= et as much press as HoTT? ETT or computational type theory relies on some notion of untyped computati= on which is then sorted by defining some semantic criteria for types. I pre= fer only to to talk about typed entities because they are the constructions= which make sense and it shouldn=E2=80=99t be necessary to refer to some un= typed codes. However, this is my preference, I am sure Bob Harper views thi= s differently. Also the semantic definitions refer to a rather unspecified = meta theory, while in a type theory specified as the initial syntax of some= kind of algebras you get a precise and 1st order definition what exactly t= he theory and the models are. 1. When that same text introduces judgmental equality, it claims that it= is a decidable relation. It does not seem to prove this, and so I suspect= ed that perhaps the evidence was in Appendix A, where things are done more = formally (twice, even). The first of these two formalisms places some rest= rictions on how one can introduce new judgmental equalities, which seem suf= ficient to guarantee its decidability, but at no point is an algorithm for = deciding it given. Is the algorithm simply to apply the only applicable ru= le over and over to reduce each side, and then compare for exact syntactic = equality? It is beyond the scope of the HoTT book to discuss the algorithm to decide = definitional equality. There are a number of standard approaches to do this= : you can normalize the terms in a syntactic way and use this to decide equ= ality but then you need to prove that the normalisation procedure actually = terminates and is well behaved wrt typing which isn=E2=80=99t trivial. Anot= her approach is to use a constructive semantical model to normalize (this i= s called normalisation by evaluation) but again this isn=E2=80=99t complete= ly trivial. The na=C3=AFve algorithm you suggest may not take care of eta-e= qualities. Moreover, the theory presented in the HoTT book has a serious problem: exte= nsionality principles like functional extensionality and univalence are add= ed as axioms, which have no place in type theory. Their presence destroys c= omputational adequacy, which means that a closed term of type Nat may not r= educe to a numeral. Baiscally it is a programming language but we don=E2=80= =99t know how to run the programs. This has been fixed now, by the work by = Thierry Ciquand and others on cubical type theory, which uses the cubical s= ets interpretation of HoTT to give a constrictive semantics which in turn c= an be used to design a normalisation procedure which does normalize correct= ly, in particular it reduces closed natural numbers to numerals. There is the remaining issue that it is not known whether the cubical theor= y coincides with the simplicial interpretation which is the standard one in= homotopy theory. 1. One of my favorite things about HoTT as a foundation for mathematics = actually comes just from DTT: Once you've formalized pi types, you can def= ine all of logic and (lots of) mathematics. But then the hierarchy of type= universes seem to require that we understand the natural numbers, which is= way more complicated than just pi types, and thus highly disappointing to = have to bring in at a foundational level. Am I right to be disappointed ab= out that or am I missing something? How do you do a lot of Mathematics without defining the natural numbers? Th= e problem with the predicative hierarchy of universes is rather that it is = rather clumsy in real life since everything you do is usually level polymor= phic. You can sort of put this under the carpet but actual implementations = of type theory haven=E2=80=99t yet found a good way to deal with this. Another issue with universes is that you always want more (they are like in= accessible cardinals in set theory). So for example you want to add a super= universe which is above all the universes in the predicative hierarchy and = so on. There has been some work investigating these universe hierarchies an= d the similarity with inaccessible cardinals is rather strong. Thorsten Thanks in advance for any help you have time and interest to provide! Nathan Carter -- 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/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com<= https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb0= 9-aa1cce32bcb2%40googlegroups.com?utm_medium=3Demail&utm_source=3Dfooter>. For more options, visit https://groups.google.com/d/optout. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment.=20 Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored=20 where permitted by law. --=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/C02F9858-5868-4447-B0C1-D1303A754F60%40exmail.nottingham= .ac.uk. For more options, visit https://groups.google.com/d/optout. --_000_C02F985858684447B0C1D1303A754F60exmailnottinghamacuk_ Content-Type: text/html; charset="UTF-8" Content-ID: <641849F06CD164498B4EC76921B4F78E@eurprd06.prod.outlook.com> Content-Transfer-Encoding: quoted-printable

Hi Nathan,

 

I can try to give answers but the answers you get ma= y depend on the person you ask.

  1. Very early in the HoTT book, it talks about the difference between types an= d sets, and says that HoTT encourages us to see sets as spaces.  Yet i= n a set of lecture videos Robert Harper did that I watched on YouTube (whic= h also seem to have disappeared, so I cannot link to them here), he said that Extensional Type Theory takes Intu= itionistic Type Theory in a different direction than HoTT does, formalizing= the idea that types are sets.  Why does the HoTT book not mention thi= s possibility?  Why does ETT not seem to get as much press as HoTT?

ETT or computational type theory relies on some notion of untyped = computation which is then sorted by defining some semantic criteria for typ= es. I prefer only to to talk about typed entities because they are the constructions which make sense and it should= n=E2=80=99t be necessary to refer to some untyped codes. However, this is m= y preference, I am sure Bob Harper views this differently. Also the semanti= c definitions refer to a rather unspecified meta theory, while in a type theory specified as the initial syntax of som= e kind of algebras you get a precise and 1st order definition wh= at exactly the theory and the models are.

  1. When that same text introduces judgmental equality, it claims that it is a = decidable relation.  It does not seem to prove this, and so I suspecte= d that perhaps the evidence was in Appendix A, where things are done more f= ormally (twice, even).  The first of these two formalisms places some restrictions on how one can introduce new= judgmental equalities, which seem sufficient to guarantee its decidability= , but at no point is an algorithm for deciding it given.  Is the algor= ithm simply to apply the only applicable rule over and over to reduce each side, and then compare for exact syntact= ic equality?

It is beyond the scope of the HoTT book to discuss the algorithm t= o decide definitional equality. There are a number of standard approaches t= o do this: you can normalize the terms in a syntactic way and use this to decide equality but then you need to pr= ove that the normalisation procedure actually terminates and is well behave= d wrt typing which isn=E2=80=99t trivial. Another approach is to use a cons= tructive semantical model to normalize (this is called normalisation by evaluation) but again this isn=E2=80=99t comple= tely trivial. The na=C3=AFve algorithm you suggest may not take care of eta= -equalities.

Moreover, the theory presented in the HoTT book has a serious prob= lem: extensionality principles like functional extensionality and univalenc= e are added as axioms, which have no place in type theory. Their presence destroys computational adequacy, whic= h means that a closed term of type Nat may not reduce to a numeral. Baiscal= ly it is a programming language but we don=E2=80=99t know how to run the pr= ograms. This has been fixed now, by the work by Thierry Ciquand and others on cubical type theory, which uses the = cubical sets interpretation of HoTT to give a constrictive semantics which = in turn can be used to design a normalisation procedure which does normaliz= e correctly, in particular it reduces closed natural numbers to numerals.

There is the remaining issue that it is not known whether the cubi= cal theory coincides with the simplicial interpretation which is the standa= rd one in homotopy theory.

  1. One of my favorite things about HoTT as a foundation for mathematics actual= ly comes just from DTT:  Once you've formalized pi types, you can defi= ne all of logic and (lots of) mathematics.  But then the hierarchy of = type universes seem to require that we understand the natural numbers, which is way more complicated than just pi types, and= thus highly disappointing to have to bring in at a foundational level.&nbs= p; Am I right to be disappointed about that or am I missing something?=

How do you do a lot of Mathematics without defining the natural nu= mbers? The problem with the predicative hierarchy of universes is rather th= at it is rather clumsy in real life since everything you do is usually level polymorphic. You can sort of put = this under the carpet but actual implementations of type theory haven=E2=80= =99t yet found a good way to deal with this.

Another issue with universes is that you always want more (they ar= e like inaccessible cardinals in set theory). So for example you want to ad= d a superuniverse which is above all the universes in the predicative hierarchy and so on. There has been some = work investigating these universe hierarchies and the similarity with inacc= essible cardinals is rather strong.

Thorsten

 

Thanks in advance for any help you have time and int= erest to provide!

 

Nathan Carter

 

--
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 Homo= topyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb0= 9-aa1cce32bcb2%40googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.


This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.=20

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored=20
where permitted by law.

--
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.go= ogle.com/d/msgid/HomotopyTypeTheory/C02F9858-5868-4447-B0C1-D1303A754F60%40= exmail.nottingham.ac.uk.
For more options, visit http= s://groups.google.com/d/optout.
--_000_C02F985858684447B0C1D1303A754F60exmailnottinghamacuk_--