From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.200.33.247 with SMTP id 52mr16474568qtz.50.1513550636896; Sun, 17 Dec 2017 14:43:56 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.200.46.200 with SMTP id i8ls6957933qta.11.gmail; Sun, 17 Dec 2017 14:43:55 -0800 (PST) X-Received: by 10.55.42.150 with SMTP id q22mr7142410qkq.11.1513550635762; Sun, 17 Dec 2017 14:43:55 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513550635; cv=none; d=google.com; s=arc-20160816; b=IO58JmLT0yBaNrCaESVyID3O1mCog5Lkpgxo7SQO4AzpZXLBoJpM8Z18ZAMQvgujiR DgAbxVqo7cJB8Hqhe8nhHyf6zgh1+4v43a1muLm1jzHz4JYmxyvVbKPDzGGQMWjZG1bP uZZGl0YIAIxPAouUfhljlqrZXNmVmEB1Q1pIVapYiGra0hOFtdIHZfEG9QK5T9Yhwiiu kDg2yv+m9JKKPlYd3mvirk41YbA0rKg+Gv91DpL4ApfEkf1uPJMlnTMVF6A7qTp/khhb nJh8TtIWLi9GTxfJMJkEJNnhQJQeraOBgjvS0uFVEYq2yJq4xtjP4bEZs7UN97yrBrd2 jB+Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=w/FRk5NC1HKE14aZIFPNnS+NZlDcIPGw37lJa0CME30=; b=vppOH7kEXPJoPjzEPjrI/iKgRIaga254E2O2xHr8DAY+WzqpGGDylx2l5RjNbzylFG u1GJuJbOYeZmpl+DRO/oYxKl+nMofqS7U4BJTFgO/WPBT/oL0DfMGpcgXsfKvo6YN1/S d4xrPiOTthY68m/WI+jwdv20InInjss/ZZ1tz7Yl4tq3rULylBbTVFP9JAKeZpN7HDKb qG0vu0Kf6wgCZaFPwR3vRsGzcm9rz0ZN5WdJyDNKBeTigw3ImEHcif3EVVLdW9QWX+O3 6fMKqS2od0efoW5OQxo/+A8Fkr7I55X6YZyUbLqGBzR6yYXde2ywy631GeG1oYyXcAbN KdXQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=Wu5ub7v2; spf=pass (google.com: domain of fpvd...@gmail.com designates 2607:f8b0:4001:c0b::242 as permitted sender) smtp.mailfrom=fpvd...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-it0-x242.google.com (mail-it0-x242.google.com. [2607:f8b0:4001:c0b::242]) by gmr-mx.google.com with ESMTPS id t9si601951qtg.3.2017.12.17.14.43.55 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 17 Dec 2017 14:43:55 -0800 (PST) Received-SPF: pass (google.com: domain of fpvd...@gmail.com designates 2607:f8b0:4001:c0b::242 as permitted sender) client-ip=2607:f8b0:4001:c0b::242; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=Wu5ub7v2; spf=pass (google.com: domain of fpvd...@gmail.com designates 2607:f8b0:4001:c0b::242 as permitted sender) smtp.mailfrom=fpvd...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-it0-x242.google.com with SMTP id z6so26210098iti.4 for ; Sun, 17 Dec 2017 14:43:55 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=w/FRk5NC1HKE14aZIFPNnS+NZlDcIPGw37lJa0CME30=; b=Wu5ub7v24DECZ9UK6w9ntT1PFSx28VzOLkMAaedLh9+QBN4unps+aEe8s3VvCTxly4 FRlrGTk6xPXbqBXLhgqRuDYNV4O3dtRF5IlmlptcpJAN8mK6WWuHsv5FCIIM1Gqcy19E w1hM4E7V5NOMrFVQkBBF6paerTlvWtHzaspJO90r+eVPoL2xm50TENEjMXQSatSdygLM v5NDPN9GH+W82IObVd4IJyIUwyKkuYdm+UYxmWJzWkwiy/b4bi19fb04wM8MvQA3nnCE WLV2E+pvuCGXxxlty7qnvBANQ2ibKPVJXjHZFmf2gJ+M05VXCSSidRDN/tSoVqNUGzVn AJ/A== X-Gm-Message-State: AKGB3mLiLKqVHrEaigSjH6mWBbWIR85awZ6nNutVSaZtHmArctYjZkHZ X2CtbN6CVdetYT0qkXI5RO7mNonvhqqGpFBAnvg= X-Received: by 10.36.108.212 with SMTP id w203mr17447602itb.148.1513550635104; Sun, 17 Dec 2017 14:43:55 -0800 (PST) MIME-Version: 1.0 Received: by 10.2.155.50 with HTTP; Sun, 17 Dec 2017 14:43:34 -0800 (PST) In-Reply-To: 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> <40D87932-BBF0-4CCF-A8D1-32E7A7BBFE5C@exmail.nottingham.ac.uk> From: Floris van Doorn Date: Sun, 17 Dec 2017 23:43:34 +0100 Message-ID: Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? To: Thorsten Altenkirch Cc: Ben Sherman , Michael Shulman , Homotopy Type Theory , Jeremy Avigad , Rob Lewis Content-Type: multipart/alternative; boundary="001a113f7a74f480a4056090f77d" --001a113f7a74f480a4056090f77d Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Just to clear some things up in this conversation: - The Lean kernel is consistent with any form of propositional extensionality, as far as I know. - The kernel for the current version of Lean, Lean 3, is not designed for HoTT and inconsistent with univalence. However, it does *not* ignore any transport of an equality. The bottom universe in Lean is the universe of propositions, Prop (not to be confused with hProp). What does hold is that there is definitional proof irrelevance for proofs of a proposition, i.e. if P : Prop and p, q : P then p is definitionally equal to q. This means that if we have a proof p : A =3D A for some type A, then transporting alon= g p is the identity function (because p =3D refl, definitionally). However, i= f p : A =3D B, then transporting along p is not the identity function (which would be type incorrect to state). - Lean has an evaluator in a virtual machine, which is used to evaluate programs and tactics efficiently outside the kernel. This evaluator is not trusted, and cannot be used when writing any proof in Lean. This evaluator removes all type information and propositions for efficiency, and can evaluate expressions to the wrong answer when axioms are added to the type theory (even if the axioms are consistent). For example, if we add the following lines to Ben's example ``` constant H : HProp_ext #eval Sig.fst (x H) ``` we see that the evaluator incorrectly evaluates this expression to tt (true). Needless to say, the evaluator was not designed for this, but instead to evaluate tactics like the following quickly. ``` if n < 1000000 then apply tactic1 else apply tactic2 ``` I hope this clears up any confusion. Best, Floris On 17 December 2017 at 18:16, Thorsten Altenkirch < Thorsten....@nottingham.ac.uk> wrote: > Thank you, Ben! That is good news actually. > > Thorsten > > From: Ben Sherman > Date: Sunday, 17 December 2017 at 18:08 > To: Michael Shulman > Cc: Thorsten Altenkirch , Homotopy Type > Theory > Subject: Re: [HoTT] Impredicative set + function extensionality + proof > irrelevance consistent? > > I don=E2=80=99t think that HProp extensionality is false in Lean (note th= at > regular Prop extensionality is an axiom that is taken to hold in Lean), o= r > at the least, I don=E2=80=99t think Thorsten=E2=80=99s argument goes thro= ugh. Here is Lean > code that formalizes the argument: > > structure HProp : Type (u + 1) :=3D > (car : Type u) > (subsingleton : =E2=88=80 x y : car, x =3D y) > > structure Sig {A : Type u} (P : A =E2=86=92 Prop) : Type u :=3D > (fst : A) > (snd : P fst) > > def Single {A : Type u} (a : A) : HProp :=3D > =E2=9F=A8 Sig (=CE=BB x : A, x =3D a) > , begin > intros, cases x, cases y, > subst snd, subst snd_1, > end > =E2=9F=A9 > > structure iffT (A B : Type u) :=3D > (left : A =E2=86=92 B) > (right : B =E2=86=92 A) > > def HProp_ext : Prop :=3D > =E2=88=80 (P Q : HProp.{u}), (iffT (HProp.car P) (HProp.car Q)) =E2=86= =92 P =3D Q > > def true_HProp : HProp.{u} :=3D =E2=9F=A8 punit , > begin intros, cases x, cases y, reflexivity end =E2=9F=A9 > > lemma Single_inh {A : Type u} (a : A) : HProp_ext.{u} =E2=86=92 Single > a =3D true_HProp :=3D > begin > intros H, > apply H, constructor; intros, > constructor, constructor, reflexivity, > end > > lemma Single_bool (H : HProp_ext.{0}) : Single tt =3D Single ff :=3D > begin > rw Single_inh, rw Single_inh, assumption, assumption, > end > > def x (H : HProp_ext.{0}) : > HProp.car (Single ff) :=3D > eq.rec_on (Single_bool H) =E2=9F=A8 tt, rfl =E2=9F=A9 > > lemma snd_x (H : HProp_ext.{0}) : Sig.fst (x H) =3D ff :=3D Sig.snd (x H) > > lemma fst_x (H : HProp_ext.{0}) : Sig.fst (x H) =3D tt :=3D begin > dsimp [x], admit, > end > > The proof state at the end of the proof for `fst_x` looks like this: > > =E2=8A=A2 (eq.rec {fst :=3D tt, snd :=3D _} _).fst =3D tt > > and `reflexivity` fails to solve the goal, so I think the `eq.rec` on the > left-hand side fails to reduce. Note that the equality proof that we > transport over is a proof that `Single tt =3D Single ff`; the two sides o= f > this equation are not definitionally equal, which I think explains why > `eq.rec` cannot reduce. > > On Dec 17, 2017, at 7:55 AM, Michael Shulman wrote: > > On Sat, Dec 16, 2017 at 7:21 AM, Thorsten Altenkirch > wrote: > > Not really: you can prove =C2=B3PropExt -> False=C2=B2 in the current sys= tem and you > shouldn=C2=B9t be able to do this. > > > Ah, I see. I didn't realize that PropExt was something you could > hypothesize inside of Lean; I thought you were proposing it as a > modification to the underlying type theory. In that case, yes, I > agree, the implementation is incorrect. (Are any Lean developers > listening?) > > By definitional proof-irrelevance I mean that we have a =C2=B3static=C2= =B2 universe > 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=C2=B9t prove =C2= =B3PropExt > -> False=C2=B2 in this system. > > One could argue that Lean=C2=B9s type theory is defined by its implementa= tion > but then it may be hard to say anything about it, including wether it is > consistent. > > I still wonder what exactly is the difference between a static > > )(efnitionally proof-irrelvant) Prop which seems to correspond to Omega i= n > 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. > > 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 > > 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" shu...@sandiego.edu> 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", because > 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=C2=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 turn= s > 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 a= t > 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 propositiona= l > extensionality, that is P,Q : Prop, (P <-> Q) <-> (P =3D Q), which is ind= eed > 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" > sojakova...@gmail.com> 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. > > > > > > > > > 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. > --001a113f7a74f480a4056090f77d Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Just to clear some things up in this conversation:
- The Lean kernel is consistent with any form of propositional = extensionality, as far as I know.
- The kernel for the current ve= rsion of Lean, Lean 3, is not designed for HoTT and inconsistent with univa= lence. However, it does *not* ignore any transport of an equality. The bott= om universe in Lean is the universe of propositions, Prop (not to be confus= ed with hProp). What does hold is that there is definitional proof irreleva= nce for proofs of a proposition, i.e. if P : Prop and p, q : P then p is de= finitionally equal to q. This means that if we have a proof p : A =3D A for= some type A, then transporting along p is the identity function (because p= =3D refl, definitionally). However, if p : A =3D B, then transporting alon= g p is not the identity function (which would be type incorrect to state).<= /div>
- Lean has an evaluator in a virtual machine, which is used to ev= aluate programs and tactics efficiently outside the kernel. This evaluator = is not trusted, and cannot be used when writing any proof in Lean. This eva= luator removes all type information and propositions for efficiency, and ca= n evaluate expressions to the wrong answer when axioms are added to the typ= e theory (even if the axioms are consistent). For example, if we add the fo= llowing lines to Ben's example
```
constant H = : HProp_ext
#eval Sig.fst (x H)
```
we = see that the evaluator incorrectly evaluates this expression to tt (true). = Needless to say, the evaluator was not designed for this, but instead to ev= aluate tactics like the following quickly.
```
if = n < 1000000 then apply tactic1 else apply tactic2
```

I hope this clears up any confusion.

<= /div>
Best,
Floris


On 17 December 2017 at 18:16, Tho= rsten Altenkirch <Thorsten....@nottingham.ac.uk>= wrote:
Thank you, Ben! That is good news actually.

Thorsten

From: Ben Sherman <she...@csail.mit.edu> Date: Sunday, 17 December 2017 at 1= 8:08
To: Michael Shulman <shu...@sandiego.edu> Cc: Thorsten Altenkirch <psz...@exmail.= nottingham.ac.uk>, Homotopy Type Theory <homotopytypetheory@goo= glegroups.com>
Subject: Re: [HoTT] Impredicative s= et + function extensionality + proof irrelevance consistent?

I don=E2=80=99t think that HProp extensionality is false in Lean (note that= regular Prop extensionality is an axiom that is taken to hold in Lean), or= at the least, I don=E2=80=99t think Thorsten=E2=80=99s argument goes throu= gh. Here is Lean code that formalizes the argument:

structure=C2=A0HProp=C2=A0:=C2=A0Type=C2=A0(u=C2=A0+=C2=A01)=C2= =A0:=3D
=C2=A0 (car :=C2=A0Type=C2=A0u)
=C2=A0 (subsingleton :=C2=A0=E2=88=80=C2=A0x y : car, x=C2=A0=3D=C2=A0y)
structure=C2=A0Sig=C2=A0{A :=C2=A0Type=C2=A0u} (P : A=C2=A0=E2=86=92=C2=A0P= rop) :=C2=A0Type=C2=A0u=C2=A0:=3D
=C2=A0 (fst : A)
=C2=A0 (snd : P fst)

def=C2=A0Single=C2=A0{A :=C2=A0Type=C2=A0u} (a : A) : HProp=C2=A0:=3D
=C2=A0 =E2=9F=A8 Sig (=CE=BB x : A, x=C2=A0=3D=C2=A0a)
=C2=A0 ,=C2=A0begin
=C2=A0 =C2=A0 intros, cases x, cases y,
=C2=A0 =C2=A0 subst snd, subst snd_1,
=C2=A0 =C2=A0=C2=A0end
=C2=A0 =E2=9F=A9

structure=C2=A0iffT=C2=A0(A B :=C2=A0Type=C2=A0u)=C2=A0:=3D
=C2=A0 (left : A=C2=A0=E2=86=92=C2=A0B)
=C2=A0 (right : B=C2=A0=E2=86=92=C2=A0A)

def=C2=A0HProp_ext=C2=A0:=C2=A0Prop=C2=A0:=3D
=C2=A0=C2=A0=E2=88=80=C2=A0(P Q : HProp.{u}), (iffT (HProp.car P) (HProp.ca= r Q))=C2=A0=E2=86=92=C2=A0P=C2=A0=3D=C2=A0Q

def=C2=A0true_HProp=C2=A0: HProp.{u}=C2=A0:=3D=C2=A0=E2=9F=A8 punit ,
=C2=A0=C2=A0begin=C2=A0intros, cases x, cases y, reflexivity=C2=A0end=C2=A0= =E2=9F=A9

lemma=C2=A0Single_inh=C2=A0{A :=C2=A0Type=C2=A0u} (a : A) : HProp_ext.{u}= =C2=A0=E2=86=92=C2=A0Single a=C2=A0=3D=C2=A0true_HProp=C2=A0:=3D
begin
intros H,
apply H, constructor; intros,
constructor, constructor, reflexivity,
end

lemma=C2=A0Single_bool=C2=A0(H : HProp_ext.{0}) : Single tt=C2=A0=3D=C2=A0S= ingle ff=C2=A0:=3D
begin
rw Single_inh, rw Single_inh, assumption, assumption,
end

def=C2=A0x=C2=A0(H : HProp_ext.{0}) :
=C2=A0 HProp.car (Single ff)=C2=A0:=3D
=C2=A0 eq.rec_on (Single_bool H) =E2=9F=A8 tt, rfl =E2=9F=A9

lemma=C2=A0snd_x=C2=A0(H : HProp_ext.{0}) : Sig.fst (x H)=C2=A0=3D=C2=A0ff= =C2=A0:=3D=C2=A0Sig.snd (x H)

lemma=C2=A0fst_x=C2=A0(H : HProp_ext.{0}) : Sig.fst (x H)=C2=A0=3D=C2=A0tt= =C2=A0:=3D=C2=A0begin
dsimp [x], admit,
end

The proof state at the end of the proof for `fst_x` looks like this:

=E2=8A=A2 (eq.rec {fst :=3D tt, snd :=3D _} _).fst =3D tt

and `reflexivity` fails to solve the goal, so I think the `eq.rec` on = the left-hand side fails to reduce. Note that the equality proof that we tr= ansport over is a proof that `Single tt =3D Single ff`; the two sides of th= is equation are not definitionally equal, which I think explains why `eq.rec` cannot reduce.

On Dec 17, 2017, at 7:55 AM, Michael Shulman <shu...@sandiego.edu> wrote:
On Sat, Dec 16, 2017 at 7:21 AM, Thorsten Altenkirch
<Thorsten.Altenkirch@nottingham.ac.u= k> wrote:
Not really: you can prove =C2=B3PropExt -> False=C2=B2 in the current sy= stem and you
shouldn=C2=B9t be able to do this.

Ah, I see.=C2=A0 I didn't realize that PropExt was something you could
hypothesize inside of Lean; I thought you were proposing it as a
modification to the underlying type theory.=C2=A0 In that case, yes, I
agree, the implementation is incorrect. =C2=A0(Are any Lean developers
listening?)

By definitional proof-irrelevance I mean that we have a =C2=B3static=C2=B2 = universe
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=C2=B9t prove =C2=B3= PropExt
-> False=C2=B2 in this system.

One could argue that Lean=C2=B9s type theory is defined by its implementati= on
but then it may be hard to say anything about it, including wether it is consistent.

I still wonder what exactly is the difference bet= ween a static
)(efnitionally proof-irrelvant) Prop which seems to correspond to Omega in<= br> 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.

=C2=A0=C2=A0=C2=A0A prime example of that "extra power" is that w= ith HProp you can prove
=C2=A0=C2=A0=C2=A0function comprehension (unique choice).=C2=A0 This goes a= long with a
=C2=A0=C2=A0=C2=A0reduction in the class of models: I believe that a static= Prop can
=C2=A0=C2=A0=C2=A0also be modeled by the strong-subobject classifier in a q= uasitopos, in
=C2=A0=C2=A0=C2=A0which 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

Ok, once we also allow QITs we know that this goe= s beyond the usual
topos logic (cf. the example in your paper with Peter).

Thorsten


On 12/12/2017, 23:14, "homotopytypetheory@googlegroups.com on behalf<= br>
of Michael Shulman" <homotopytypetheory@googlegroups.com on behalf= of
shu...@sandiego.ed= u> wrote:

=C2=A0=C2=A0=C2=A0This is really interesting.=C2=A0 It's true that all = toposes satisfy
both
=C2=A0=C2=A0=C2=A0unique choice and proof irrelev= ance.=C2=A0 I agree that one
interpretation
=C2=A0=C2=A0=C2=A0is that definitional proof-irre= levance is incompatible with the
=C2=A0=C2=A0=C2=A0HoTT-style *definition* of propositions as (-1)-truncated= types,
so
=C2=A0=C2=A0=C2=A0that you can *prove* something = is a proposition, rather than
having
=C2=A0=C2=A0=C2=A0"being a proposition"= being only a judgment.=C2=A0 But could we
instead
=C2=A0=C2=A0=C2=A0blame it on the unjustified omi= ssion of type annotations?
Morally, a
=C2=A0=C2=A0=C2=A0pairing constructor

=C2=A0=C2=A0=C2=A0(-,-) : (a:A) -> B(a) -> Sum(x:A) B(x)

=C2=A0=C2=A0=C2=A0ought really to be annotated with the types it acts on:
=C2=A0=C2=A0=C2=A0(-,-)^{(a:A). B(a)} : (a:A) -> B(a) -> Sum(x:A) B(x= )

=C2=A0=C2=A0=C2=A0and likewise the projection

=C2=A0=C2=A0=C2=A0first : (Sum(x:A) B(x)) -> A

=C2=A0=C2=A0=C2=A0should really be

=C2=A0=C2=A0=C2=A0first^{(a:A). B(a)} : (Sum(x:A) B(x)) -> A.

=C2=A0=C2=A0=C2=A0If we put these annotations in, then your "x" i= s

=C2=A0=C2=A0=C2=A0(true,refl)^{(b:Bool). true=3Db}

=C2=A0=C2=A0=C2=A0and your two apparently contradictory terms are

=C2=A0=C2=A0=C2=A0first^{(b:Bool). true=3Db} x =3D=3D true

=C2=A0=C2=A0=C2=A0and

=C2=A0=C2=A0=C2=A0second^{(b:Bool). false=3Db} x : first^{(b:Bool). false= =3Db} x =3D
false

=C2=A0=C2=A0=C2=A0And we don't have "first^{(b:Bool). false=3Db} x= =3D=3D true", because
=C2=A0=C2=A0=C2=A0beta-reduction requires the type annotations on the proje= ction
and the
=C2=A0=C2=A0=C2=A0pairing to match.=C2=A0 So it&#= 39;s not really the same "first x" that's
equal
=C2=A0=C2=A0=C2=A0to true as the one that's e= qual to false.

=C2=A0=C2=A0=C2=A0In many type theories, we can omit these annotations on p= airing
and
=C2=A0=C2=A0=C2=A0projection constructors because= they are uniquely inferrable.
But if
=C2=A0=C2=A0=C2=A0we end up in a type theory wher= e they are not uniquely
inferrable, we
=C2=A0=C2=A0=C2=A0are no longer justified in omit= ting them.


=C2=A0=C2=A0=C2=A0On Tue, Dec 12, 2017 at 4:21 AM, Thorsten Altenkirch
=C2=A0=C2=A0=C2=A0<Thorsten.Altenkirch@nottingham.ac.uk> wrote:
Good point.

OK, in a topos you have a static universe of propositions.
That is wether something is a proposition doesn=C2=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<= br> 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<= br> x /\ Pi y:A.P y -> x=3Dy then this is a proposition even though A may no= t
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"
<streicher@mathematik.tu-darmstadt.de> wrote:

But very topos is a model of extensional type the= ory when
taking Prop
=3D Omega. All elements of Prop are proof irrelev= ant 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 defin= itional
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<= br> 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" <sanz...@gmail.com>
wrote:

On Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenki= rch
<Thor= sten.Altenkirch@nottingham.ac.uk> 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<= br> extensionality, that is P,Q : Prop, (P <-> Q) <-> (P =3D Q), wh= ich is indeed
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 boole= ans would
support
both proof irrelevance and propositional extensio= nality,
classically
at least. Is there some extra assumption I am mis= sing here?


It should be possible to use a realizability sema= ntics
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,
"ho= motopytypetheory@googlegroups.com on behalf of Kristina Sojakova&q= uot;
<homo= topytypetheory@googlegroups.com on behalf of
sojakova...@gmai= l.com> wrote:

=C2=A0=C2=A0=C2=A0Dear all,

=C2=A0=C2=A0=C2=A0I asked this question last year on the coq-club
mailing list but did not
=C2=A0=C2=A0=C2=A0receive a conclusive answer so = I am trying here now.
Is the theory with
=C2=A0=C2=A0=C2=A0a proof-relevant impredicative = universe Set,
proof-irrelevant
=C2=A0=C2=A0=C2=A0impredicative universe Prop, an= d function
extensionality (known to be)
=C2=A0=C2=A0=C2=A0consistent? It is known that th= e proof-irrelevance of
Prop makes the Id
=C2=A0=C2=A0=C2=A0type behave differently usual a= nd in particular,
makes the theory
=C2=A0=C2=A0=C2=A0incompatible with univalence, s= o it is not just a
matter of tacking on
=C2=A0=C2=A0=C2=A0an interpretation for Prop.

=C2=A0=C2=A0=C2=A0Thanks in advance for any insight,

=C2=A0=C2=A0=C2=A0Kristina







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<= br>
immediately delete it.

Please do not use, copy or disclose the information
contained in this
message or in any attachment.=C2=A0 Any views or = opinions
expressed by the
author of this email do not necessarily reflect t= he views
of the
University of Nottingham.

This message has been checked for viruses but the
contents of an
attachment may still contain software viruses whi= ch 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.=C2=A0 Any views or = opinions
expressed by the
author of this email do not necessarily reflect t= he views of
the
University of Nottingham.

This message has been checked for viruses but the contents
of an
attachment may still contain software viruses whi= ch 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.=C2=A0 Any views or = opinions expressed
by the
author of this email do not necessarily reflect t= he views of
the
University of Nottingham.

This message has been checked for viruses but the contents of
an
attachment may still contain software viruses whi= ch 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 HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

=C2=A0=C2=A0=C2=A0--
=C2=A0=C2=A0=C2=A0You received this message because you are subscribed to t= he
Google Groups "Homotopy Type Theory" group.
=C2=A0=C2=A0=C2=A0To unsubscribe from this group = and stop receiving emails from
it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.
=C2=A0=C2=A0=C2=A0For 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.=C2=A0 Any views or opinions expressed by the<= br> 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 HomotopyTypeTheory+unsub...@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.=C2=A0 Any views or opinions expressed by the<= br> 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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to Ho= motopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--=C2=A0
You received this message because you are subscribed to the Google Groups &quo= t;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an ema= il to=C2=A0HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit=C2=A0https://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.=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.

--
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+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--001a113f7a74f480a4056090f77d--