[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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, [email protected] 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
