[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> Le 6 juil. 2019 à 03:44, Martin Escardo <[email protected]> a écrit : > > [ 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. … and this complete lattice gives you a Tarski fixed point theorem, on which the Paco library for coinductive reasoning is built, making use of Mendler-style recursion (also requiring impredicativity). — Matthieu > 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
