Equality in computer proof-assistants

Equality is fundamental notion of logic and mathematics as a whole. If computer-supported formalization of knowledge is taken into account, sooner or later one should precisely declare the intended meaning/interpretation of the primitive predicate symbol of equality. In the paper we draw some issues how computerized proof-assistants can deal with this notion, and at the same time, we propose solutions, which are not contradictory with mathematical tradition and readability of source code. Our discussion is illustrated with examples taken from the implementation of the MIZAR system.