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.