This PR removes the practically empty module Cubical.Relation.Nullary.DecidableEq. The contents of this module were moved to Cubical.Relation.Nullary.Properties in https://github.com/agda/cubical/pull/333. It contained only two re-exports since then. And it seems like these re-exports aren't used anywhere. (Every module that needs them imports Cubical.Relation.Nullary.Properties anyway.)
In case people see reasons to keep Cubical.Relation.Nullary.DecidableEq, I would also be happy to just remove the unused imports.
This PR removes the practically empty module
Cubical.Relation.Nullary.DecidableEq. The contents of this module were moved toCubical.Relation.Nullary.Propertiesin https://github.com/agda/cubical/pull/333. It contained only two re-exports since then. And it seems like these re-exports aren't used anywhere. (Every module that needs them importsCubical.Relation.Nullary.Propertiesanyway.)In case people see reasons to keep
Cubical.Relation.Nullary.DecidableEq, I would also be happy to just remove the unused imports.