Connectedness

This reduces universe variables in conn_pointed_type and conn_point_elim, which refer to Unit.

There is a slight controversy of indexing for connectedness — in particular, how the indexing for maps shoud relate to the indexing for types. One may reasonably take the connectedness of a map to correspond either to that of its *fibers*, or of its *cofiber*; these differ by 1. The traditional topological indexing uses the cofiber. We use the fiber, as does Lurie in HTT; but we choose to agree with the traditional indexing on types, while Lurie agrees with it on maps. Currently, the translation is therefore as follows: HoTT Traditional Lurie Map (n-1)-connected n-connected n-connective Type n-connected n-connected (n+1)-connective A handy benchmark: under our indexing, the map S1 → 1 is 0-connected but not 1-connected, while the map 1 → S1 is (–1)–connected but not 0-connected. One reason for our choice is that this way, the n-truncated and n-connected maps are the modal and modally-connected maps for the n-truncation modality. Many of the basic lemmas about connected maps are in fact true for any modality, and can be found in Modality.v. Thus, here we consider mainly properties that involve the interaction of connectedness at different truncation levels.

Truncatedness of the type of extensions

A key lemma on the interaction between connectedness and truncatedness: suppose one is trying to extend along an n-connected map, into a k-truncated family of types (k ≥ n). Then the space of possible extensions is (k–n–2)-truncated. (Mnemonic for the indexing: think of the base case, where k=n; then we know we can eliminate, so the space of extensions is contractible.) This lemma is most useful via corollaries like the wedge-inclusion, the wiggly wedge, and their n-ary generalizations.

Connectedness of path spaces

Connectivity of pointed types

The connectivity of a pointed type and (the inclusion of) its point are intimately connected. We can't make both of these Instances, as that would result in infinite loops.

Note that OO_cancelR_conn_map and OO_cancelL_conn_map (Proposition 2.31 of CORS) generalize the above statements to 2/3 of a 2-out-of-3 property for connected maps, for any reflective subuniverse and its subuniverse of separated types. If useful, we could specialize that more general form explicitly to truncations. To prove an n-truncated predicate on an (n+1)-connected, pointed type, it's enough to prove it for the basepoint.

This follows from conn_point_incl and conn_map_elim, but we give a direct proof.

Since A is n+1-connected, a0 = a is n-connected, which means that Tr n (a0 = a) has an element.

Decreasing connectedness

An n.+1-connected type is also n-connected. This obviously can't be an Instance!

A k-connected type is n-connected, when k ≥ n. We constrain k by making it of the form n +2+ m, which makes the induction go through smoothly.

A version with the order of summands swapped, which is sometimes handy, e.g. in the next two results.

It follows that an n.+1-connected type is also -1-connected.

And that an n.+2-connected type is 0-connected.

0-connectedness

To be 0-connected is the same as to be (-1)-connected and that any two points are merely equal. TODO: This should also be generalized to separated subuniverses (CORS Remark 2.35).

This follows immediately from isconnected_paths above.

The path component of a point x : X is connected.

Any two points in a path component are merely equal. This follows from merely_path_is0connected, but this proof doesn't need univalence.

The path component of a point x : X is equivalent to the image of the constant map Unit → X at x.

0-connected types are indecomposable

Connectivity of the wedge into the product.

A very useful form of the key lemma istrunc_extension_along_conn is the connectivity of the wedge into the product, for a pair of pointed spaces. In fact this can be formulated without mentioning the wedge per se (so, without requiring HIT’s), since the statement only needs to talk about maps out of the wedge. Once again, we believe that the type of the conclusion is an hprop (though we do not prove it) — essentially because it is wrapping up an elimination principle and its corresponding computation rule — and so we make the proof of this result opaque.

It is easier to apply the above result with its components separated.