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

[Kristina Sojakova <sojakova...@gmail.com>]

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.