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.