Impredicative set + function extensionality + proof irrelevance consistent?

Impredicative set + function extensionality + proof irrelevance consistent?

[Kristina Sojakova]

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

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Jon Sterling]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Kristina Sojakova]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Jon Sterling]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thorsten Altenkirch]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thomas Streicher]

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

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Kristina Sojakova]

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
>

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Andrea Vezzosi]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thorsten Altenkirch]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thomas Streicher]

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.
> 

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thorsten Altenkirch]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Jon Sterling]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thomas Streicher]

> 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

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Martin Escardo]

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

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Michael Shulman]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thorsten Altenkirch]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thorsten Altenkirch]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Michael Shulman]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thomas Streicher]

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 :-)

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thorsten Altenkirch]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thorsten Altenkirch]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thomas Streicher]

> >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

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thorsten Altenkirch]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Michael Shulman]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Ben Sherman]

[-- 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 --]

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thorsten Altenkirch]

[-- 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 --]

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Floris van Doorn]

[-- 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 --]

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Matt Oliveri]

[-- 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 --]

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Michael Shulman]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thorsten Altenkirch]

[-- 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 --]

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Matt Oliveri]

[-- 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 --]

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thomas Streicher]

> >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

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Matt Oliveri]

[-- 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 --]

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Matt Oliveri]

[-- 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 --]

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Michael Shulman]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Matt Oliveri]

[-- 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 --]

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thorsten Altenkirch]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Andrej Bauer]

> 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

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thorsten Altenkirch]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thomas Streicher]

>     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

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thorsten Altenkirch]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thomas Streicher]

> 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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thorsten Altenkirch]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Steve Awodey]

> 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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Andrej Bauer]

> 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

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Steve Awodey]

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

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thomas Streicher]

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

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thorsten Altenkirch]

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.

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thomas Streicher]

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

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Matt Oliveri]

[-- 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 --]

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Thorsten Altenkirch]

[-- 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 --]

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Martín Hötzel Escardó]

[-- 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 --]

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Martín Hötzel Escardó]

[-- 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 --]

Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Matt Oliveri]

[-- 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 --]