mathlib3

5796783b - chore(category_theory): homogenise usage of notation for terminal objects (#8106)

chore(category_theory): homogenise usage of notation for terminal objects (#8106) I went with the option that is used more frequently, but I'm also happy to switch to the space-less option if people prefer it.