BUNDLE

Bundle package contains basic information about fibers (needed for weak-equivalence) and fiber bundles, constructions from algebraic topology.

Fiber

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

fiber (E B: U) (p: E -> B) (y: B): U
    = (x: E) * Path B y (p x)

Fiber Bundle

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

Trivial Fiber Bundle

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

Family (B: U): U = B -> U

total (B: U) (F: Family B): U = Sigma B F
trivial (B: U) (F: Family B): total B F -> B = \ (x: total B F) -> x.1
homeo (B E: U) (F: Family B) (p: E -> B) (y: B) :
           fiber E B p y -> total B F

Fiber is a Dependent Family

(Fiber in a trivial total space is a family over base). Inverse image (fiber) of fiber bundle in point equals . Thre proof sketch is following:

F y = (_: isContr B) * (F y)
    = (x y: B) * (_: Path B x y) * (F y)
    = (z: B) * (k: F z) * Path B z y
    = (z: E) * Path B z.1 y
    = fiber (total B F) B (trivial B F) y

The equality is proven by lemma and functions.

encode (B: U) (F: B -> U) (y: B)
     : fiber (total B F) B (trivial B F) y -> F y
     = \ (x: fiber (total B F) B (trivial B F) y)
      -> subst B F x.1.1 y (<i>x.2@-i) x.1.2

decode (B: U) (F: B -> U) (y: B)
     : F y -> fiber (total B F) B (trivial B F) y
     = \ (x: F y) -> ((y,x),refl B y)

lem2 (B: U) (F: B -> U) (y: B) (x: F y)
   : Path (F y) (comp (<_> F y) x []) x
   = <j> comp (<_> F y) x [ (j=1) -> <_> x]

lem3 (B: U) (F: B -> U) (y: B) (x: fiber (total B F) B (trivial B F) y)
   : Path (fiber (total B F) B (trivial B F) y) ((y,encode B F y x),refl B y) x
   = <i> ((x.2 @ -i,comp (<j> F (x.2 @ -i /\ j)) x.1.2 [(i=1) -> <_> x.1.2 ]),<j> x.2 @ -i \/ j)

TrivialFiberBundleEqualsPi (B: U) (F: Family B) (y: B)
    : Path U (fiber (total B F) B (trivial B F) y) (F y)
    = isoPath T A f g s t where
    T: U = fiber (total B F) B (trivial B F) y
    A: U = F y
    f: T -> A = encode B F y
    g: A -> T = decode B F y
    s (x: A): Path A (f (g x)) x = lem2 B F y x
    t (x: T): Path T (g (f x)) x = lem3 B F y x

G-structure

The structure group of an -fiber bundle is just , the loop space of .