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 should 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

As a consequence, we have that ap f is n-connected when f is (n+1)-connected. See HFiber.v and Loops.v for similar results about truncated maps.

The converse to isconnected_paths holds when A is merely inhabited.

As a consequence, we get a converse to isconnmap_ap_isconnmap for (-1)-connected maps.

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. And the first one is not likely to be useful as an instance, as it requires guessing the point a0.

conn_point_incl can be made an instance, but at the time of writing, this doesn't cause any additional goals to be solved compared to making it an immediate hint, so we do the latter.

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.

Decreasing connectedness

An n.+1-connected type is also n-connected.

A version explicitly using the predecessor function.

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.

(-2)-connectedness

Every type is (-2)-connected.

Every map is (-2)-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 converse holds when A is merely inhabited.

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. The version involving the wedge itself is deduced in Homotopy/Wedge.v. 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.