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


(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


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