------------- Thomas Streicher pointed out a problem in my definition of the "canonically separated" objects for triposes based on PCAs (and recall this does not simply mean the tripos given by a PCA in the most direct way). The correct definition is: The tripos construction of a topos takes as objects all pairs (X,=) where "=" is a partial equivalence relation in the sense of the tripos on the set X. To get a category of assemblies instead, take only those pairs (X,=) where = is contained (in the tripos sense) in (Exist)(delta_X)(true) In other words, those = contained in the "direct image" along the diagonal function for the set X of the maximal predicate (in the tripos sense) on X. Call these the "canonically separated" objects. In the case of the effective topos this agrees with Hyland's usage. The rest works as in the original post. These objects can be represented by assemblies and the arrows between them as ordinary set theoretic functions with moduli. That gives a regular category whose effective reflection is the topos given by the tripos. The assemblies are (up to iso) precisely the separated objects of the topos. Colin McLarty ==============================================================================