From Dependent Type Theory to Higher Algebraic Structures