I don’t 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’t think Thorsten’s argument goes through. Here is Lean code that formalizes the argument: structure HProp : Type (u + 1) := (car : Type u) (subsingleton : ∀ x y : car, x = y) structure Sig {A : Type u} (P : A → Prop) : Type u := (fst : A) (snd : P fst) def Single {A : Type u} (a : A) : HProp := ⟨ Sig (λ x : A, x = a) , begin intros, cases x, cases y, subst snd, subst snd_1, end ⟩ structure iffT (A B : Type u) := (left : A → B) (right : B → A) def HProp_ext : Prop := ∀ (P Q : HProp.{u}), (iffT (HProp.car P) (HProp.car Q)) → P = Q def true_HProp : HProp.{u} := ⟨ punit , begin intros, cases x, cases y, reflexivity end ⟩ lemma Single_inh {A : Type u} (a : A) : HProp_ext.{u} → Single a = true_HProp := begin intros H, apply H, constructor; intros, constructor, constructor, reflexivity, end lemma Single_bool (H : HProp_ext.{0}) : Single tt = Single ff := begin rw Single_inh, rw Single_inh, assumption, assumption, end def x (H : HProp_ext.{0}) : HProp.car (Single ff) := eq.rec_on (Single_bool H) ⟨ tt, rfl ⟩ lemma snd_x (H : HProp_ext.{0}) : Sig.fst (x H) = ff := Sig.snd (x H) lemma fst_x (H : HProp_ext.{0}) : Sig.fst (x H) = tt := begin dsimp [x], admit, end The proof state at the end of the proof for `fst_x` looks like this: ⊢ (eq.rec {fst := tt, snd := _} _).fst = 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 = Single ff`; the two sides of 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 ³PropExt -> False² in the current system and you >> shouldn¹t 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 ³static² 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¹t prove ³PropExt >> -> False² in this system. >> >> One could argue that Lean¹s type theory is defined by its implementation >> 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 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. >> >> 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=b} >>> >>> and your two apparently contradictory terms are >>> >>> first^{(b:Bool). true=b} x == true >>> >>> and >>> >>> second^{(b:Bool). false=b} x : first^{(b:Bool). false=b} x = >> false >>> >>> And we don't have "first^{(b:Bool). false=b} x == 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¹t 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=y 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 >>>>> = 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) = Sigma x:A.a=x. We have >> Single(a) : Prop and >>>>>> >>>>>> p : Single(true) <-> Single(false) >>>>>> >>>>>> since both are inhabited. Hence by extProp >>>>>> >>>>>> extProp p : Single(true) = Single(false) >>>>>> >>>>>> now we can use transport on (true,refl) : Single(true) to >> obtain >>>>>> >>>>>> x = (extProp p)*(true,refl) : Single(false) >>>>>> >>>>>> and we can show that >>>>>> >>>>>> second x : first x = false >>>>>> >>>>>> but since Lean computationally ignores (extProp p)* we also >> get (definitionally): >>>>>> >>>>>> first x == 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 = Q), which 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 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 .