# pi

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

```
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.

## Application

```
app (A : U) (B: A -> U)
(a : A) (f: A -> B a): B a = f a
```

Application is correspondent Lambda eliminator.