Формализуя абстрактную алгебру Даммита и Фута в Rocq на второй неделе в Recurse Center, я обнаружил, что цель первого упражнения на доказательство ложна. Утверждение гласит, что функция инъективна тогда и только тогда, когда она имеет левый обратный. Но существует контрпример: пусть A пусто, а B = {1}. Пустая функция f: A -> B вакуумно инъективна, однако не существует функции g: B -> A, потому что B непусто, а A пусто. Этот крайний случай легко упустить на бумаге, но Rocq заставил меня с ним столкнуться. После борьбы я проверил список опечаток в книге и нашёл его там. Это было неприятно, но захватывающе обнаружить это самостоятельно.