FUNCTION SPACES

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

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.

def FiberPi (B: U) (F: B -> U) (y: B)
  : Path U (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)
  : 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: