Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
It looks like for this entry it is important to declare what is meant by “morphism” and to refer to hom type.
So after the word “morphism” I have added a parenthetical
also I touched the formatting of the formula that now looks as follows:
$\big(x \cong_A y\big) \;\;\coloneqq\;\; \sum_{ \mathclap{ f \colon \mathrm{hom}_A(x, y) } } \mathrm{isIso}(f)$1 to 2 of 2