coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Non-strict positivity and impredicativity

From: Stefan Monnier <monnier AT iro.umontreal.ca>
To: Fredrik Nordvall Forsberg <fredrik.nordvall-forsberg AT strath.ac.uk>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Non-strict positivity and impredicativity
Date: Wed, 18 Mar 2020 20:06:32 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=monnier AT iro.umontreal.ca; spf=Pass smtp.mailfrom=monnier AT iro.umontreal.ca; spf=None smtp.helo=postmaster AT mailscanner.iro.umontreal.ca
Ironport-phdr: 9a23:aAyqMBRvNB4L9NOmLkHz2NfyKtpsv+yvbD5Q0YIujvd0So/mwa64ZxeN2/xhgRfzUJnB7Loc0qyN7PCmBDRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnY6Uy/yPgttJ+nzBpWaz4Huj7jzqNXvZFBmnjexe7JxZDOxtwnPv80SyaVlML07xwHG6i9GYela32JrY1SUhRri78O0uZBk6T9atugu39VcS6zmf+IxRvpFD2J1HXoy4ZjQqRTNRA3Hw3waVGQbiFIcBg/D6hD3RL/wqCy8q+963jWAMMTyC7s9D2fxp5x3QQPl3X9UfwUy93va34kp1PoC8UCR4idnyouRW7m7cf93f6fTZ9QfHDoTX9xWETFEBYWgdYYGC6wKNLQB9tWvlx41tRK7QDKUKqb30DYR1i33x6p8zuEmFx3c0QUkWdkH4iyN8YfFcZwKWOXw95HmiDXOa/QNgWX44YnMaRsop/eBR/Rxa82X1EwoER/fg1yU74fsbWuY

>> Would it be possible to define an injective function from `X : Type` to
>> `X → Prop` if it weren't for Coq's impredicative treatment of indices?
> You can use Leibniz equality, which lives in Prop thanks
> to impredicativity:
>
> Definition leibniz {X : Type}(a b:X) : Prop := forall P:X -> Prop, P a ->
> P b.

Duh, indeed that's sufficient to push the proof through, thank you.

So there are 2 places where impredicativity is used in the proof.

Would it be possible to define an injective function from `X : Type` to
`X → Prop` if it weren't for Coq's impredicativity?

Stefan

[Coq-Club] Non-strict positivity and impredicativity, Stefan Monnier, 03/17/2020
- Re: [Coq-Club] Non-strict positivity and impredicativity, Fredrik Nordvall Forsberg, 03/18/2020
  - Re: [Coq-Club] Non-strict positivity and impredicativity, Stefan Monnier, 03/19/2020