From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.80.244.178 with SMTP id s47mr5115998edm.6.1513437672029; Sat, 16 Dec 2017 07:21:12 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.80.144.196 with SMTP id d4ls4560201eda.4.gmail; Sat, 16 Dec 2017 07:21:10 -0800 (PST) X-Received: by 10.80.142.245 with SMTP id x50mr5111963edx.0.1513437670621; Sat, 16 Dec 2017 07:21:10 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513437670; cv=none; d=google.com; s=arc-20160816; b=qVKY0jRJy0LD5mMB/M8VUNND+fm8ESLu/mF6Qhvoa/A/cUPVbjFOCGJArJLJTapre/ 1FddHR4osTfdrJwjQxlprQO0r/HyfJMFaOPUvK0uLH4q9+7kdm8IK5iTdGpgZymWpp88 U06VC47han16wjA0p/dOGR6Bhuko6t/hYe0mlSCRhiAKU+ldSDvtOqx3pg2pmG3lEPW3 6SR/ouz5hdZwfYZX3ivuifqNfrkwLYPFvV37bbflvp/q16mBL4BhEAISfBtEDiKQxnqh QSR9ruks6PKXDTio3AS7gSJVWXBbLzTO5rmW/uxg5qT9VQMu2PIACzaL+fRmuF36X9QL pFqg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-id :spamdiagnosticmetadata:spamdiagnosticoutput:user-agent :content-language:accept-language:references:message-id:date :thread-index:thread-topic:subject:cc:to:from :arc-authentication-results; bh=zHbjfiCBcGHF5YNXQ2NC1D9dROu0Fq/YkF6uCphMqY8=; b=zWa29+1gsZLqTP4Zb9MMdSgEssH80BLmj+Z+Mgc6KH2KSsN/+rMj7zJ8pZmqpPPwpS 9y0j3+PbkrvKH5EtpwbrlXMzNs8DqxTVx5JKFSsKTFnRCUsWT6TWzXH9p4kaDYVhDxKZ AfJNog1Uckjbmgk9cfPBfkWXAi7Hzgv3dpxKA4blhlTR6tKp1twzPdM4t1npT4UhggGJ jvD/1lQmqPHZZ3FGD5rtQFxUC891B2KxlBss3U9D0Kz2M4YWf1DO2M9b8inPb8k8LnQI DOXLJaOv3Z8ixX3lkS9QQzKAhlyuHQ28gRkIO5Nuwwx+c5DUczvTUUkjFwNMVYiCvWWH ucQw== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten....@nottingham.ac.uk designates 128.243.43.128 as permitted sender) smtp.mailfrom=Thorsten....@nottingham.ac.uk Return-Path: Received: from uidappmx05.nottingham.ac.uk (uidappmx05.nottingham.ac.uk. [128.243.43.128]) by gmr-mx.google.com with ESMTP id r58si1130771eda.3.2017.12.16.07.21.10 for ; Sat, 16 Dec 2017 07:21:10 -0800 (PST) Received-SPF: pass (google.com: domain of thorsten....@nottingham.ac.uk designates 128.243.43.128 as permitted sender) client-ip=128.243.43.128; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of thorsten....@nottingham.ac.uk designates 128.243.43.128 as permitted sender) smtp.mailfrom=Thorsten....@nottingham.ac.uk Received: from uidappmx05.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 3F86B8358E1_A3539E6B for ; Sat, 16 Dec 2017 15:21:10 +0000 (GMT) Received: from smtp4.nottingham.ac.uk (smtp4.nottingham.ac.uk [128.243.220.65]) by uidappmx05.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id D8A95789B0F_A3539E5F for ; Sat, 16 Dec 2017 15:21:09 +0000 (GMT) Received: from uiwexhub03.is.nottingham.ac.uk ([128.243.15.146] helo=UIWEXHUB03.ad.nottingham.ac.uk) by smtp4.nottingham.ac.uk with esmtps (TLSv1:AES128-SHA:128) (Exim 4.85) (envelope-from ) id 1eQEGz-0001LS-RY; Sat, 16 Dec 2017 15:21:09 +0000 Received: from EUR01-DB5-obe.outbound.protection.outlook.com (213.199.154.183) by mail.nottingham.ac.uk (128.243.15.146) with Microsoft SMTP Server (TLS) id 14.3.351.0; Sat, 16 Dec 2017 15:21:09 +0000 Received: from DB5PR06MB1717.eurprd06.prod.outlook.com (10.165.213.15) by DB5PR06MB1717.eurprd06.prod.outlook.com (10.165.213.15) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384_P256) id 15.20.302.9; Sat, 16 Dec 2017 15:21:07 +0000 Received: from DB5PR06MB1717.eurprd06.prod.outlook.com ([fe80::51a3:6727:473b:460e]) by DB5PR06MB1717.eurprd06.prod.outlook.com ([fe80::51a3:6727:473b:460e%14]) with mapi id 15.20.0302.017; Sat, 16 Dec 2017 15:21:07 +0000 From: Thorsten Altenkirch To: Michael Shulman CC: Homotopy Type Theory Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? Thread-Topic: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? Thread-Index: AQHTcje6ntODVCgsJUW7bijhlNm7RQ== Date: Sat, 16 Dec 2017 15:21:07 +0000 Message-ID: <40D87932-BBF0-4CCF-A8D1-32E7A7BBFE5C@exmail.nottingham.ac.uk> References: <4c4fe126-f429-0c82-25e8-80bfb3a0ac78@gmail.com> <11CC10D7-7853-48E7-88BD-42A8EFD47998@exmail.nottingham.ac.uk> <20171212120233.GA32661@mathematik.tu-darmstadt.de> <643DFB5A-10F8-467F-AC3A-46D4BC938E85@exmail.nottingham.ac.uk> Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/14.5.7.151005 authentication-results: spf=none (sender IP is ) smtp.mailfrom=psz...@exmail.nottingham.ac.uk; x-originating-ip: [82.31.58.108] x-ms-publictraffictype: Email x-microsoft-exchange-diagnostics: 1;DB5PR06MB1717;6:XKs+UDhzKX9rS3SML5iP97wXP5VM6HU8Pcmj1UeMgo7qS4qEZSpqQQjhfpd0ITxGvrVHA5iQsYLd/ccyKwsFJoW0vAWG59+2FXwy5Bi8UhVpFy1JjJ2B6Bleb+k/czhza2NSVnXEWU+K3v3bWp7zkxUf3uic9u4f3Hc5y5DSZFgluWEFrS/c4p8AOJdMI13YJQVDtMS/dqRTDMWBYViw8Pxmx+OLH2hPUivdWvgeaj7781+OD5CTghT+LmnpnJJ/jYNOuBup77qbfCjEz0v1JCPNcLk0FFs02cRFpgvGcNt3bdNtbGRIjf4U3zr1vd+jHq6JBjL3SyqrlfGUyoJvM1Z7IlJcmgSCPDnA3bp7U10=;5:JRHiFYsuWnI4ESd2nAVc8ZId9FqWpVKXu3bPdPT2FT41OKVQlLUT77lLXq/38d5GPHMM5IcmrKPpmvUKzISyy9YHqWhLIyHiDBvIi/fZxrctT2FSYiQQzR3Q+BvPY9aKM/56o/7W55Ac1wM/GBLoCUwK6xdBIuO7p8DqDbeW0tw=;24:N/e+1gbURcVeddJUhqYdHBiVgcXNOZfxyYaAIWNwI80uS0i47/4PMvYk3mwVHjrVFCw/QqJXMOb/7iB9t66cJQWq3+nLu05lLc/WovScUUM=;7:OYLxDVnsoNjbYOCpNUJD2JPl9h0zpxxsE7PBkZ/Xv4kQNXER5krO9re+BwfCykoJVZZkpJVBfnf6wLIkkUNJRR/n+TRibavLMnNYEh7jwEHStU4Qj3CYWIBIlwZqQY3y1uJztIzQsO3c6l/itpC/smg/kbpCNolEU2MvdyWOmjIGu7vhTrWv1He8hzOL6DY+1lliAI9p4rHbyY4LqwxIdUIlQhmSiajSmJkQZLTqnqf+jfOP71GHBqJ6sSVYbJt3 x-ms-exchange-antispam-srfa-diagnostics: SSOS; x-ms-office365-filtering-correlation-id: d6314a50-f6b3-4d94-c90c-08d54498a18a x-microsoft-antispam: UriScan:;BCL:0;PCL:0;RULEID:(5600026)(4604075)(4534020)(4602075)(4627115)(201703031133081)(201702281549075)(2017052603307);SRVR:DB5PR06MB1717; x-ms-traffictypediagnostic: DB5PR06MB1717: x-microsoft-antispam-prvs: x-exchange-antispam-report-test: UriScan:(215639381216008)(228788266533470)(131327999870524)(211936372134217)(214861330456307)(155532106045638); x-exchange-antispam-report-cfa-test: BCL:0;PCL:0;RULEID:(6040450)(2401047)(5005006)(8121501046)(3231023)(920507027)(93006095)(93001095)(3002001)(10201501046)(6041248)(20161123564025)(201703131423075)(201702281529075)(201702281528075)(201703061421075)(201703061406153)(20161123555025)(20161123562025)(20161123558100)(20161123560025)(6072148)(201708071742011);SRVR:DB5PR06MB1717;BCL:0;PCL:0;RULEID:(100000803101)(100110400095);SRVR:DB5PR06MB1717; x-forefront-prvs: 0523CF0711 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(346002)(396003)(376002)(366004)(39860400002)(51874003)(24454002)(189003)(199004)(25786009)(45080400002)(786003)(316002)(966005)(5890100001)(3280700002)(105586002)(53946003)(83716003)(106356001)(2900100001)(8936002)(93886005)(478600001)(3660700001)(66066001)(58126008)(5660300001)(82746002)(6512007)(6306002)(2906002)(6246003)(229853002)(8676002)(68736007)(74482002)(83506002)(81166006)(42882006)(2171002)(81156014)(33656002)(6916009)(99286004)(86362001)(6486002)(14454004)(5250100002)(6506007)(53546011)(53936002)(4326008)(102836003)(3846002)(7736002)(6116002)(76176011)(34040400001)(59450400001)(305945005)(97736004)(6436002)(42522002)(42262002);DIR:OUT;SFP:1102;SCL:1;SRVR:DB5PR06MB1717;H:DB5PR06MB1717.eurprd06.prod.outlook.com;FPR:;SPF:None;PTR:InfoNoRecords;MX:1;A:1;LANG:en; received-spf: None (protection.outlook.com: exmail.nottingham.ac.uk does not designate permitted sender hosts) spamdiagnosticoutput: 1:99 spamdiagnosticmetadata: NSPM Content-Type: text/plain; charset="iso-8859-1" Content-ID: <7E592FFFCBD14E44...@eurprd06.prod.outlook.com> Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: d6314a50-f6b3-4d94-c90c-08d54498a18a X-MS-Exchange-CrossTenant-originalarrivaltime: 16 Dec 2017 15:21:07.7488 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-Transport-CrossTenantHeadersStamped: DB5PR06MB1717 X-OriginatorOrg: exmail.nottingham.ac.uk X-Spam-Note: SpamAssassin run bypassed due to message size On 14/12/2017, 18:52, "Michael Shulman" wrote: On Thu, Dec 14, 2017 at 4:32 AM, Thorsten Altenkirch wrote: > Excellent observation! So basically the implementation of Lean is incorrect because we shouldn=B9t be able to derive true =3D false from the assumption of propositional extensionality if we take account of the type annotations. > > The example arose from the question whether we can add propositional extensionality to Lean. That s we define HProp =3D Sigma P:Type.Pi x,y.P.x=3Dy. Note that the equality we use here is the static Prop valued equality. Now I suggested to add propositional extensionality for HProp as an axiom to Lean but it seemed to lead to the problem. =20 Well, if I understand you correctly, it sounds like the implementation of Lean isn't *currently* incorrect -- omitting such type annotations is a perfectly fine optimization for implementations of most type theories. It's just that it would have to be modified in order to *remain* correct under the addition of propositional extensionality for HProp. Right? Not really: you can prove =B3PropExt -> False=B2 in the current system and = you shouldn=B9t be able to do this. By definitional proof-irrelevance I mean that we have a =B3static=B2 univer= se of propositions and the principle that any tow proofs of propositions are definitionally equal. That is what I suggested in my LICS 99 paper. However, it seems (following your comments) that we can=B9t prove =B3PropEx= t -> False=B2 in this system. One could argue that Lean=B9s type theory is defined by its implementation but then it may be hard to say anything about it, including wether it is consistent. =20 > I still wonder what exactly is the difference between a static )(efnitionally proof-irrelvant) Prop which seems to correspond to Omega in a topos and set-level HoTT (i.e. using HProp). Hprop is also a subobject classifier (with some predicativity proviso) but the HoTT view gives you some extra power. =20 A prime example of that "extra power" is that with HProp you can prove function comprehension (unique choice). This goes along with a reduction in the class of models: I believe that a static Prop can also be modeled by the strong-subobject classifier in a quasitopos, in which case unique choice is false. Ok, so you are saying that a static Prop only gives rise to a quasitopos which fits with the observation that we don't get unique choice in this case. On the other hand set level HoTT gives rise to a topos? Thorsten =20 > Ok, once we also allow QITs we know that this goes beyond the usual topos logic (cf. the example in your paper with Peter). > > Thorsten > > > On 12/12/2017, 23:14, "homotopyt...@googlegroups.com on behalf of Michael Shulman" wrote: > > This is really interesting. It's true that all toposes satisfy both > unique choice and proof irrelevance. I agree that one interpretation > is that definitional proof-irrelevance is incompatible with the > HoTT-style *definition* of propositions as (-1)-truncated types, so > that you can *prove* something is a proposition, rather than having > "being a proposition" being only a judgment. But could we instead > blame it on the unjustified omission of type annotations? Morally, a > pairing constructor > > (-,-) : (a:A) -> B(a) -> Sum(x:A) B(x) > > ought really to be annotated with the types it acts on: > > (-,-)^{(a:A). B(a)} : (a:A) -> B(a) -> Sum(x:A) B(x) > > and likewise the projection > > first : (Sum(x:A) B(x)) -> A > > should really be > > first^{(a:A). B(a)} : (Sum(x:A) B(x)) -> A. > > If we put these annotations in, then your "x" is > > (true,refl)^{(b:Bool). true=3Db} > > and your two apparently contradictory terms are > > first^{(b:Bool). true=3Db} x =3D=3D true > > and > > second^{(b:Bool). false=3Db} x : first^{(b:Bool). false=3Db} x = =3D false > > And we don't have "first^{(b:Bool). false=3Db} x =3D=3D true", be= cause > beta-reduction requires the type annotations on the projection and the > pairing to match. So it's not really the same "first x" that's equal > to true as the one that's equal to false. > > In many type theories, we can omit these annotations on pairing and > projection constructors because they are uniquely inferrable. But if > we end up in a type theory where they are not uniquely inferrable, we > are no longer justified in omitting them. > > > On Tue, Dec 12, 2017 at 4:21 AM, Thorsten Altenkirch > wrote: > > Good point. > > > > OK, in a topos you have a static universe of propositions. That is wether something is a proposition doesn=B9t depend on other assumptions you make. > > > > In set-level HoTT we define Prop as the types which have at most one inhabitant. Now wether a type is a proposition may depend on other assumptions. (-1)-univalence i.e. propositional extensionality turns Prop into a subobject classifier (if you have resizing otherwise you get some sort of predicative topos). > > > > However, the dynamic interpretation of propositions gives you some additional power, in particular you can proof unique choice, because if you can prove Ex! x:A.P x , where Ex! x:A.P x is defined as Sigma x:A.P x /\ Pi y:A.P y -> x=3Dy then this is a proposition even though A may not be. However using projections you also get Sigma x:A.P x. > > > > Hence I guess I should have said a topos with unique choice (I am not sure wether this is enough). Btw, set-level HoTT also gives you QITs which eliminate many uses of choice (e.g. the definition of the Cauchy Reals and the partiality monad). > > > > Thorsten > > > > > > > > > > > > > > On 12/12/2017, 12:02, "Thomas Streicher" wrote: > > > >>But very topos is a model of extensional type theory when taking Prop > >>=3D Omega. All elements of Prop are proof irrelevant and equivalent > >>propositions are equal. > >> > >>Since it is a model of extensional TT there is no difference between > >>propsoitional and judgemental equality. > >> > >>Thomas > >> > >> > >>> If you have proof-irrelevance in the strong definitional sense then you cannot be in a topos. This came up recently in the context of Lean which is a type-theory based interactive proof system developed at microsoft and which does implement proof-irrelvance. Note that any topos has extProp: > >>> > >>> Given a:A define Single(a) =3D Sigma x:A.a=3Dx. We have Single(a) : Prop and > >>> > >>> p : Single(true) <-> Single(false) > >>> > >>> since both are inhabited. Hence by extProp > >>> > >>> extProp p : Single(true) =3D Single(false) > >>> > >>> now we can use transport on (true,refl) : Single(true) to obtain > >>> > >>> x =3D (extProp p)*(true,refl) : Single(false) > >>> > >>> and we can show that > >>> > >>> second x : first x =3D false > >>> > >>> but since Lean computationally ignores (extProp p)* we also get (definitionally): > >>> > >>> first x =3D=3D true > >>> > >>> My conclusion is that strong proof-irrelvance is a bad idea (note that my ???99 paper on Extensionality in Intensional Type Theory used exactly this). It is more important that our core theory is extensional and something pragmatically close to definitional proof-irrelevance can be realised as some tactic based sugar. It has no role in a foundational calculus. > >>> > >>> > >>> Thorsten > >>> > >>> > >>> > >>> > >>> On 12/12/2017, 10:15, "Andrea Vezzosi" wrote: > >>> > >>> >On Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenkirch > >>> > wrote: > >>> >> Hi Kristina, > >>> >> > >>> >> I guess you are not assuming Prop:Set because that would be System U and hence inconsistent. > >>> >> > >>> >> By proof-irrelevance I assume that you mean that any two inhabitants of a proposition are definitionally equal. This assumption is inconsistent with it being a tops since in any Topos you get propositional extensionality, that is P,Q : Prop, (P <-> Q) <-> (P =3D Q), which is indee= d an instance of univalence. > >>> >> > >>> > > >>> >I don't know if it's relevant to the current discussion, but I thought > >>> >the topos of sets with Prop taken to be the booleans would support > >>> >both proof irrelevance and propositional extensionality, classically > >>> >at least. Is there some extra assumption I am missing here? > >>> > > >>> > > >>> >> It should be possible to use a realizability semantics like omega-sets or Lambda-sets to model the impredicative theory and identify the propositions with PERs that are just subsets. > >>> >> > >>> >> Cheers, > >>> >> Thorsten > >>> >> > >>> >> > >>> >> On 11/12/2017, 04:22, "homotopyt...@googlegroups.com on behalf of Kristina Sojakova" wrote: > >>> >> > >>> >> Dear all, > >>> >> > >>> >> I asked this question last year on the coq-club mailing list but did not > >>> >> receive a conclusive answer so I am trying here now. Is the theory with > >>> >> a proof-relevant impredicative universe Set, proof-irrelevant > >>> >> impredicative universe Prop, and function extensionality (known to be) > >>> >> consistent? It is known that the proof-irrelevance of Prop makes the Id > >>> >> type behave differently usual and in particular, makes the theory > >>> >> incompatible with univalence, so it is not just a matter of tacking on > >>> >> an interpretation for Prop. > >>> >> > >>> >> Thanks in advance for any insight, > >>> >> > >>> >> Kristina > >>> >> > >>> >> > >>> >> > >>> >> > >>> >> > >>> >> > >>> >> > >>> >> 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 send it back to me, and immediately delete it. > >>> >> > >>> >> Please do not use, copy or disclose the information contained in this > >>> >> message or in any attachment. Any views or opinions expressed by the > >>> >> author of this email do not necessarily reflect the views of the > >>> >> University of Nottingham. > >>> >> > >>> >> This message has been checked for viruses but the contents of an > >>> >> attachment may still contain software viruses which could damage your > >>> >> computer system, you are advised to perform your own checks. Email > >>> >> communications with the University of Nottingham may be monitored as > >>> >> permitted by UK legislation. > >>> >> > >>> > >>> > >>> > >>> > >>> 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 send it back to me, and immediately delete it. > >>> > >>> Please do not use, copy or disclose the information contained in this > >>> message or in any attachment. Any views or opinions expressed by the > >>> author of this email do not necessarily reflect the views of the > >>> University of Nottingham. > >>> > >>> This message has been checked for viruses but the contents of an > >>> attachment may still contain software viruses which could damage your > >>> computer system, you are advised to perform your own checks. Email > >>> communications with the University of Nottingham may be monitored as > >>> permitted by UK legislation. > >>> > > > > > > > > > > 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 send it back to me, and immediately delete it. > > > > Please do not use, copy or disclose the information contained in this > > message or in any attachment. Any views or opinions expressed by the > > author of this email do not necessarily reflect the views of the > > University of Nottingham. > > > > This message has been checked for viruses but the contents of an > > attachment may still contain software viruses which could damage your > > computer system, you are advised to perform your own checks. Email > > communications with the University of Nottingham may be monitored as > > permitted by UK legislation. > > > > -- > > 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 HomotopyTypeThe...@googlegroups.com. > > For more options, visit https://groups.google.com/d/optout. > > -- > 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 HomotopyTypeThe...@googlegroups.com. > 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 send it back to me, and immediately delete it. > > Please do not use, copy or disclose the information contained in this > message or in any attachment. Any views or opinions expressed by the > author of this email do not necessarily reflect the views of the > University of Nottingham. > > This message has been checked for viruses but the contents of an > attachment may still contain software viruses which could damage your > computer system, you are advised to perform your own checks. Email > communications with the University of Nottingham may be monitored as > permitted by UK legislation. > > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. =20 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 send it back to me, and immediately delete it.=20 Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. This message has been checked for viruses but the contents of an attachment may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.