On the role of description

AbstractIn a topos, the characteristic arrow of a diagonal is called “internal equality”. It is natural to wonder if axiomatizing internal equality, through a “diagonal classifier”, instead of the subobject classifier, would be enough in order to have a topos. We prove that the answer is no, but that it becomes yes, if we add a single axiom, asking for the existence of a “description operator”, which enables to “peek” the sole element of any singleton. In a linguistic conclusion, we explain how this illuminates the role of sentences like “the unique x in A, such that …”, in ordinary mathematical language