DEPENDENT PRODUCT

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.

def ∘ᵀ (α β γ: U) : U := (β → γ) → (α → β) → (α → γ)
def ∘ (α β γ : U) : ∘ᵀ α β γ := λ (g: β → γ) (f: α → β) (x: α), g (f x)

Computation

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