Domain theory in constructive and predicative univalent foundations