The Coq mailing list

[Andrés Sicard-Ramírez <asr AT eafit.edu.co>]

On 4 September 2014 19:47, Daniel Schepler 
<dschepler AT gmail.com>
 wrote:
>> In p. 60, Coquand and Paulin wrote:
>>
>> Proposition: For any type A, there cannot be an intensional injection
>>
>>   ((A → Prop) → Prop) → A.
>>
>> Proof: For any type X there is an intensional injection
>>
>>   X → (X → Prop)
>>
>> which is ... Hence, by composition, we get an intensional injection
>>
>>   f : (A → Prop) → A.
>>
>> Question: How I get the function f?
>
> Set X := (A -> Prop)?

Of course. Thanks!


-- 
Andrés