Per Martin-Löf‘s dependent type theory, also known as intuitionistic or constructive type theory, is a foundation for constructive mathematics notably using П-types, Σ-types, and W-types.

References:
nLab
Intuitionistic Type Theory