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

[Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>]

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.