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

[Matt Oliveri <atm...@gmail.com>]

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