* Impredicative set + function extensionality + proof irrelevance consistent? @ 2017-12-11 4:22 Kristina Sojakova 2017-12-11 11:42 ` [HoTT] " Jon Sterling 2017-12-11 14:23 ` Thorsten Altenkirch 0 siblings, 2 replies; 54+ messages in thread From: Kristina Sojakova @ 2017-12-11 4:22 UTC (permalink / raw) To: Homotopy Type Theory 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 ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-11 4:22 Impredicative set + function extensionality + proof irrelevance consistent? Kristina Sojakova @ 2017-12-11 11:42 ` Jon Sterling 2017-12-11 12:15 ` Kristina Sojakova 2017-12-11 14:23 ` Thorsten Altenkirch 1 sibling, 1 reply; 54+ messages in thread From: Jon Sterling @ 2017-12-11 11:42 UTC (permalink / raw) To: HomotopyTypeTheory Can we make sense of this by interpreting into a realizability topos? In particular, I am under the impression that Eff (the effective topos) models an impredicative universe of proof-relevant types, and on the other hand its subobject classifier can be used to model a proof-irrelevant Prop. As a topos, Eff models extensional type theory, and thence we have the functional extensionality law. Best, Jon On Sun, Dec 10, 2017, at 08:22 PM, 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 > > -- > 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-11 11:42 ` [HoTT] " Jon Sterling @ 2017-12-11 12:15 ` Kristina Sojakova 2017-12-11 12:43 ` Jon Sterling 0 siblings, 1 reply; 54+ messages in thread From: Kristina Sojakova @ 2017-12-11 12:15 UTC (permalink / raw) To: HomotopyTypeTheory Hi Jon, Thanks for the answer! In this model, what would be the interpretation of the eq_A(a,b) : Prop type in Coq, which is logically equivalent to Id_A(a,b) : Type but proof irrelevant? Best, Kristina On 12/11/2017 6:42 AM, Jon Sterling wrote: > Can we make sense of this by interpreting into a realizability topos? > > In particular, I am under the impression that Eff (the effective topos) > models an impredicative universe of proof-relevant types, and on the > other hand its subobject classifier can be used to model a > proof-irrelevant Prop. > > As a topos, Eff models extensional type theory, and thence we have the > functional extensionality law. > > Best, > Jon > > > On Sun, Dec 10, 2017, at 08:22 PM, 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 >> >> -- >> 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-11 12:15 ` Kristina Sojakova @ 2017-12-11 12:43 ` Jon Sterling 2017-12-11 14:28 ` Thomas Streicher 0 siblings, 1 reply; 54+ messages in thread From: Jon Sterling @ 2017-12-11 12:43 UTC (permalink / raw) To: HomotopyTypeTheory Hi Kristina, If you are using the subobject classifier to model Prop, I think that you can just use the ordinary equality predicate of the topos logic. The equality predicate for a type 'A' is given by the (generalized/Lawvere-style) existential quantification along the diagonal "δ : X -> X * X". I think this ought to be the same as alternatively first constructing the identity type in the proof-relevant fragment and then reflecting it into the subobject classifier, since toposes model extensional identity types. Best, Jon On Mon, Dec 11, 2017, at 04:15 AM, Kristina Sojakova wrote: > Hi Jon, > > Thanks for the answer! In this model, what would be the interpretation > of the eq_A(a,b) : Prop type in Coq, which is logically equivalent to > Id_A(a,b) : Type but proof irrelevant? > > Best, > > Kristina > > > On 12/11/2017 6:42 AM, Jon Sterling wrote: > > Can we make sense of this by interpreting into a realizability topos? > > > > In particular, I am under the impression that Eff (the effective topos) > > models an impredicative universe of proof-relevant types, and on the > > other hand its subobject classifier can be used to model a > > proof-irrelevant Prop. > > > > As a topos, Eff models extensional type theory, and thence we have the > > functional extensionality law. > > > > Best, > > Jon > > > > > > On Sun, Dec 10, 2017, at 08:22 PM, 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 > >> > >> -- > >> 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-11 12:43 ` Jon Sterling @ 2017-12-11 14:28 ` Thomas Streicher 2017-12-11 14:32 ` Kristina Sojakova 0 siblings, 1 reply; 54+ messages in thread From: Thomas Streicher @ 2017-12-11 14:28 UTC (permalink / raw) To: Jon Sterling; +Cc: HomotopyT... It's amazing how common knoledge from late 80s can disappeear easily. For interpreting Coq one uses Asm(A), assemblies over a pca A, Set is interpreted as modest sets and Prop as subterminal modest sets. It's important to take Asm(A) instead of the realizability topos for showing that Set is internally complete in a sufficiently strong sense. (See Ed Robinson's old LICS paper "How Complete is PER?"). Of course, these models don't validate UA but they were not meant to be. Id takes values in Prop and is isomorphic to Leibniz equality. See work from the 80s by Martin Hyland, myself and a few others. Thomas ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-11 14:28 ` Thomas Streicher @ 2017-12-11 14:32 ` Kristina Sojakova 0 siblings, 0 replies; 54+ messages in thread From: Kristina Sojakova @ 2017-12-11 14:32 UTC (permalink / raw) To: HomotopyTypeTheory Hi Thomas, Thank you for the answer! You wrote: "Id takes values in Prop and is isomorphic to Leibniz equality." That would be what coq calls "eq". But what is the interpretation of the proof-relevant identity type "Id", which takes values in Type? For my theory I want both. Kristina > > See work from the 80s by Martin Hyland, myself and a few others. > > Thomas > ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-11 4:22 Impredicative set + function extensionality + proof irrelevance consistent? Kristina Sojakova 2017-12-11 11:42 ` [HoTT] " Jon Sterling @ 2017-12-11 14:23 ` Thorsten Altenkirch 2017-12-12 10:15 ` Andrea Vezzosi 1 sibling, 1 reply; 54+ messages in thread From: Thorsten Altenkirch @ 2017-12-11 14:23 UTC (permalink / raw) To: Kristina Sojakova, Homotopy Type Theory 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. 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" <homotopyt...@googlegroups.com on behalf of 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 -- 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-11 14:23 ` Thorsten Altenkirch @ 2017-12-12 10:15 ` Andrea Vezzosi 2017-12-12 11:03 ` Thorsten Altenkirch 0 siblings, 1 reply; 54+ messages in thread From: Andrea Vezzosi @ 2017-12-12 10:15 UTC (permalink / raw) To: Thorsten Altenkirch; +Cc: Kristina Sojakova, Homotopy Type Theory On Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenkirch <Thorsten....@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 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" <homotopyt...@googlegroups.com on behalf of 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 > > -- > 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-12 10:15 ` Andrea Vezzosi @ 2017-12-12 11:03 ` Thorsten Altenkirch 2017-12-12 12:02 ` Thomas Streicher [not found] ` <fa8c0c3c-4870-4c06-fd4d-70be992d3ac0@skyskimmer.net> 0 siblings, 2 replies; 54+ messages in thread From: Thorsten Altenkirch @ 2017-12-12 11:03 UTC (permalink / raw) To: Andrea Vezzosi; +Cc: Kristina Sojakova, Homotopy Type Theory 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" <sanz...@gmail.com> wrote: >On Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenkirch ><Thorsten....@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 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" <homotopyt...@googlegroups.com on behalf of 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 >> >> -- >> 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-12 11:03 ` Thorsten Altenkirch @ 2017-12-12 12:02 ` Thomas Streicher 2017-12-12 12:21 ` Thorsten Altenkirch [not found] ` <fa8c0c3c-4870-4c06-fd4d-70be992d3ac0@skyskimmer.net> 1 sibling, 1 reply; 54+ messages in thread From: Thomas Streicher @ 2017-12-12 12:02 UTC (permalink / raw) To: Thorsten Altenkirch Cc: Andrea Vezzosi, Kristina Sojakova, Homotopy Type Theory 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" <sanz...@gmail.com> wrote: > > >On Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenkirch > ><Thorsten....@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 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" <homotopyt...@googlegroups.com on behalf of 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. > ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-12 12:02 ` Thomas Streicher @ 2017-12-12 12:21 ` Thorsten Altenkirch 2017-12-12 13:17 ` Jon Sterling ` (2 more replies) 0 siblings, 3 replies; 54+ messages in thread From: Thorsten Altenkirch @ 2017-12-12 12:21 UTC (permalink / raw) To: Thomas Streicher; +Cc: Andrea Vezzosi, Kristina Sojakova, Homotopy Type Theory 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" <stre...@mathematik.tu-darmstadt.de> 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" <sanz...@gmail.com> wrote: >> >> >On Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenkirch >> ><Thorsten....@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 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" <homotopyt...@googlegroups.com on behalf of 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-12 12:21 ` Thorsten Altenkirch @ 2017-12-12 13:17 ` Jon Sterling 2017-12-12 19:29 ` Thomas Streicher 2017-12-12 23:14 ` Michael Shulman 2017-12-15 17:00 ` Thomas Streicher 2 siblings, 1 reply; 54+ messages in thread From: Jon Sterling @ 2017-12-12 13:17 UTC (permalink / raw) To: HomotopyTypeTheory On Tue, Dec 12, 2017, at 04: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). Thorsten, I think that unique choice holds in every topos, at least when you state it in the topos logic. This is in Mac Lane & Moerdijk as exercise 11 in chapter VI, Topoi And Logic. I'm a little confused now, but maybe this has to do with some subtle difference between the ordinary topos-theoretic subobject classifier, and the HoTT-style one which you get from univalence (as you describe). Best, Jon > 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" > <stre...@mathematik.tu-darmstadt.de> 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" <sanz...@gmail.com> wrote: > >> > >> >On Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenkirch > >> ><Thorsten....@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 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" <homotopyt...@googlegroups.com on behalf of 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-12 13:17 ` Jon Sterling @ 2017-12-12 19:29 ` Thomas Streicher 2017-12-12 19:52 ` Martin Escardo 0 siblings, 1 reply; 54+ messages in thread From: Thomas Streicher @ 2017-12-12 19:29 UTC (permalink / raw) To: Jon Sterling; +Cc: HomotopyT... > I think that unique choice holds in every topos, at least when you state > it in the topos logic. This is in Mac Lane & Moerdijk as exercise 11 in > chapter VI, Topoi And Logic. > > I'm a little confused now, but maybe this has to do with some subtle > difference between the ordinary topos-theoretic subobject classifier, > and the HoTT-style one which you get from univalence (as you describe). Of course, toposes all validate AUC. Since in an arbitrary topos logic is interpreted via the topos's Omega AUC holds then as well. Univalence is something which will not hold in most toposes and if it does one has to interpret Id in a way that it is not a proposition. Thomas ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-12 19:29 ` Thomas Streicher @ 2017-12-12 19:52 ` Martin Escardo 0 siblings, 0 replies; 54+ messages in thread From: Martin Escardo @ 2017-12-12 19:52 UTC (permalink / raw) To: Thomas Streicher, Jon Sterling; +Cc: HomotopyT... On 12/12/17 19:29, Thomas Streicher wrote: > Univalence is something which will not hold in most toposes and if it > does one has to interpret Id in a way that it is not a proposition. How do you even formulate univalence for an arbitrary topos? Martin ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-12 12:21 ` Thorsten Altenkirch 2017-12-12 13:17 ` Jon Sterling @ 2017-12-12 23:14 ` Michael Shulman 2017-12-14 12:32 ` Thorsten Altenkirch 2017-12-15 17:00 ` Thomas Streicher 2 siblings, 1 reply; 54+ messages in thread From: Michael Shulman @ 2017-12-12 23:14 UTC (permalink / raw) To: Thorsten Altenkirch; +Cc: Homotopy Type Theory 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 <Thorsten....@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’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" <stre...@mathematik.tu-darmstadt.de> 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" <sanz...@gmail.com> wrote: >>> >>> >On Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenkirch >>> ><Thorsten....@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 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" <homotopyt...@googlegroups.com on behalf of 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-12 23:14 ` Michael Shulman @ 2017-12-14 12:32 ` Thorsten Altenkirch 2017-12-14 18:52 ` Michael Shulman 0 siblings, 1 reply; 54+ messages in thread From: Thorsten Altenkirch @ 2017-12-14 12:32 UTC (permalink / raw) To: Michael Shulman; +Cc: Homotopy Type Theory Excellent observation! So basically the implementation of Lean is incorrect because we shouldn’t be able to derive true = 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 = Sigma P:Type.Pi x,y.P.x=y. 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. 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. 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" <homotopyt...@googlegroups.com on behalf of 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 <Thorsten....@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’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" <stre...@mathematik.tu-darmstadt.de> 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" <sanz...@gmail.com> wrote: >>> >>> >On Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenkirch >>> ><Thorsten....@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 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" <homotopyt...@googlegroups.com on behalf of 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-14 12:32 ` Thorsten Altenkirch @ 2017-12-14 18:52 ` Michael Shulman 2017-12-16 15:21 ` Thorsten Altenkirch 0 siblings, 1 reply; 54+ messages in thread From: Michael Shulman @ 2017-12-14 18:52 UTC (permalink / raw) To: Thorsten Altenkirch; +Cc: Homotopy Type Theory On Thu, Dec 14, 2017 at 4:32 AM, Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> wrote: > Excellent observation! So basically the implementation of Lean is incorrect because we shouldn’t be able to derive true = 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 = Sigma P:Type.Pi x,y.P.x=y. 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. 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? > 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, 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" <homotopyt...@googlegroups.com on behalf of 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 > <Thorsten....@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’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" <stre...@mathematik.tu-darmstadt.de> 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" <sanz...@gmail.com> wrote: > >>> > >>> >On Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenkirch > >>> ><Thorsten....@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 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" <homotopyt...@googlegroups.com on behalf of 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-14 18:52 ` Michael Shulman @ 2017-12-16 15:21 ` Thorsten Altenkirch 2017-12-17 12:55 ` Michael Shulman 0 siblings, 1 reply; 54+ messages in thread From: Thorsten Altenkirch @ 2017-12-16 15:21 UTC (permalink / raw) To: Michael Shulman; +Cc: Homotopy Type Theory On 14/12/2017, 18:52, "Michael Shulman" <shu...@sandiego.edu> wrote: On Thu, Dec 14, 2017 at 4:32 AM, Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> wrote: > Excellent observation! So basically the implementation of Lean is incorrect because we shouldn¹t be able to derive true = 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 = Sigma P:Type.Pi x,y.P.x=y. 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. 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 ³PropExt -> False² in the current system and you shouldn¹t be able to do this. 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" <homotopyt...@googlegroups.com on behalf of 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 > <Thorsten....@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¹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" <stre...@mathematik.tu-darmstadt.de> 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" <sanz...@gmail.com> wrote: > >>> > >>> >On Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenkirch > >>> ><Thorsten....@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 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" <homotopyt...@googlegroups.com on behalf of 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-16 15:21 ` Thorsten Altenkirch @ 2017-12-17 12:55 ` Michael Shulman 2017-12-17 17:08 ` Ben Sherman 0 siblings, 1 reply; 54+ messages in thread From: Michael Shulman @ 2017-12-17 12:55 UTC (permalink / raw) To: Thorsten Altenkirch; +Cc: Homotopy Type Theory On Sat, Dec 16, 2017 at 7:21 AM, Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> 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" <homotopyt...@googlegroups.com on behalf of > 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 > > <Thorsten....@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¹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" > <stre...@mathematik.tu-darmstadt.de> 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" <sanz...@gmail.com> > wrote: > > >>> > > >>> >On Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenkirch > > >>> ><Thorsten....@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 > 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" > <homotopyt...@googlegroups.com on behalf of > 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-17 12:55 ` Michael Shulman @ 2017-12-17 17:08 ` Ben Sherman 2017-12-17 17:16 ` Thorsten Altenkirch 0 siblings, 1 reply; 54+ messages in thread From: Ben Sherman @ 2017-12-17 17:08 UTC (permalink / raw) To: Michael Shulman; +Cc: Thorsten Altenkirch, Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 17886 bytes --] 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 <shu...@sandiego.edu> wrote: > > On Sat, Dec 16, 2017 at 7:21 AM, Thorsten Altenkirch > <Thorsten....@nottingham.ac.uk <mailto:Thorsten....@nottingham.ac.uk>> 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" <homotopyt...@googlegroups.com on behalf of >> 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 >>> <Thorsten....@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¹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" >> <stre...@mathematik.tu-darmstadt.de> 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" <sanz...@gmail.com> >> wrote: >>>>>> >>>>>>> On Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenkirch >>>>>>> <Thorsten....@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 >> 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" >> <homotopyt...@googlegroups.com on behalf of >> 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 <mailto:HomotopyTypeThe...@googlegroups.com>. > For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>. [-- Attachment #2: Type: text/html, Size: 46969 bytes --] ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-17 17:08 ` Ben Sherman @ 2017-12-17 17:16 ` Thorsten Altenkirch 2017-12-17 22:43 ` Floris van Doorn 0 siblings, 1 reply; 54+ messages in thread From: Thorsten Altenkirch @ 2017-12-17 17:16 UTC (permalink / raw) To: Ben Sherman, Michael Shulman; +Cc: Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 17688 bytes --] Thank you, Ben! That is good news actually. Thorsten From: Ben Sherman <she...@csail.mit.edu<mailto:she...@csail.mit.edu>> Date: Sunday, 17 December 2017 at 18:08 To: Michael Shulman <shu...@sandiego.edu<mailto:shu...@sandiego.edu>> Cc: Thorsten Altenkirch <psz...@exmail.nottingham.ac.uk<mailto:psz...@exmail.nottingham.ac.uk>>, Homotopy Type Theory <homotopyt...@googlegroups.com<mailto:homotopyt...@googlegroups.com>> Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 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 <shu...@sandiego.edu<mailto:shu...@sandiego.edu>> wrote: On Sat, Dec 16, 2017 at 7:21 AM, Thorsten Altenkirch <Thorsten....@nottingham.ac.uk<mailto:Thorsten....@nottingham.ac.uk>> 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<mailto:homotopyt...@googlegroups.com> on behalf of Michael Shulman" <homotopyt...@googlegroups.com<mailto:homotopyt...@googlegroups.com> on behalf of shu...@sandiego.edu<mailto: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 <Thorsten....@nottingham.ac.uk<mailto:Thorsten....@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¹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" <stre...@mathematik.tu-darmstadt.de<mailto:stre...@mathematik.tu-darmstadt.de>> 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" <sanz...@gmail.com<mailto:sanz...@gmail.com>> wrote: On Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenkirch <Thorsten....@nottingham.ac.uk<mailto:Thorsten....@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 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<mailto:homotopyt...@googlegroups.com> on behalf of Kristina Sojakova" <homotopyt...@googlegroups.com<mailto:homotopyt...@googlegroups.com> on behalf of sojakova...@gmail.com<mailto: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<mailto: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<mailto: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<mailto: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<mailto: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<mailto: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. [-- Attachment #2: Type: text/html, Size: 51361 bytes --] ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-17 17:16 ` Thorsten Altenkirch @ 2017-12-17 22:43 ` Floris van Doorn 0 siblings, 0 replies; 54+ messages in thread From: Floris van Doorn @ 2017-12-17 22:43 UTC (permalink / raw) To: Thorsten Altenkirch Cc: Ben Sherman, Michael Shulman, Homotopy Type Theory, Jeremy Avigad, Rob Lewis [-- Attachment #1: Type: text/plain, Size: 20456 bytes --] 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 = A for some type A, then transporting along p is the identity function (because p = refl, definitionally). However, if p : A = 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 <she...@csail.mit.edu> > Date: Sunday, 17 December 2017 at 18:08 > To: Michael Shulman <shu...@sandiego.edu> > Cc: Thorsten Altenkirch <psz...@exmail.nottingham.ac.uk>, Homotopy Type > Theory <homotopyt...@googlegroups.com> > Subject: Re: [HoTT] Impredicative set + function extensionality + proof > irrelevance consistent? > > 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 <shu...@sandiego.edu> wrote: > > On Sat, Dec 16, 2017 at 7:21 AM, Thorsten Altenkirch > <Thorsten....@nottingham.ac.uk> 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" <homotopyt...@googlegroups.com on behalf of > 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 > <Thorsten....@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¹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" > > <stre...@mathematik.tu-darmstadt.de> 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" <sanz...@gmail.com> > > wrote: > > > On Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenkirch > <Thorsten....@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 > 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" > <homotopyt...@googlegroups.com on behalf of > 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. > [-- Attachment #2: Type: text/html, Size: 44320 bytes --] ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-12 12:21 ` Thorsten Altenkirch 2017-12-12 13:17 ` Jon Sterling 2017-12-12 23:14 ` Michael Shulman @ 2017-12-15 17:00 ` Thomas Streicher 2017-12-17 8:47 ` Thorsten Altenkirch 2 siblings, 1 reply; 54+ messages in thread From: Thomas Streicher @ 2017-12-15 17:00 UTC (permalink / raw) To: Thorsten Altenkirch Cc: Andrea Vezzosi, Kristina Sojakova, Homotopy Type Theory Hi Thorsten, my analysis of your proof of true = false in Lean is as follows. I don't see that (\Sigma x:A) a = x is an element of Prop though it certainly is isomorphic to an element in Prop, namely true. But leaving this aside I analyse the situation as follows. Your argument essentially is as follows. Since Single(true) and Single(false) are isomorphic they are equal (essentially by UA applied to subsingletons). Now you have c in Single(true) and d in Single(false) whose first projections are true and false respectively. From this you conclude that that true and false are equal since c and d are equal. But they aren't since they belong to different types. This style of argument allows you prove that all types are propositions as follows. Suppose a and a' are elements of A. Then Single(a) and Single(a') are equivalent propositions and thus equal. Then also their first projections are equal and thus a = a'. I fully agree with Mike's analysis that projections have to be typed. But, moreover, we must not neglect equality proofs when replacing equals by equals. Moreover, toposes will not validate univalence. As pointed out to me by Martin Escardo you can't even formulate it because in arbitrary toposes you don't have universe (not to speak of univalent ones). Thomas PS Your observation doesn't really increase my believe in the gain of certainty when formalizing proofs :-) ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-15 17:00 ` Thomas Streicher @ 2017-12-17 8:47 ` Thorsten Altenkirch 2017-12-17 10:21 ` Thomas Streicher 0 siblings, 1 reply; 54+ messages in thread From: Thorsten Altenkirch @ 2017-12-17 8:47 UTC (permalink / raw) To: Thomas Streicher; +Cc: Andrea Vezzosi, Kristina Sojakova, Homotopy Type Theory On 15/12/2017, 17:00, "homotopyt...@googlegroups.com on behalf of Thomas Streicher" <homotopyt...@googlegroups.com on behalf of stre...@mathematik.tu-darmstadt.de> wrote: >Moreover, toposes will not validate univalence. As pointed out to me >by Martin Escardo you can't even formulate it because in arbitrary >toposes you don't have universe (not to speak of univalent ones). I was only talking about the special case of (-1)-univalence or propositional extensionality that is for P,Q : Prop (P <-> Q) -> (P = Q) Thorsten > 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-17 8:47 ` Thorsten Altenkirch @ 2017-12-17 10:21 ` Thomas Streicher 2017-12-17 11:39 ` Thorsten Altenkirch 0 siblings, 1 reply; 54+ messages in thread From: Thomas Streicher @ 2017-12-17 10:21 UTC (permalink / raw) To: Thorsten Altenkirch Cc: Andrea Vezzosi, Kristina Sojakova, Homotopy Type Theory > >Moreover, toposes will not validate univalence. As pointed out to me > >by Martin Escardo you can't even formulate it because in arbitrary > >toposes you don't have universe (not to speak of univalent ones). > > I was only talking about the special case of (-1)-univalence or > propositional extensionality that is for P,Q : Prop > > (P <-> Q) -> (P = Q) This would be ok but you assume also that Single(True) and Single(false) are propositions but they are just both ISOMORPHIC to 1 in Omega = Prop. That's where you apply UA for (sub)singletons UNCONSCIOUSLY. The inconsistency proof you have given is a slightly distorted version of the following ridiculous argument: {a} and {b} are isomorphic thus equal for which reason a = b. Thomas ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-17 10:21 ` Thomas Streicher @ 2017-12-17 11:39 ` Thorsten Altenkirch 2017-12-18 7:41 ` Matt Oliveri 2017-12-18 11:52 ` Thomas Streicher 0 siblings, 2 replies; 54+ messages in thread From: Thorsten Altenkirch @ 2017-12-17 11:39 UTC (permalink / raw) To: Thomas Streicher; +Cc: Andrea Vezzosi, Kristina Sojakova, Homotopy Type Theory On 17/12/2017, 10:21, "Thomas Streicher" <stre...@mathematik.tu-darmstadt.de> wrote: >> >Moreover, toposes will not validate univalence. As pointed out to me >> >by Martin Escardo you can't even formulate it because in arbitrary >> >toposes you don't have universe (not to speak of univalent ones). >> >> I was only talking about the special case of (-1)-univalence or >> propositional extensionality that is for P,Q : Prop >> >> (P <-> Q) -> (P = Q) > >This would be ok but you assume also that Single(True) and >Single(false) are propositions but they are just both ISOMORPHIC to 1 >in Omega = Prop. That's where you apply UA for (sub)singletons >UNCONSCIOUSLY. I wasn't defending the inconsistency derivation I posted earlier, as Mike pointed out it, it ignores type annotations. However, I don't understand your point. Surely UA for subsingletons is exactly propositional extensionality. >The inconsistency proof you have given is a slightly distorted version >of the following ridiculous argument: {a} and {b} are isomorphic thus >equal for which reason a = b. Indeed, but we are not in set theory. In set level HoTT Single(True) = Single(False) but True != False. Whenever we can prove that a type is A propositional, that is all x,y:A.x=y it is a subsingleton and we can construct a corresponding element of Prop (aka Omega). Hence a topos corresponds to set-level HoTT (ignoring predicativity issues for the moment). In a language like Lean with a static universe of propositions this is not the case. Only certain subsingletons get classified. I don't really understand the relation but it seems that you get a quasitopos. And indeed in this language you don't have unique choice (which was the cause of my confusion). The issue was this: in a type theory with a static universe of propositions you can add definitional proof-irrelevance, that is any two proofs of a proposition are definitionally equal. The derivation I posted earlier seemed to imply that you cannot have definitional proof-irrelevance and a be in a topos. Luckily this turns out to be incorrect and it is just due to the way proof irrelevance is implemented in Lean (which is just wrong imho). 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-17 11:39 ` Thorsten Altenkirch @ 2017-12-18 7:41 ` Matt Oliveri 2017-12-18 10:00 ` Michael Shulman 2017-12-18 10:10 ` Thorsten Altenkirch 2017-12-18 11:52 ` Thomas Streicher 1 sibling, 2 replies; 54+ messages in thread From: Matt Oliveri @ 2017-12-18 7:41 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 1781 bytes --] Hello. I'd like to see if I have the situation straight: For presenting a topos as a type system, there are expected to be (at least) two styles: having a type of "static" propositions, or using hprops. With hprops, you can prove unique choice, so it's always topos-like (pretopos?). With static props, you can't prove unique choice, but it may be consistent as an additional primitive, or you can ensure in some other way that you have a subobject classifier. If you don't necessarily have unique choice or equivalent, you're dealing with a quasitopos, which is a more general thing. With static props and unique choice, subsingletons generally aren't already propositions, but they all correspond to a proposition stating that the subsingleton is inhabited. Unique choice obtains the element of a subsingleton known to be inhabited. The usual way to present a topos as a type system is with a non-dependent type system like IHOL. This will not be able to express hprops, so static props is the way. Proofs will not be objects, so proof-irrelevance doesn't come up. The static props approach can also be used in a dependent type system, along with unique choice or equivalent. (To say nothing of whether that's a natural kind of system.) In a dependent type system, a type of static props may or may not be a universe. If it's not, proofs still aren't objects and proof-irrelevance still doesn't come up. But if it is, you should at least have typal proof-irrelevance. (That is, stated using equality types.) In that case, with equality reflection, you automatically get judgmental proof-irrelevance. This does not necessarily mean that proofs are computationally irrelevant. With unique choice, they cannot be, or else you lose canonicity. All OK? [-- Attachment #1.2: Type: text/html, Size: 1908 bytes --] ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-18 7:41 ` Matt Oliveri @ 2017-12-18 10:00 ` Michael Shulman 2017-12-18 11:55 ` Matt Oliveri 2017-12-18 10:10 ` Thorsten Altenkirch 1 sibling, 1 reply; 54+ messages in thread From: Michael Shulman @ 2017-12-18 10:00 UTC (permalink / raw) To: Matt Oliveri; +Cc: Homotopy Type Theory That seems about right to me, except that I don't know whether a static universe of props without unique choice *actually* gives a quasitopos. It gives you a class of subobjects that have a classifer, which looks kind of like a quasitopos, but can we prove that they are actually the strong/regular monos as in a quasitopos? And a quasitopos also has finite colimits; do HITs make sense with a static Prop? On Sun, Dec 17, 2017 at 11:41 PM, Matt Oliveri <atm...@gmail.com> wrote: > Hello. I'd like to see if I have the situation straight: > > For presenting a topos as a type system, there are expected to be (at least) > two styles: having a type of "static" propositions, or using hprops. > > With hprops, you can prove unique choice, so it's always topos-like > (pretopos?). > > With static props, you can't prove unique choice, but it may be consistent > as an additional primitive, or you can ensure in some other way that you > have a subobject classifier. > > If you don't necessarily have unique choice or equivalent, you're dealing > with a quasitopos, which is a more general thing. > > With static props and unique choice, subsingletons generally aren't already > propositions, but they all correspond to a proposition stating that the > subsingleton is inhabited. Unique choice obtains the element of a > subsingleton known to be inhabited. > > The usual way to present a topos as a type system is with a non-dependent > type system like IHOL. This will not be able to express hprops, so static > props is the way. Proofs will not be objects, so proof-irrelevance doesn't > come up. > > The static props approach can also be used in a dependent type system, along > with unique choice or equivalent. (To say nothing of whether that's a > natural kind of system.) > > In a dependent type system, a type of static props may or may not be a > universe. > > If it's not, proofs still aren't objects and proof-irrelevance still doesn't > come up. > > But if it is, you should at least have typal proof-irrelevance. (That is, > stated using equality types.) > > In that case, with equality reflection, you automatically get judgmental > proof-irrelevance. This does not necessarily mean that proofs are > computationally irrelevant. With unique choice, they cannot be, or else you > lose canonicity. > > All OK? > > -- > 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-18 10:00 ` Michael Shulman @ 2017-12-18 11:55 ` Matt Oliveri 2017-12-18 16:24 ` Michael Shulman 0 siblings, 1 reply; 54+ messages in thread From: Matt Oliveri @ 2017-12-18 11:55 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 2803 bytes --] Oh right. Static propositions alone doesn't seem to guarantee a quasitopos either. I thought HITs make sense with static props. After all, the type of propositions isn't even involved, formally. On Monday, December 18, 2017 at 5:00:51 AM UTC-5, Michael Shulman wrote: > > That seems about right to me, except that I don't know whether a > static universe of props without unique choice *actually* gives a > quasitopos. It gives you a class of subobjects that have a classifer, > which looks kind of like a quasitopos, but can we prove that they are > actually the strong/regular monos as in a quasitopos? And a > quasitopos also has finite colimits; do HITs make sense with a static > Prop? > > On Sun, Dec 17, 2017 at 11:41 PM, Matt Oliveri <atm...@gmail.com > <javascript:>> wrote: > > Hello. I'd like to see if I have the situation straight: > > > > For presenting a topos as a type system, there are expected to be (at > least) > > two styles: having a type of "static" propositions, or using hprops. > > > > With hprops, you can prove unique choice, so it's always topos-like > > (pretopos?). > > > > With static props, you can't prove unique choice, but it may be > consistent > > as an additional primitive, or you can ensure in some other way that you > > have a subobject classifier. > > > > If you don't necessarily have unique choice or equivalent, you're > dealing > > with a quasitopos, which is a more general thing. > > > > With static props and unique choice, subsingletons generally aren't > already > > propositions, but they all correspond to a proposition stating that the > > subsingleton is inhabited. Unique choice obtains the element of a > > subsingleton known to be inhabited. > > > > The usual way to present a topos as a type system is with a > non-dependent > > type system like IHOL. This will not be able to express hprops, so > static > > props is the way. Proofs will not be objects, so proof-irrelevance > doesn't > > come up. > > > > The static props approach can also be used in a dependent type system, > along > > with unique choice or equivalent. (To say nothing of whether that's a > > natural kind of system.) > > > > In a dependent type system, a type of static props may or may not be a > > universe. > > > > If it's not, proofs still aren't objects and proof-irrelevance still > doesn't > > come up. > > > > But if it is, you should at least have typal proof-irrelevance. (That > is, > > stated using equality types.) > > > > In that case, with equality reflection, you automatically get judgmental > > proof-irrelevance. This does not necessarily mean that proofs are > > computationally irrelevant. With unique choice, they cannot be, or else > you > > lose canonicity. > > > > All OK? > [-- Attachment #1.2: Type: text/html, Size: 3429 bytes --] ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-18 11:55 ` Matt Oliveri @ 2017-12-18 16:24 ` Michael Shulman 2017-12-18 20:08 ` Matt Oliveri 0 siblings, 1 reply; 54+ messages in thread From: Michael Shulman @ 2017-12-18 16:24 UTC (permalink / raw) To: Matt Oliveri; +Cc: Homotopy Type Theory HITs involve equality, so if equality is a static prop, then it is involved. On Mon, Dec 18, 2017 at 3:55 AM, Matt Oliveri <atm...@gmail.com> wrote: > Oh right. Static propositions alone doesn't seem to guarantee a quasitopos > either. > > I thought HITs make sense with static props. After all, the type of > propositions isn't even involved, formally. > > On Monday, December 18, 2017 at 5:00:51 AM UTC-5, Michael Shulman wrote: >> >> That seems about right to me, except that I don't know whether a >> static universe of props without unique choice *actually* gives a >> quasitopos. It gives you a class of subobjects that have a classifer, >> which looks kind of like a quasitopos, but can we prove that they are >> actually the strong/regular monos as in a quasitopos? And a >> quasitopos also has finite colimits; do HITs make sense with a static >> Prop? >> >> On Sun, Dec 17, 2017 at 11:41 PM, Matt Oliveri <atm...@gmail.com> wrote: >> > Hello. I'd like to see if I have the situation straight: >> > >> > For presenting a topos as a type system, there are expected to be (at >> > least) >> > two styles: having a type of "static" propositions, or using hprops. >> > >> > With hprops, you can prove unique choice, so it's always topos-like >> > (pretopos?). >> > >> > With static props, you can't prove unique choice, but it may be >> > consistent >> > as an additional primitive, or you can ensure in some other way that you >> > have a subobject classifier. >> > >> > If you don't necessarily have unique choice or equivalent, you're >> > dealing >> > with a quasitopos, which is a more general thing. >> > >> > With static props and unique choice, subsingletons generally aren't >> > already >> > propositions, but they all correspond to a proposition stating that the >> > subsingleton is inhabited. Unique choice obtains the element of a >> > subsingleton known to be inhabited. >> > >> > The usual way to present a topos as a type system is with a >> > non-dependent >> > type system like IHOL. This will not be able to express hprops, so >> > static >> > props is the way. Proofs will not be objects, so proof-irrelevance >> > doesn't >> > come up. >> > >> > The static props approach can also be used in a dependent type system, >> > along >> > with unique choice or equivalent. (To say nothing of whether that's a >> > natural kind of system.) >> > >> > In a dependent type system, a type of static props may or may not be a >> > universe. >> > >> > If it's not, proofs still aren't objects and proof-irrelevance still >> > doesn't >> > come up. >> > >> > But if it is, you should at least have typal proof-irrelevance. (That >> > is, >> > stated using equality types.) >> > >> > In that case, with equality reflection, you automatically get judgmental >> > proof-irrelevance. This does not necessarily mean that proofs are >> > computationally irrelevant. With unique choice, they cannot be, or else >> > you >> > lose canonicity. >> > >> > All OK? > > -- > 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-18 16:24 ` Michael Shulman @ 2017-12-18 20:08 ` Matt Oliveri 0 siblings, 0 replies; 54+ messages in thread From: Matt Oliveri @ 2017-12-18 20:08 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 3636 bytes --] Well that's true. For some reason, I was thinking equality would still be an ordinary type, but I guess that would be silly. So what do you require, for HITs to "make sense", with equality being a static prop family? That they can provide finite colimits? Don't they do this, analogously to homotopy colimits in HoTT? On Monday, December 18, 2017 at 11:25:22 AM UTC-5, Michael Shulman wrote: > > HITs involve equality, so if equality is a static prop, then it is > involved. > > On Mon, Dec 18, 2017 at 3:55 AM, Matt Oliveri <atm...@gmail.com > <javascript:>> wrote: > > Oh right. Static propositions alone doesn't seem to guarantee a > quasitopos > > either. > > > > I thought HITs make sense with static props. After all, the type of > > propositions isn't even involved, formally. > > > > On Monday, December 18, 2017 at 5:00:51 AM UTC-5, Michael Shulman wrote: > >> > >> That seems about right to me, except that I don't know whether a > >> static universe of props without unique choice *actually* gives a > >> quasitopos. It gives you a class of subobjects that have a classifer, > >> which looks kind of like a quasitopos, but can we prove that they are > >> actually the strong/regular monos as in a quasitopos? And a > >> quasitopos also has finite colimits; do HITs make sense with a static > >> Prop? > >> > >> On Sun, Dec 17, 2017 at 11:41 PM, Matt Oliveri <atm...@gmail.com> > wrote: > >> > Hello. I'd like to see if I have the situation straight: > >> > > >> > For presenting a topos as a type system, there are expected to be (at > >> > least) > >> > two styles: having a type of "static" propositions, or using hprops. > >> > > >> > With hprops, you can prove unique choice, so it's always topos-like > >> > (pretopos?). > >> > > >> > With static props, you can't prove unique choice, but it may be > >> > consistent > >> > as an additional primitive, or you can ensure in some other way that > you > >> > have a subobject classifier. > >> > > >> > If you don't necessarily have unique choice or equivalent, you're > >> > dealing > >> > with a quasitopos, which is a more general thing. > >> > > >> > With static props and unique choice, subsingletons generally aren't > >> > already > >> > propositions, but they all correspond to a proposition stating that > the > >> > subsingleton is inhabited. Unique choice obtains the element of a > >> > subsingleton known to be inhabited. > >> > > >> > The usual way to present a topos as a type system is with a > >> > non-dependent > >> > type system like IHOL. This will not be able to express hprops, so > >> > static > >> > props is the way. Proofs will not be objects, so proof-irrelevance > >> > doesn't > >> > come up. > >> > > >> > The static props approach can also be used in a dependent type > system, > >> > along > >> > with unique choice or equivalent. (To say nothing of whether that's a > >> > natural kind of system.) > >> > > >> > In a dependent type system, a type of static props may or may not be > a > >> > universe. > >> > > >> > If it's not, proofs still aren't objects and proof-irrelevance still > >> > doesn't > >> > come up. > >> > > >> > But if it is, you should at least have typal proof-irrelevance. (That > >> > is, > >> > stated using equality types.) > >> > > >> > In that case, with equality reflection, you automatically get > judgmental > >> > proof-irrelevance. This does not necessarily mean that proofs are > >> > computationally irrelevant. With unique choice, they cannot be, or > else > >> > you > >> > lose canonicity. > >> > > >> > All OK? > [-- Attachment #1.2: Type: text/html, Size: 4786 bytes --] ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-18 7:41 ` Matt Oliveri 2017-12-18 10:00 ` Michael Shulman @ 2017-12-18 10:10 ` Thorsten Altenkirch 2017-12-18 11:17 ` Matt Oliveri 2017-12-18 12:09 ` Matt Oliveri 1 sibling, 2 replies; 54+ messages in thread From: Thorsten Altenkirch @ 2017-12-18 10:10 UTC (permalink / raw) To: Matt Oliveri, Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 4514 bytes --] I agree with most of your summary. Some comments and questions. From: <homotopyt...@googlegroups.com> on behalf of Matt Oliveri <atm...@gmail.com> Date: Monday, 18 December 2017 at 07:41 To: Homotopy Type Theory <homotopyt...@googlegroups.com> Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? Hello. I'd like to see if I have the situation straight: For presenting a topos as a type system, there are expected to be (at least) two styles: having a type of "static" propositions, or using hprops. With hprops, you can prove unique choice, so it's always topos-like (pretopos?). Yes, indeed. The remaining issue is the question of impredicativity. If you want to stay predicative you may want to add quotients or QITs. Interestingly it seems that QITs are more expressive then quotients (which can be encoded impredicatively). With static props, you can't prove unique choice, but it may be consistent as an additional primitive, or you can ensure in some other way that you have a subobject classifier. Yes, indeed. However, adding postulates to Type Theory is just a stop gap measure because you still don’t have a computational interpretation. While we have a computational interpretation for most of HoTT, namely cubical type theory ala Coquand et al, one might hope that there is a simpler way to deal with the set level fragment of HoTT. If you don't necessarily have unique choice or equivalent, you're dealing with a quasitopos, which is a more general thing. Basically you reflect some subobjects but not all. I don’t yet understand how the definition of a quasitops relates to static universes of propositios. With static props and unique choice, subsingletons generally aren't already propositions, but they all correspond to a proposition stating that the subsingleton is inhabited. Unique choice obtains the element of a subsingleton known to be inhabited. The usual way to present a topos as a type system is with a non-dependent type system like IHOL. This will not be able to express hprops, so static props is the way. Proofs will not be objects, so proof-irrelevance doesn't come up. Indeed or to put it the other way: set level HoTT is a novel way to present a topos. And as I said above, QITs are an interesting extension which in some instances avoids appealing to the axiom of choice. The static props approach can also be used in a dependent type system, along with unique choice or equivalent. (To say nothing of whether that's a natural kind of system.) In a dependent type system, a type of static props may or may not be a universe. What do you mean by “is a universe” here? If it's not, proofs still aren't objects and proof-irrelevance still doesn't come up. But if it is, you should at least have typal proof-irrelevance. (That is, stated using equality types.) In that case, with equality reflection, you automatically get judgmental proof-irrelevance. For equality but not for propositions in general. This does not necessarily mean that proofs are computationally irrelevant. Now I am confused: what is the difference between judgmental and computational irrelevance? With unique choice, they cannot be, or else you lose canonicity. Since I didn’t understand the previous sentences I am not sure about this conclusion. It sounds right, though. Thorsten All OK? -- 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<mailto: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. [-- Attachment #2: Type: text/html, Size: 8648 bytes --] ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-18 10:10 ` Thorsten Altenkirch @ 2017-12-18 11:17 ` Matt Oliveri 2017-12-18 12:09 ` Matt Oliveri 1 sibling, 0 replies; 54+ messages in thread From: Matt Oliveri @ 2017-12-18 11:17 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 2762 bytes --] On Monday, December 18, 2017 at 5:10:15 AM UTC-5, Thorsten Altenkirch wrote: > > > With static props, you can't prove unique choice, but it may be consistent > as an additional primitive, or you can ensure in some other way that you > have a subobject classifier. > > > > Yes, indeed. However, adding postulates to Type Theory is just a stop gap > measure because you still don’t have a computational interpretation. While > we have a computational interpretation for most of HoTT, namely cubical > type theory ala Coquand et al, one might hope that there is a simpler way > to deal with the set level fragment of HoTT. > I suspect one could also come up with a type system with a computational interpretation that has static props and unique choice. I was counting this possibility too as an additional primitive. > The static props approach can also be used in a dependent type system, > along with unique choice or equivalent. (To say nothing of whether that's a > natural kind of system.) > > In a dependent type system, a type of static props may or may not be a > universe. > > > > What do you mean by “is a universe” here? > Just that the type of props would be one of the built-in universes, either Russell or Tarski-style. > But if it is, you should at least have typal proof-irrelevance. (That is, > stated using equality types.) > > In that case, with equality reflection, you automatically get judgmental > proof-irrelevance. > > > > For equality but not for propositions in general. > I'm saying if you have typal proof-irrelevance and equality reflection, you get judgmental proof-irrelevance by reflecting the equalities between proofs given by typal proof-irrelevance. > > This does not necessarily mean that proofs are computationally irrelevant. > > > > Now I am confused: what is the difference between judgmental and > computational irrelevance? > By computationally-irrelevant proofs, I mean that terms of propositions are never needed when evaluating closed terms of non-proposition types. Like, Coq has a type of static propositions: the universe Prop. And the proofs are supposed to be computationally irrelevant. This is relied upon to erase them with program extraction. From the earlier messages about Lean, it sounds like Lean's proofs are also intended to be computationally irrelevant. With equality reflection, irrelevance according to judgmental equality can be totally different from computational relevance. (Though it seems like a confusing and unhelpful possibility. When judgments are undecidable anyway, computationally irrelevant proofs can simply be removed from the term language entirely.) [-- Attachment #1.2: Type: text/html, Size: 4117 bytes --] ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-18 10:10 ` Thorsten Altenkirch 2017-12-18 11:17 ` Matt Oliveri @ 2017-12-18 12:09 ` Matt Oliveri 1 sibling, 0 replies; 54+ messages in thread From: Matt Oliveri @ 2017-12-18 12:09 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 589 bytes --] I don't understand these things you wrote: On Monday, December 18, 2017 at 5:10:15 AM UTC-5, Thorsten Altenkirch wrote: > > Interestingly it seems that QITs are more expressive then quotients (which > can be encoded impredicatively). > > > And as I said above, QITs are an interesting extension which in some > instances avoids appealing to the axiom of choice. > Like, in a constructive, predicative system without any choice principles, and where quotients are not expressed as QITs, is there an expressiveness difference? (I'm thinking of Computational Type Theory, for example.) [-- Attachment #1.2: Type: text/html, Size: 875 bytes --] ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-17 11:39 ` Thorsten Altenkirch 2017-12-18 7:41 ` Matt Oliveri @ 2017-12-18 11:52 ` Thomas Streicher 2017-12-19 11:26 ` Thorsten Altenkirch 1 sibling, 1 reply; 54+ messages in thread From: Thomas Streicher @ 2017-12-18 11:52 UTC (permalink / raw) To: Thorsten Altenkirch Cc: Andrea Vezzosi, Kristina Sojakova, Homotopy Type Theory > >The inconsistency proof you have given is a slightly distorted version > >of the following ridiculous argument: {a} and {b} are isomorphic thus > >equal for which reason a = b. > > Indeed, but we are not in set theory. In set level HoTT Single(True) = > Single(False) but True != False. This is not a question of set theory. In a topos we have propositional extensionality in the sense that \forall p,q:Omega. (p <-> q) -> p = q but what we don't have is that Single(a) \in \Omega for a \in A. Thomas ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-18 11:52 ` Thomas Streicher @ 2017-12-19 11:26 ` Thorsten Altenkirch 2017-12-19 13:52 ` Andrej Bauer 0 siblings, 1 reply; 54+ messages in thread From: Thorsten Altenkirch @ 2017-12-19 11:26 UTC (permalink / raw) To: Thomas Streicher; +Cc: Andrea Vezzosi, Kristina Sojakova, Homotopy Type Theory I don’t understand this: HProps are subobjects of 1 hence they get classified as propositions. Hence there is an element of Omega corresponding to Sigle(a). Thorsten On 18/12/2017, 11:52, "homotopyt...@googlegroups.com on behalf of Thomas Streicher" <homotopyt...@googlegroups.com on behalf of stre...@mathematik.tu-darmstadt.de> wrote: > >The inconsistency proof you have given is a slightly distorted version > >of the following ridiculous argument: {a} and {b} are isomorphic thus > >equal for which reason a = b. > > Indeed, but we are not in set theory. In set level HoTT Single(True) = > Single(False) but True != False. This is not a question of set theory. In a topos we have propositional extensionality in the sense that \forall p,q:Omega. (p <-> q) -> p = q but what we don't have is that Single(a) \in \Omega for a \in A. Thomas -- 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-19 11:26 ` Thorsten Altenkirch @ 2017-12-19 13:52 ` Andrej Bauer 2017-12-19 14:44 ` Thorsten Altenkirch 2017-12-19 16:41 ` Steve Awodey 0 siblings, 2 replies; 54+ messages in thread From: Andrej Bauer @ 2017-12-19 13:52 UTC (permalink / raw) To: Homotopy Type Theory > I don’t understand this: HProps are subobjects of 1 hence they get classified as propositions. Hence there is an element of Omega corresponding to Sigle(a). I beleive a lot of the confusion in this discussion would go away if we translated some of what Thomas is saying into a more syntactic setup. We have to be a bit careful about what "corresponds to" means. To say that Ω classifies truth values, or h-propositions, means that: 1. There is a type Ω. 2. There is a type family El(p) indexed by p : Ω. 3. For every p : Ω the type El(p) is an h-prop (there's a term witnessing this). 4. For every h-prop P -- which is a type, not an element of Ω! -- there is p : Ω such that P is equivalent to El(p). (Again we need a term witnessing the equivalence.) Now, it may happen that h-props P and Q are both equivalent to El(r) even though they are not equal. Furthermore, there can be class-many subobjects of 1 in a topos, for instance in sets there are class-many singletons. Of course, a whole lot of them will be isomorphic and very many "correspond to" the element ⊤ : Ω. But at least on this mailing list we're not in the business of sweeping isomorphisms under the rug. With kind regards, Andrej ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-19 13:52 ` Andrej Bauer @ 2017-12-19 14:44 ` Thorsten Altenkirch 2017-12-19 15:31 ` Thomas Streicher 2017-12-19 16:41 ` Steve Awodey 1 sibling, 1 reply; 54+ messages in thread From: Thorsten Altenkirch @ 2017-12-19 14:44 UTC (permalink / raw) To: Andrej Bauer, Homotopy Type Theory Thank you, Andrej. Indeed, while in usual Type Theory a universe (U, El) with a unit type is presented as one : U El one == 1 (where == is definitional equality) semantically we only have α : El one ~ 1 (where ~ is isomorphism). I was just applying the same abuse of language to Ω, that is there is “Single(a)” : Ω El (“Single(a)”) == Single(a) Where I should have said: β : El (“Single(a)”) ~ Single(a) However, if the category in question is univalent then isomorphic objects are equal and the abuse of language is justified. Thorsten On 19/12/2017, 13:52, "homotopyt...@googlegroups.com on behalf of Andrej Bauer" <homotopyt...@googlegroups.com on behalf of andrej...@andrej.com> wrote: > I don’t understand this: HProps are subobjects of 1 hence they get classified as propositions. Hence there is an element of Omega corresponding to Sigle(a). I beleive a lot of the confusion in this discussion would go away if we translated some of what Thomas is saying into a more syntactic setup. We have to be a bit careful about what "corresponds to" means. To say that Ω classifies truth values, or h-propositions, means that: 1. There is a type Ω. 2. There is a type family El(p) indexed by p : Ω. 3. For every p : Ω the type El(p) is an h-prop (there's a term witnessing this). 4. For every h-prop P -- which is a type, not an element of Ω! -- there is p : Ω such that P is equivalent to El(p). (Again we need a term witnessing the equivalence.) Now, it may happen that h-props P and Q are both equivalent to El(r) even though they are not equal. Furthermore, there can be class-many subobjects of 1 in a topos, for instance in sets there are class-many singletons. Of course, a whole lot of them will be isomorphic and very many "correspond to" the element ⊤ : Ω. But at least on this mailing list we're not in the business of sweeping isomorphisms under the rug. With kind regards, Andrej -- 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-19 14:44 ` Thorsten Altenkirch @ 2017-12-19 15:31 ` Thomas Streicher 2017-12-19 16:10 ` Thorsten Altenkirch 0 siblings, 1 reply; 54+ messages in thread From: Thomas Streicher @ 2017-12-19 15:31 UTC (permalink / raw) To: Thorsten Altenkirch; +Cc: Andrej Bauer, Homotopy Type Theory > Furthermore, there can be class-many subobjects of 1 in a topos, for > instance in sets there are class-many singletons. Of course, a whole > lot of them will be isomorphic and very many "correspond to" the > element ??? : ??. But at least on this mailing list we're not in the > business of sweeping isomorphisms under the rug. Thanks, Andrej, for trying to clean up the discussion! Thorsten hads not daid how to inetrpret equality. In an arbitrary topos there is no other choice than interpeting equality by fibrewise diagonals. So we have extensional equality! I am afraid there want exist too many univalent categories. They all would be rigid which is very inconstructive. Thomas ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-19 15:31 ` Thomas Streicher @ 2017-12-19 16:10 ` Thorsten Altenkirch 2017-12-19 16:31 ` Thomas Streicher 0 siblings, 1 reply; 54+ messages in thread From: Thorsten Altenkirch @ 2017-12-19 16:10 UTC (permalink / raw) To: Thomas Streicher; +Cc: Andrej Bauer, Homotopy Type Theory Ah, you suffer from using set theory as a meta language. ( There are lots if univalent categories. In HoTT. Thorsten On 19/12/2017, 15:31, "homotopyt...@googlegroups.com on behalf of Thomas Streicher" <homotopyt...@googlegroups.com on behalf of stre...@mathematik.tu-darmstadt.de> wrote: I am afraid there want exist too many univalent categories. They all would be rigid which is very inconstructive. 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-19 16:10 ` Thorsten Altenkirch @ 2017-12-19 16:31 ` Thomas Streicher 2017-12-19 16:37 ` Thorsten Altenkirch 0 siblings, 1 reply; 54+ messages in thread From: Thomas Streicher @ 2017-12-19 16:31 UTC (permalink / raw) To: Thorsten Altenkirch; +Cc: Andrej Bauer, Homotopy Type Theory > Ah, you suffer from using set theory as a meta language. ( > > There are lots if univalent categories. In HoTT. That clears it up! Thomas PS I am not fixed to set theory. Could as well be a suffiently strong extensional type theory. But, of course, set theory is fine for me as a metalanguage. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-19 16:31 ` Thomas Streicher @ 2017-12-19 16:37 ` Thorsten Altenkirch 2017-12-20 11:00 ` Thomas Streicher 0 siblings, 1 reply; 54+ messages in thread From: Thorsten Altenkirch @ 2017-12-19 16:37 UTC (permalink / raw) To: Thomas Streicher; +Cc: Andrej Bauer, Homotopy Type Theory I think there is a trade off: you can be destructive and use choice but stick to sets or you are constructive and use HoTT. But having no choice and using sets is sad. T. On 19/12/2017, 16:31, "Thomas Streicher" <stre...@mathematik.tu-darmstadt.de> wrote: > Ah, you suffer from using set theory as a meta language. ( > > There are lots if univalent categories. In HoTT. That clears it up! Thomas PS I am not fixed to set theory. Could as well be a suffiently strong extensional type theory. But, of course, set theory is fine for me as a metalanguage. 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-19 16:37 ` Thorsten Altenkirch @ 2017-12-20 11:00 ` Thomas Streicher 2017-12-20 11:16 ` Thorsten Altenkirch 0 siblings, 1 reply; 54+ messages in thread From: Thomas Streicher @ 2017-12-20 11:00 UTC (permalink / raw) To: Thorsten Altenkirch; +Cc: Andrej Bauer, Homotopy Type Theory Now at first sight it looks as if doing toposes in a univalent metatheory makes them inconsistent in the sense that all toposes are trivial. But, luckily, that is not the case. If a and a' are in A then (a,refl(a)) and (a',refl(a')) are in Single(a) and Single(a') respectively. These types are certainly isomorphic but not judgementally equal. You can project (a,refl(a)) on a and (a',refl(a')) to a' by applying DIFFERENT first projection functions pi and pi' respectively. But you cannot apply pi' to (a,refl(a)) before having it transformed into an object of Single(a') along an iso between Single(a) and Single(a'). Thorsten has claimed that this were possible in LEAN but it shouldn't! Here is an excerpt from Thorsten's original mail > 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 > he clearly says that "since Lean computationally ignores (extProp p)*" but that is balatantly wrong since it mixes judgemental and propositional equality. And there we are back to what I originally said. Of course, {a} and {a'} are isomorphic and thus equal as elements of P(A) if we postulate UA for P(A). Thus we shouldn't! Another gap in Thorsten's argument is the following. Though Single(a) and Single(a') are isomorphic in order to conclude that they are propositionally equal they would have to be elements of a univalent universe BUT I don't see where such a universe should come from in the general topos case! Thomas ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-20 11:00 ` Thomas Streicher @ 2017-12-20 11:16 ` Thorsten Altenkirch 2017-12-20 11:41 ` Thomas Streicher 0 siblings, 1 reply; 54+ messages in thread From: Thorsten Altenkirch @ 2017-12-20 11:16 UTC (permalink / raw) To: Thomas Streicher; +Cc: Andrej Bauer, Homotopy Type Theory Hi Thomas, we have already established that my argument was incorrect (for the reasons you state) and I was misinformed about the behaviour of Lean. > >Another gap in Thorsten's argument is the following. Though Single(a) and >Single(a') are isomorphic in order to conclude that they are propositionally >equal they would have to be elements of a univalent universe BUT I don't see >where such a universe should come from in the general topos case! I don’t understand this point. In a type theoretic implementation of a topos Single(a) and Single(a’) would be propositionally equal due to propositional extensionality. The only additional assumption I need to make is that the universe of proposition is strict, e.g. we have that El(A -> B) is definitionally equal to EL(A) -> El(B). This seems to be quite natural from the point of type theory where universes are usually strict and moreover this is true in any univalent category giving rise to a topos. Thorsten 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-20 11:16 ` Thorsten Altenkirch @ 2017-12-20 11:41 ` Thomas Streicher 2017-12-21 0:42 ` Matt Oliveri 0 siblings, 1 reply; 54+ messages in thread From: Thomas Streicher @ 2017-12-20 11:41 UTC (permalink / raw) To: Thorsten Altenkirch; +Cc: Andrej Bauer, Homotopy Type Theory Hi Thorsten, > we have already established that my argument was incorrect (for the > reasons you state) and I was misinformed about the behaviour of > Lean. I know, I just wanted to spot where the problem precisely is. > >Another gap in Thorsten's argument is the following. Though Single(a) and > >Single(a') are isomorphic in order to conclude that they are propositionally > >equal they would have to be elements of a univalent universe BUT I don't see > >where such a universe should come from in the general topos case! > I don???t understand this point. In a type theoretic implementation of a topos Single(a) and Single(a???) would be propositionally equal due to propositional extensionality. The only additional assumption I need to make is that the universe of proposition is strict, e.g. we have that El(A -> B) is definitionally equal to EL(A) -> El(B). This seems to be quite natural from the point of type theory where universes are usually strict and moreover this is true in any univalent category giving rise to a topos. Well, Single(a) and Single(a') were propsitionally equal if they were elements of a univalent universe U but where should this come from if you start from an elementary topos in a univalent metatheory. Thomas ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-20 11:41 ` Thomas Streicher @ 2017-12-21 0:42 ` Matt Oliveri 2017-12-22 11:18 ` Thorsten Altenkirch 0 siblings, 1 reply; 54+ messages in thread From: Matt Oliveri @ 2017-12-21 0:42 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 2021 bytes --] Hi Thorsten and Thomas, It still looks to me like you're talking about different things and having a misunderstanding. By "propositional extensionality", Thorsten seems to mean the special case of univalence that applies to hprops. (Which he's simply calling propositions.) But it sounds like Thomas is counting "propositional extensionality" as a separate principle from univalence, for a type of static props. I think the system Thorsten has in mind presents a (pre)topos as a univalent type system, where hprops are used *instead of* a type of static props. But maybe not, and I'm misunderstanding. On Wednesday, December 20, 2017 at 6:41:14 AM UTC-5, Thomas Streicher wrote: > > Hi Thorsten, > > > we have already established that my argument was incorrect (for the > > reasons you state) and I was misinformed about the behaviour of > > Lean. > > I know, I just wanted to spot where the problem precisely is. > > > >Another gap in Thorsten's argument is the following. Though Single(a) > and > > >Single(a') are isomorphic in order to conclude that they are > propositionally > > >equal they would have to be elements of a univalent universe BUT I > don't see > > >where such a universe should come from in the general topos case! > > > I don???t understand this point. In a type theoretic implementation of a > topos Single(a) and Single(a???) would be propositionally equal due to > propositional extensionality. The only additional assumption I need to make > is that the universe of proposition is strict, e.g. we have that El(A -> B) > is definitionally equal to EL(A) -> El(B). This seems to be quite natural > from the point of type theory where universes are usually strict and > moreover this is true in any univalent category giving rise to a topos. > > Well, Single(a) and Single(a') were propsitionally equal if they were > elements of a univalent universe U but where should this come from if > you start from an elementary topos in a univalent metatheory. > > Thomas > [-- Attachment #1.2: Type: text/html, Size: 2296 bytes --] ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-21 0:42 ` Matt Oliveri @ 2017-12-22 11:18 ` Thorsten Altenkirch 2017-12-22 21:20 ` Martín Hötzel Escardó 0 siblings, 1 reply; 54+ messages in thread From: Thorsten Altenkirch @ 2017-12-22 11:18 UTC (permalink / raw) To: Matt Oliveri, Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 4781 bytes --] Hi Matt, Yes, this is what I wanted to say. To put it in a different way: in Type Theory we can approximate Omega by HProp. And indeed, every subobject of 1 is represented as an element of HProp. There are 2 mismatches: HProp is large but Omega is small (this corresponds to impredicativity or resizing). The other is propositional extensionality which is an instance of univalence. We can view topoi as a first approximation of HoTT. When we replace a subobject classifier by an object classifier, that is classifying all maps and not just propositions we obtain univalent universes. However, two provisos are necessary: 1. we cannot classify all maps otherwise we end up with a system with Type : Type and 2. we have to move to an (omega,1)-category because univalence is forced upon us as an equality and this doesn’t work if all types are sets. That is a higher predicative topos fixes the historic shortcomings of topos theory. By moving to a predicative setting we give up the encodings of colimits (e.g. coequalizers) using the subobject classifier. Indeed, this is just the impredicative encoding of quotient types. Instead we need to explictly add them but we can do this in a way which goes beyond topos theory (even in the propositional setting) namely as QITs (propositional) or HITs (in the higher case). Thorsten From: <homotopyt...@googlegroups.com<mailto:homotopyt...@googlegroups.com>> on behalf of Matt Oliveri <atm...@gmail.com<mailto:atm...@gmail.com>> Date: Thursday, 21 December 2017 at 00:42 To: Homotopy Type Theory <homotopyt...@googlegroups.com<mailto:homotopyt...@googlegroups.com>> Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? Hi Thorsten and Thomas, It still looks to me like you're talking about different things and having a misunderstanding. By "propositional extensionality", Thorsten seems to mean the special case of univalence that applies to hprops. (Which he's simply calling propositions.) But it sounds like Thomas is counting "propositional extensionality" as a separate principle from univalence, for a type of static props. I think the system Thorsten has in mind presents a (pre)topos as a univalent type system, where hprops are used *instead of* a type of static props. But maybe not, and I'm misunderstanding. On Wednesday, December 20, 2017 at 6:41:14 AM UTC-5, Thomas Streicher wrote: Hi Thorsten, > we have already established that my argument was incorrect (for the > reasons you state) and I was misinformed about the behaviour of > Lean. I know, I just wanted to spot where the problem precisely is. > >Another gap in Thorsten's argument is the following. Though Single(a) and > >Single(a') are isomorphic in order to conclude that they are propositionally > >equal they would have to be elements of a univalent universe BUT I don't see > >where such a universe should come from in the general topos case! > I don???t understand this point. In a type theoretic implementation of a topos Single(a) and Single(a???) would be propositionally equal due to propositional extensionality. The only additional assumption I need to make is that the universe of proposition is strict, e.g. we have that El(A -> B) is definitionally equal to EL(A) -> El(B). This seems to be quite natural from the point of type theory where universes are usually strict and moreover this is true in any univalent category giving rise to a topos. Well, Single(a) and Single(a') were propsitionally equal if they were elements of a univalent universe U but where should this come from if you start from an elementary topos in a univalent metatheory. Thomas -- 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<mailto: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. [-- Attachment #2: Type: text/html, Size: 6579 bytes --] ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-22 11:18 ` Thorsten Altenkirch @ 2017-12-22 21:20 ` Martín Hötzel Escardó 2017-12-22 21:36 ` Martín Hötzel Escardó 2017-12-23 0:25 ` Matt Oliveri 0 siblings, 2 replies; 54+ messages in thread From: Martín Hötzel Escardó @ 2017-12-22 21:20 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 2520 bytes --] There may be some confusion about univalence and equality of subsets of a type. Univalence is compatible with the fact that two subsets A,B of a type X are equal iff they have the same elements. In fact, univalence implies that. Define Prop=Σ(P : U),isProp P where isProp(P:U) = Π(x,y:P),x=y. This is a large type (it lives in the same universe as U, rather than in U). You may wish to make this small (like in UniMath), or not, but this is orthogonal to this discussion. Then define the powerset of a type X by ℙ X = X → Prop. (As in topos theory.) Then for A : ℙ X and x : X we write x ∈ A to mean A x. (As in the internal language of a topos.) Then, assuming univalence, we have (theorem of intensional MLTT+UA): (A=B) = ∀(x:X), x ∈ A ⇔ x ∈ B. (Because the middle equality is that of two sets, we don't need to worry about which specific equality we pick - there is at most one. This again relies on univalence.) Without assuming univalence, we can't prove (or disprove) this equality. Not in intensional MLTT, or even in so-called extensional MLTT (= intensional MLTT + equality reflection). This is because in order to prove this equality, we need both functional and propositional extensionality. Extensional MLTT has the former but not the latter. Univalent MLTT has both. Here, the quantifier ∀ is a function of type (X → Prop) → Prop and the logical connective _⇔_ is a function Prop → Prop → Prop (or Prop × Prop → Prop, it doesn't matter). Now, from a subset A : ℙ X, we get a type A' and an embedding A' → X. (The construction works like this: we have A : X → Prop, and a projection Prop → U. Then the type A' is the sum (Σ) of composite function. The embedding is the first projection.) It is definitely not the case that if A'=B' for A,B : ℙ X then A=B. Example: X=ℕ, A=isEven and B=isOdd. Then A ≠ B but A'=B' (because A' and B' are isomorphic sets). However, we do have that ℙ X ≃ Σ (A' : U), Σ (e : A' → X), isEmbedding e, where (isEmbedding e) means that the fibers of e are propositions. Then the elements (Σ isEven, (_ , _)) and (Σ isOdd, (_ , _)) of the rhs type, for uniquely determined "_", are different, even though the types Σ isEven and Σ isOdd are equal. All the misunderstandings in the previous messages are caused by looking at the particular type X=1 without enough care. And I think this is what Thomas is pointing out. Best, Martin [-- Attachment #1.2: Type: text/html, Size: 7723 bytes --] ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-22 21:20 ` Martín Hötzel Escardó @ 2017-12-22 21:36 ` Martín Hötzel Escardó 2017-12-23 0:25 ` Matt Oliveri 1 sibling, 0 replies; 54+ messages in thread From: Martín Hötzel Escardó @ 2017-12-22 21:36 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 533 bytes --] Correction (that you already spotted, of course): On Friday, 22 December 2017 21:20:21 UTC, Martín Hötzel Escardó wrote: > > > Then, assuming univalence, we have (theorem of intensional MLTT+UA): > > (A=B) = ∀(x:X), x ∈ A ⇔ x ∈ B. > > (Because the middle equality is that of two sets, we don't need to > worry about which specific equality we pick - there is at most > one. This again relies on univalence.) > It is an equality of two *propositions*, of course, which is what I meant to say. M. [-- Attachment #1.2: Type: text/html, Size: 1288 bytes --] ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-22 21:20 ` Martín Hötzel Escardó 2017-12-22 21:36 ` Martín Hötzel Escardó @ 2017-12-23 0:25 ` Matt Oliveri 1 sibling, 0 replies; 54+ messages in thread From: Matt Oliveri @ 2017-12-23 0:25 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 892 bytes --] On Friday, December 22, 2017 at 4:20:21 PM UTC-5, Martín Hötzel Escardó wrote: > > There may be some confusion about univalence and equality of subsets > of a type. > > [...] > > Now, from a subset A : ℙ X, we get a type A' and an embedding A' → X. > (The construction works like this: we have A : X → Prop, and a > projection Prop → U. Then the type A' is the sum (Σ) of composite > function. The embedding is the first projection.) > > It is definitely not the case that if A'=B' for A,B : ℙ X then A=B. > > [...] > > All the misunderstandings in the previous messages are caused by > looking at the particular type X=1 without enough care. > > And I think this is what Thomas is pointing out. > Huh? Your isEven/isOdd example is fine, but there, X ≠ 1. Is it not the case that if A'=B' for A,B : ℙ 1 then A=B? (Note the specialization to 1.) [-- Attachment #1.2: Type: text/html, Size: 2422 bytes --] ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-19 13:52 ` Andrej Bauer 2017-12-19 14:44 ` Thorsten Altenkirch @ 2017-12-19 16:41 ` Steve Awodey 2017-12-20 0:14 ` Andrej Bauer 1 sibling, 1 reply; 54+ messages in thread From: Steve Awodey @ 2017-12-19 16:41 UTC (permalink / raw) To: Andrej Bauer; +Cc: Homotopy Type Theory > On Dec 19, 2017, at 8:52 AM, Andrej Bauer <andrej...@andrej.com> wrote: > >> I don’t understand this: HProps are subobjects of 1 hence they get classified as propositions. Hence there is an element of Omega corresponding to Sigle(a). > > I beleive a lot of the confusion in this discussion would go away if > we translated some of what Thomas is saying into a more syntactic > setup. We have to be a bit careful about what "corresponds to" means. > > To say that Ω classifies truth values, or h-propositions, means that: > > 1. There is a type Ω. > > 2. There is a type family El(p) indexed by p : Ω. > > 3. For every p : Ω the type El(p) is an h-prop (there's a term witnessing this). > > 4. For every h-prop P -- which is a type, not an element of Ω! -- > there is p : Ω such that P is equivalent to El(p). (Again we need a > term witnessing the equivalence.) > > Now, it may happen that h-props P and Q are both equivalent to El(r) > even though they are not equal. > > Furthermore, there can be class-many subobjects of 1 in a topos, for > instance in sets there are class-many singletons. Of course, a whole > lot of them will be isomorphic and very many "correspond to" the > element ⊤ : Ω. But at least on this mailing list we're not in the > business of sweeping isomorphisms under the rug. So far so good, but the last remark is a bit too cryptic. If this is supposed to be subobject classification in the sense of an elementary topos, then the p’s that “correspond to" isomorphic h-props still need to be identified. That’s univalence for Omega, of course, which does indeed hold in a topos. Otherwise, you are talking about a looser notion of “classification” of h-props. Steve > > With kind regards, > > Andrej > > -- > 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-19 16:41 ` Steve Awodey @ 2017-12-20 0:14 ` Andrej Bauer 2017-12-20 3:55 ` Steve Awodey 0 siblings, 1 reply; 54+ messages in thread From: Andrej Bauer @ 2017-12-20 0:14 UTC (permalink / raw) To: Steve Awodey; +Cc: Homotopy Type Theory > If this is supposed to be subobject classification in the sense of an elementary topos, > then the p’s that “correspond to" isomorphic h-props still need to be identified. > That’s univalence for Omega, of course, which does indeed hold in a topos. Isn't Thomas's point that the p's that correspond to isomorphic h-props are *equal*, and that there is only one reasonable notion of equality in a topos, which is extensional equality? With kind regards, Andrej ^ permalink raw reply [flat|nested] 54+ messages in thread
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? 2017-12-20 0:14 ` Andrej Bauer @ 2017-12-20 3:55 ` Steve Awodey 0 siblings, 0 replies; 54+ messages in thread From: Steve Awodey @ 2017-12-20 3:55 UTC (permalink / raw) To: Homotopy Type Theory Yes, that’s fine, but it wasn’t part of your reformulation (at least not explicitly). Steve Sent from mobile - sorry fr typos. On Dec 19, 2017, at 19:14, Andrej Bauer <andrej...@andrej.com> wrote: >> If this is supposed to be subobject classification in the sense of an elementary topos, >> then the p’s that “correspond to" isomorphic h-props still need to be identified. >> That’s univalence for Omega, of course, which does indeed hold in a topos. > > Isn't Thomas's point that the p's that correspond to isomorphic > h-props are *equal*, and that there is only one reasonable notion of > equality in a topos, which is extensional equality? > > With kind regards, > > Andrej ^ permalink raw reply [flat|nested] 54+ messages in thread
[parent not found: <fa8c0c3c-4870-4c06-fd4d-70be992d3ac0@skyskimmer.net>]
* Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? [not found] ` <fa8c0c3c-4870-4c06-fd4d-70be992d3ac0@skyskimmer.net> @ 2017-12-14 13:28 ` Thorsten Altenkirch 0 siblings, 0 replies; 54+ messages in thread From: Thorsten Altenkirch @ 2017-12-14 13:28 UTC (permalink / raw) To: Gaëtan Gilbert, homotopyt...@googlegroups.com I guess you are concerned that while singleton is contractible in HoTT, this is not true if we use an equality which is always propositional However, since I am talking about set-level HoTT, I am assuming A:Set (that is HSet). Btw, I meant Single(a) : HProp (since there is the other static Prop as well). But I think Mike’s comment nails it. Thorsten On 14/12/2017, 13:03, "homotopyt...@googlegroups.com on behalf of Gaëtan Gilbert" <homotopyt...@googlegroups.com on behalf of gaetan....@skyskimmer.net> wrote: >We have Single(a) : Prop How do we have this without truncating (which means we don't have projections)? Gaëtan Gilbert On 12/12/2017 12:03, Thorsten Altenkirch wrote: > 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" <sanz...@gmail.com> wrote: > >> On Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenkirch >> <Thorsten....@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 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" <homotopyt...@googlegroups.com on behalf of 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 >>> >>> -- >>> 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. 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. ^ permalink raw reply [flat|nested] 54+ messages in thread
end of thread, other threads:[~2017-12-23 0:25 UTC | newest] Thread overview: 54+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2017-12-11 4:22 Impredicative set + function extensionality + proof irrelevance consistent? Kristina Sojakova 2017-12-11 11:42 ` [HoTT] " Jon Sterling 2017-12-11 12:15 ` Kristina Sojakova 2017-12-11 12:43 ` Jon Sterling 2017-12-11 14:28 ` Thomas Streicher 2017-12-11 14:32 ` Kristina Sojakova 2017-12-11 14:23 ` Thorsten Altenkirch 2017-12-12 10:15 ` Andrea Vezzosi 2017-12-12 11:03 ` Thorsten Altenkirch 2017-12-12 12:02 ` Thomas Streicher 2017-12-12 12:21 ` Thorsten Altenkirch 2017-12-12 13:17 ` Jon Sterling 2017-12-12 19:29 ` Thomas Streicher 2017-12-12 19:52 ` Martin Escardo 2017-12-12 23:14 ` Michael Shulman 2017-12-14 12:32 ` Thorsten Altenkirch 2017-12-14 18:52 ` Michael Shulman 2017-12-16 15:21 ` Thorsten Altenkirch 2017-12-17 12:55 ` Michael Shulman 2017-12-17 17:08 ` Ben Sherman 2017-12-17 17:16 ` Thorsten Altenkirch 2017-12-17 22:43 ` Floris van Doorn 2017-12-15 17:00 ` Thomas Streicher 2017-12-17 8:47 ` Thorsten Altenkirch 2017-12-17 10:21 ` Thomas Streicher 2017-12-17 11:39 ` Thorsten Altenkirch 2017-12-18 7:41 ` Matt Oliveri 2017-12-18 10:00 ` Michael Shulman 2017-12-18 11:55 ` Matt Oliveri 2017-12-18 16:24 ` Michael Shulman 2017-12-18 20:08 ` Matt Oliveri 2017-12-18 10:10 ` Thorsten Altenkirch 2017-12-18 11:17 ` Matt Oliveri 2017-12-18 12:09 ` Matt Oliveri 2017-12-18 11:52 ` Thomas Streicher 2017-12-19 11:26 ` Thorsten Altenkirch 2017-12-19 13:52 ` Andrej Bauer 2017-12-19 14:44 ` Thorsten Altenkirch 2017-12-19 15:31 ` Thomas Streicher 2017-12-19 16:10 ` Thorsten Altenkirch 2017-12-19 16:31 ` Thomas Streicher 2017-12-19 16:37 ` Thorsten Altenkirch 2017-12-20 11:00 ` Thomas Streicher 2017-12-20 11:16 ` Thorsten Altenkirch 2017-12-20 11:41 ` Thomas Streicher 2017-12-21 0:42 ` Matt Oliveri 2017-12-22 11:18 ` Thorsten Altenkirch 2017-12-22 21:20 ` Martín Hötzel Escardó 2017-12-22 21:36 ` Martín Hötzel Escardó 2017-12-23 0:25 ` Matt Oliveri 2017-12-19 16:41 ` Steve Awodey 2017-12-20 0:14 ` Andrej Bauer 2017-12-20 3:55 ` Steve Awodey [not found] ` <fa8c0c3c-4870-4c06-fd4d-70be992d3ac0@skyskimmer.net> 2017-12-14 13:28 ` Thorsten Altenkirch
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).