Module mathcomp.analysis.homotopy_theory.wedge_sigT

# wedge sum for sigT A foundational construction for homotopy theory. It glues a dependent sum at a single point. It's classicaly used in the proof that every free group is a fundamental group of some space. We also will use it as part of our construction of paths and path concatenation. ``` wedge_rel p0 x y == x and y are equal, or they are (p0 i) and (p0 j) for some i and j wedge p0 == the quotient of {i : X i} along `wedge_rel p0` wedge_lift i == the lifting of elements of (X i) into the wedge pwedge p0 == the wedge of ptopologicalTypes at their designated point wedge_fun f == lifts a family of functions on each component into a function on the wedge, when they all agree at the wedge point wedge_prod == the mapping from the wedge as a quotient of sums to the wedge as a subspace of the product topology. It's an embedding when the index is finite. bpwedge_shared_pt b == the shared point in the bpwedge. Either zero or one depending on `b`. bpwedge == wedge of two bipointed spaces gluing zero to one bpwedge_lift == wedge_lift specialized to the bipointed wedge ``` The type `wedge p0` is endowed with the structures of: - topology via `quotient_topology` - quotient The type `pwedge` is endowed with the structures of: - topology via `quotient_topology` - quotient - pointed The type `bpwedge` is endowed with the structures of: - topology via `quotient_topology` - quotient - bipointed