Recurse Centerでの2週目に、RocqでDummitとFooteの『抽象代数』を形式化しているとき、最初の証明演習のゴールが偽であることに気づきました。その命題は、関数が単射であることと左逆写像を持つことが同値であると主張しています。しかし反例が存在します：Aを空集合、B = {1}とします。空関数f: A -> Bは空虚に単射ですが、Bが非空でAが空であるため、関数g: B -> Aは存在しません。このコーナーケースは紙面上では見逃しやすいですが、Rocqはそれに直面せざるを得ませんでした。苦労した後、本の正誤表を確認し、それが記載されているのを見つけました。もどかしいですが、独立に発見できて興奮しました。