@dzaima Preliminary spec for identity values
here. I decided to restrict it to right identities since I can't figure out how to justify left ones. That cuts out
√|<≤
, which seems to me to be a good thing. I also allow an identity that only works on the range of the function, which makes
≠
and
=
work. Largest invariant set (a subset of the range) might be more precise but I can't think of a situation where it would matter.