Primary doctrines present a fragment of first order logic over a base category. Primary doctrines need not have internal notions of equality, but Pasquali showed we can add one cofreely by taking "quotients" by all possible equivalence relations. In this talk we will show that in the proof relevant generalisation of primary doctrines, called primary fibrations, we can also cofreely add equality. Here internal groupoids play the role of equivalence relations.