search

agda / cubical

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

Some miscellaneous separated/stable type facts #1030

Closed dolio closed 1 year ago

dolio commented 1 year ago

Added separatedness of Bool

Added some convenient functions for deriving Stable and Separated for e.g. functions.

These were some general facts I found useful while working on some other stuff, sort of similar to various h-level combinators.

MatthiasHu commented 1 year ago

I will merge this when the CI is done.