feat(category/is_iso): make is_iso a Prop (#6662)
Perhaps long overdue, this makes `is_iso` into a Prop.
It hasn't been a big deal, as it was always a subsingleton. Nevertheless this is probably safer than carrying data around in the typeclass inference system.
As a side effect `simple` is now a Prop as well.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
