The Coq mailing list

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

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?

All the best,

-- 
Andrés