The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Thu, Sep 4, 2014 at 5:30 PM, Andrés Sicard-Ramírez 
<asr AT eafit.edu.co>
 wrote:
> On 4 September 2014 08:04, Frédéric Blanqui 
> <frederic.blanqui AT inria.fr>
>  wrote:
>> Non-strictly positive types are not necessarily inconsistent. In 
>> Inductively
>> defined types, COLOG'88, Thierry Coquand and Christine Paulin show that a
>> particular "big" non-strictly positive type is inconsistent (section 3.1,
>> page 59).
>
> 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)?
-- 
Daniel Schepler