Decidability in a set-valued functor category (source code)

= Decidability in a set-valued functor category

A covariant set-valued functor $F$ is a decidable object precisely when every transition map $F(u)$ is injective. The pointwise complement of its diagonal consists of unequal pairs; it is a subfunctor exactly when transition maps preserve inequality. For left <M-sets>, this says that every action map is injective.