Implicit products are a fascinating approach to universal quantification in dependent type theory, as well as proof irrelevance/erasure in compiler implementation.

I wrote this post to bring some awareness to a really cool idea. It is a crucial piece of Cedille's type theory.