[TYPES] Example uses of impredicativity

[Martin Escardo]

One example is the powerset P X of a type X, defined as the type X -> 
Prop of functions into Prop. Without the impredicativity of Prop, you 
are not able to construct a function P(P X) -> P X that gives the union 
of a set of sets. Also Prop itself wouldn't be a complete lattice with a 
join function P Prop -> Prop in the absence of impredictivity. Martin

On 05/07/2019 23:08, monnier at iro.umontreal.ca wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Hi,
> 
> I was recently reminded that not only I only understand impredicativity
> in a very superficial way, but on top of that, I don't know of many
> uses of it.
> 
> Basically, I know of its use in Church encodings, in Shao et. al.'s λₕ
> (from Type-safe Certified Binaries, which I also used in my "swiss
> coercion"), as well as in type-preserving closure conversion, but that's
> pretty much it.
> 
> When I started to look for examples in Coq, I soon realized that many
> Coq libraries have definitions whose universe level is affected by
> impredicativity but it's a lot more work to discover if the same
> development would work as well without impredicativity.
> 
> Is there some place where I could find a kind of "collection" of
> developments/techniques which rely on impredicativity?
> 
> Short of that, I'd be happy to hear from examples which
> I could assemble to make such a collection.
> 
> 
>          Stefan
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe