The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

Oh, yes, sure !

In fact, inhabited T -> T is proved by epsilon, if I am not mistaken.

-- 
JH


Le 10/03/2016 18:11, Pierre-Marie Pédrot a écrit :
> On 10/03/2016 18:09, Jacques-Henri Jourdan wrote:
>> If I remember correctly, this restriction is important to soundness :
>> because Prop is impredicative, we can build a proof of false from
>> inhabited T -> T.
> I'm not sure this is sufficient. IIRC, you need to assume in addition
> that this function is the inverse of the inhabits constructor, otherwise
> you won't be able to do much with this function alone.
>
> PMP
>

Attachment: signature.asc
Description: OpenPGP digital signature