-type is a space that contains dependent functions, which
codomain type depends on value from domain type. As fiber domain
present in every defined function, -type is also a dependent product.

Spaces of dependent functions are using in type theory to model
various mathematical constructions, objects, types, or spaces and their maps:
dependent functions, continuous maps, étale maps, fibre bundles, universal
quantifier -type, implications, etc.

Formation

(-Formation, Dependent Product).
-types represents the way we create the spaces of dependent functions
with domain in and codomain in type family over .

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

When codomain is not dependent on valude from domain the function
is studied in System F, dependent case in studied
in Systen P or Calculus of Construction (CoC).

Elimination

(-Induction Principle). States that
if predicate holds for lambda function
then there is a function from function space to the space of predicate.

def П-ind (A :U)(B : A -> U)(C : Pi A B →U)(g: Π (x: Pi A B), C x): П (p: Pi A B), C p
:= \ (p: Pi A B), g p

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

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

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

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

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

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

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

def piIsContr (A:U)(B: A -> U)(u: isContr A)(q: П (x: A), isContr (B x)): isContr (Pi A B) def pathPi (A:U)(B: A -> U)(f g : Pi A B):PathU(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: