+-- |Type class for indirectly equality-comparable types. That is, any
+-- @α@ of @'Eq'' α@ has a monomorphism to some
+-- equality-comparable type @γ@ while @α@ itself isn't
+-- necessarily an instance of 'Eq'. This way we can generalise the
+-- '==' operator so that it can take two different types as long as
+-- they both have monomorphisms to the same 'Eq' type @γ@.
+--
+-- Minimal complete definition: 'Unified' and 'unify'.