$$\def\mapright#1{\xrightarrow{{#1}}} \def\mapdown#1{\Big\downarrow\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagl#1{\vcenter{\searrow}\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagr#1{\vcenter{\swarrow}\rlap{\raise2pt{\scriptstyle{#1}}}} $$

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


Definition (Fiber). The fiber of the map $p: E \rightarrow B$ in a point $y: B$ is all points $x: E$ such that $p(x)=y$.

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

Fiber Bundle

Definition (Fiber Bundle). The fiber bundle $ F \rightarrow E \mapright{p} B$ on a total space $E$ with fiber layer $F$ and base $B$ is a structure $(F,E,p,B)$ where $p: E \rightarrow B$ is a surjective map with following property: for any point $y: B$ exists a neighborhood $U_b$ for which a homeomorphism $f: p^{-1}(U_b) \rightarrow U_b \times F$ making the following diagram commute.

$$ \begin{array}{ccc} p^{-1}(U_b) & \mapright{f} & U_b \times F \\ \mapdown{\mathbf{p}} & \mapdiagr{pr_1} & \\ U_b & & \\ \end{array} $$

Trivial Fiber Bundle

Definition (Trivial Fiber Bundle). When total space $E$ is cartesian product $\Sigma(B,F)$ and $p = pr_1$ then such bundle is called trivial $(F,\Sigma(B,F),pr_1,B)$.

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

Theorem (Fiber in a trivial total space is a family over base). Inverse image (fiber) of fiber bundle $(F,B*F,pr_1,B)$ in point $y:B$ equals $F(y)$. 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 $isoPath$ lemma and $encode/decode$ 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>[email protected]) 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 $F$-fiber bundle is just Aut(F), the loop space of BAut(F).