I got at least an interesting comment on my question. It seems that what I'm trying to do is very much not trivial. Johnstone had a conjecture about the first order sentences of the generic model for the theory of pure equality that he couldn't confirm or refute for over a decade.

@MaliceVidrine And you got an answer too.

@user21820 - I just saw that. And Ingo is someone I've been following anyway, so my hopes are raised.

@MaliceVidrine What are you referring to? In my type theory, there is a universal type called obj, and I see no reason anyone should dispute the well-defined-ness of it. Anything and everything is a member of it. =)

I.e. ∀x∈obj ( x∈obj ), and obj∈obj.

@MaliceVidrine That's great! Anyway, sorry got to go. Talk to you again next time!

This was someone talking about standard set theory, and not wanting to call the things in the domain of quantification "objects". It's a context where it clearly did not mean a special class or type like Obj.