Commit 2025-12-07 10:19 b32362e5

View on Github →

chore(CategoryTheory): remove use of erw in ι_gluedIso_hom (#32523)

Estimated changes