Moved various induction pattern constructions out of HoTT into Context
basic inductive type traits
clean up of universes