Commit 2021-07-07 13:35 5796783b
View on Github →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.