I think that's because, before the HoTT extensions, all definable types could be seen as in the Category of Sets. And they didn't get rid of Set and Prop entir

I think that's because, before the HoTT extensions, all definable types could be seen as in the Category of Sets. And they didn't get rid of Set and Prop entirely. They just made them default-imported symbols instead of keywords.