Users of this file almost always want to be able to write Tr n for both a Modality and a ReflectiveSubuniverse, so they want the coercion modality_to_reflective_subuniverse:

Truncations of types

The definition

The definition of Trunc n, the n-truncation of a type. If Coq supported higher inductive types natively, we would construct this as something like: Inductive Trunc n (A : Type) : Type := | tr : A -> Trunc n A | istrunc_truncation : forall (f : Sphere n.+1 -> Trunc n A) (x : Sphere n.+1), f x = f North. However, while we are faking our higher-inductives anyway, we can take some shortcuts, rather than translating the definition above. Firstly, we directly posit a “constructor” giving truncatedness, rather than rephrasing it in terms of maps of spheres. Secondly, we omit the “computation rule” for this constructor, since it is implied by truncatedness of the result type (and, for essentially that reason, is never wanted in practice anyway).

Without explicit universe parameters, this instance is insufficiently polymorphic.

The non-dependent version of the eliminator.

Trunc is a modality

We don't usually declare modalities as coercions, but this particular one is convenient so that lemmas about (for instance) connected maps can be applied to truncation modalities without the user/reader needing to be (particularly) aware of the general notion of modality.

However, if the coercion is not printed, then we get things like Tr (-1) X being printed as (-1) X, which is terribly confusing. So we tell Coq to always print this coercion. This does mean that although the user can type things like IsConnected n X, it will always be displayed back as IsConnected (Tr n) X.

Functoriality

Since a modality lives on a single universe, by default if we simply define Trunc_functor to be O_functor then it would force X and Y to live in the same universe. But since we defined Trunc as a cumulative inductive, if we add universe annotations we can make Trunc_functor more universe-polymorphic than O_functor is. This is sometimes useful.

We have to teach Coq to translate back and forth between IsTrunc n and In (Tr n).

Having both of these as Instances would cause infinite loops.

Instead, we make the latter an immediate instance, but with high cost (i.e. low priority) so that it doesn't override the ordinary lemmas about truncation. Unfortunately, Hint Immediate doesn't allow specifying a cost, so we use Hint Extern instead. Hint Immediate istrunc_inO_tr : typeclass_instances. See https://github.com/coq/coq/issues/11697

This doesn't seem to be quite the same as Hint Immediate with a different cost either, though. Unfortunately, this isn't perfect; Coq still can't always find In n hypotheses in the context when it wants IsTrunc. You can always apply istrunc_inO_tr explicitly, but sometimes it also works to just pose it into the context. We do the same for IsTruncMap n and MapIn (Tr n).

A few special things about the (-1)-truncation

We define merely A to be an inhabitant of the universe hProp of hprops, rather than a type. We can always treat it as a type because there is a coercion, but this means that if we need an element of hProp then we don't need a separate name for it.

A stable type is logically equivalent to its (-1)-truncation. (It follows that this is true for decidable types as well.)

Surjections

Surjections are the (-1)-connected maps, but they can be characterized more simply since an inhabited hprop is automatically contractible.

A family of types is pointwise merely inhabited if and only if the corresponding fibration is surjective.

Surjections cancel on the right

Retractions are surjective.

Embeddings

Since embeddings are the (-1)-truncated maps, a map that is both a surjection and an embedding is an equivalence.

As a corollary, it follows that if i o f is an equivalence and i is an embedding, then f is an equivalence.

If X is a set and f : Y → Z is a surjection, then - o f is an embedding.

We next prove that paths : X → (X → Type) is an embedding. This was proved by Escardo as Lemma 15 in "Injective types in univalent mathematics", but we give an argument similar to the proof of Thm 2.25 of CORS. This will be an inverse to ap paths. We'll want to show that it is an embedding, so we'll construct it out of pieces that are clearly equivalences, except for one step, equiv_fun.

A Yoneda-like embedding for path types: paths : X → (X → Type) is an embedding.

Tactic to remove truncations in hypotheses if possible

search for truncated hypotheses

ensure that we didn't generate more than one subgoal, i.e. that the goal was appropriately truncated

See strip_reflections and strip_modalities for generalizations to other reflective subuniverses and modalities. We provide this version because it sometimes needs fewer universes (due to the cumulativity of Trunc). However, that same cumulativity sometimes causes free universe variables. For a hypothesis of type Trunc@{i} X, we can use Trunc_ind@{i j}, but sometimes Coq uses Trunc_ind@{k j} with i ≤ k and k otherwise free. In these cases, strip_reflections and/or strip_modalities may generate fewer universe variables.

Iterated truncations

Compare to O_leq_Tr and O_strong_leq_Tr in SeparatedTrunc.v.

If you are looking for a theorem about truncation, you may want to read the note "Finding Theorems" in "STYLE.md".