agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
446 stars 136 forks source link

Generalize types of inspect idiom #1041

Closed dolio closed 11 months ago

dolio commented 11 months ago

This generalizes some types to allow doing an inspect of a dependent function. I've found myself wanting this from time to time, and I haven't noticed the generalization having any adverse effects (I think the fact that f is an argument nails down potential ambiguities about B).