A suitable notion of model for type theory without extensionality principle for predicate seems to be the following : C is a weak topos iff C is locally cartesian closed and there exists a generic mono g , i.e. any mono of C can be obtained as a pullback of g (that I would call a weak subobject classifier). Such a category is automatically regular (as one can define existential quantification in the internal logic). Now if one takes TOP(C) = Map(Split(Rel(C))) one gets a topos. Alternatively one could take the fibration of monos over C thus getting a tripos and perform the construction of the associated topos. Now my question are the following : Under which conditions is C the category of separated objects of TOP(C) ? For which toposes E is Sep(E) a weak topos in the sense of my definition ? We know that the effective topos is an example BUT is it possible for non-boolean Grothendieck toposes ? Thomas Streicher ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++