Pi package contains basic theorems about sigma types. Sigma type is built in core.
Pi (A: U) (P: A->U): U = (x: A) -> P x
All the constructions on $\Pi$-types arise as straightforward generalizations of the ones for function types. The type of function codomain is allowed to be perametrized by the value from the domain type.
intro (A : U) (B: A -> U) (a : A) (b: B a): A -> B a = \(x: A) -> b
Lambda constructor is also built in core as primitive. It defines the element of functional space.
app (A : U) (B: A -> U) (a : A) (f: A -> B a): B a = f a
Application is correspondent Lambda eliminator.