Comment by mietek

Roughly, yes. See B. Werner (1997) “Sets in types, types in sets”.