Mientras formalizaba el Álgebra Abstracta de Dummit y Foote en Rocq durante mi segunda semana en el Recurse Center, encontré que el objetivo del primer ejercicio de prueba era falso. La proposición afirma que una función es inyectiva si y solo si tiene inversa por la izquierda. Pero existe un contraejemplo: sea A vacío y B = {1}.

La función vacía f: A -> B es inyectiva vacuamente, sin embargo no existe función g: B -> A porque B es no vacío y A es vacío. Este caso límite es fácil de pasar por alto en papel, pero Rocq me obligó a enfrentarlo. Después de luchar, revisé la fe de erratas del libro y lo encontré listado.

Fue frustrante pero emocionante descubrirlo de manera independiente.