System F_{ω} appears impredicative, but I'm wondering if there is an easy way to embed it into predicative dependent type theory by inferring bounds on universes. Also, if anyone can provide an example of a System F_{ω} term that would be rejected by Coq's typical ambiguity resolver, that would be helpful to me.

Any references or thought are appreciated.

## Recent comments

4 days 7 hours ago

6 days 2 hours ago

2 weeks 3 days ago

3 weeks 2 days ago

4 weeks 2 days ago

6 weeks 8 hours ago

6 weeks 3 days ago

7 weeks 4 days ago

8 weeks 11 hours ago

8 weeks 14 hours ago