is a dependent function type, the generalization of functions.
As a function it can serve the wide range of mathematical constructions,
objects, types, or spaces. The known domain and codomain spaces could be:
depndent functions itself, sets, polynomial functors, -groupoids,
cw-complexes, categories, languages, processes, protocols, etc.

In Category Theory is called dependent product as right adjoint of base change.

Formation

(-Formation). -types represents the way we create
the spaces of dependent functions from type family B of functions over type A.

def Pi (A :U)(B : A →U):U:= Π (x : A), B x

Introduction

(-function).
Lambda constructor defines a new lambda function in the space of dependent functions.
it is called lambda abstraction and displayed as or .

def lambda (A:U)(B: A →U)(b: Pi A B): Pi A B := λ (x : A), b x
def lam (A B:U)(f: A → B): A → B := λ (x : A), f x

Elimination

(Application).
Application reduces the term by using recursive substitution.

def apply (A:U)(B: A →U)(f: Pi A B)(a: A): B a := f a
def app (A B:U)(f: A → B)(x: A): B := f x

(Composition).
Composition is using application of appropriate singnatures.

(Computation ).
-rule shows that composition could be fused.

def Π-β (A :U)(B : A →U)(a : A)(f : Pi A B): Path (B a)(apply A B (lambda A B f) a)(f a):= idp (B a)(f a)

Uniqueness

(Uniqueness ).
-rule shows that composition could be fused.

def Π-η (A :U)(B : A →U)(a : A)(f : Pi A B): Path (Pi A B) f (λ (x : A), f x):= idp (Pi A B) f

Theorems

(Functions Preserve Paths). For a function
there is an . This is called
application of to path or congruence property (, for non-dependent case).
This property behaves functoriality as if paths are groupoid morphisms and types are objects.

(Trivial Fiber equals Family of Sets).
Inverse image (fiber) of fiber bundle in point equals .

FiberPi (B:U)(F: B -> U)(y: B): Path U(fiber (Sigma B F) B (pi1 B F) y)(F y)

(Homotopy Equivalence). If fiber space is set for all base, and
there are two functions and two
homotopies between them, then these homotopies are equal.

setPi (A:U)(B: A -> U)(h:(x: A) -> isSet (B x))(f g: Pi A B)(p q: Path (Pi A B) f g): Path (Path (Pi A B) f g) p q

(HomSet). If codomain is set then space of sections is a set.

setFun (A B :U)(_: isSet B): isSet (A -> B)

(Contractability). If domain and codomain is contractible then
the space of sections is contractible.

piIsContr (A:U)(B: A -> U)(u: isContr A)(q:(x: A) -> isContr (B x)): isContr (Pi A B) pathPi (A:U)(B:A->U)(f g : Pi A B): Path U(Path (Pi A B) f g)((x:A) -> Path (B x)(f x)(g x))

Interpretations

Homotopy Theory

Geometrically, -type is a space of sections,
while the dependent codomain is a space of fibrations.
Lambda functions are sections or points in these spaces,
while the function result is a fibration.

(Fiber). The fiber of the map in a point
is all points such that .

(Fiber Bundle). The fiber bundle on a
total space with fiber layer and base is a
structure where is a surjective
map with following property:
for any point exists a neighborhood for which a
homeomorphism
making the following diagram commute.

(Cartesian Product of Family over B). Is a set
of sections of the bundle with elimination map .
such that
is a product projection, so , are moriphisms
of slice category . The universal mapping property of :
for all and morphism in exists
unique map such that everything commute. So a category
with all dependent products is necessarily a category with all pullbacks.

(Trivial Fiber Bundle).
When total space is cartesian product
and then such bundle is called trivial .

Category Theory

Categorically, -types arise in locally cartesian closed categories.
In this case -type represents the cartesian family of sets,
generalizing the cartesian product of sets or dependent product.

(Section). A section of morphism
in some category is the morphism such that
equals the identity morphism on B.

(Dependent Product). The dependent product along
morphism in category is the right
adjoint of the base change functor.

(Space of Sections). Let be
a -topos, and let a bundle in
, object in the slice topos. Then the space of sections
of this bundle is the Dependent Product: