Fréchet Spaces and Presheave Morphisms.



A topological vector space V is both a topological space and a vector space such that the vector space operations are continuous. A topological vector space is locally convex if its topology admits a basis consisting of convex sets (a set A is convex if (1 – t) + ty ∈ A ∀ x, y ∈ A and t ∈ [0, 1].

We say that a locally convex topological vector space is a Fréchet space if its topology is induced by a translation-invariant metric d and the space is complete with respect to d, that is, all the Cauchy sequences are convergent.

A seminorm on a vector space V is a real-valued function p such that ∀ x, y ∈ V and scalars a we have:

(1) p(x + y) ≤ p(x) + p(y),

(2) p(ax) = |a|p(x),

(3) p(x) ≥ 0.

The difference between the norm and the seminorm comes from the last property: we do not ask that if x ≠ 0, then p(x) > 0, as we would do for a norm.

If {pi}{i∈N} is a countable family of seminorms on a topological vector space V, separating points, i.e. if x ≠ 0, there is an i with pi(x) ≠ 0, then ∃ a translation-invariant metric d inducing the topology, defined in terms of the {pi}:

d(x, y) = ∑i=1 1/2i pi(x – y)/(1 + pi(x – y))

The following characterizes Fréchet spaces, giving an effective method to construct them using seminorms.

A topological vector space V is a Fréchet space iff it satisfies the following three properties:

  • it is complete as a topological vector space;
  • it is a Hausdorff space;
  • its topology is induced by a countable family of seminorms {pi}{i∈N}, i.e., U ⊂ V is open iff for every u ∈ U ∃ K ≥ 0 and ε > 0 such that {v|pk(u – v) < ε ∀ k ≤ K} ⊂ U.

We say that a sequence (xn) in V converges to x in the Fréchet space topology defined by a family of seminorms iff it converges to x with respect to each of the given seminorms. In other words, xn → x, iff pi(xn – x) → 0 for each i.

Two families of seminorms defined on the locally convex vector space V are said to be equivalent if they induce the same topology on V.

To construct a Fréchet space, one typically starts with a locally convex topological vector space V and defines a countable family of seminorms pk on V inducing its topology and such that:

  1. if x ∈ V and pk(x) = 0 ∀ k ≥ 0, then x = 0 (separation property);
  2. if (xn) is a sequence in V which is Cauchy with respect to each seminorm, then ∃ x ∈ V such that (xn) converges to x with respect to each seminorm (completeness property).

The topology induced by these seminorms turns V into a Fréchet space; property (1) ensures that it is Hausdorff, while the property (2) guarantees that it is complete. A translation-invariant complete metric inducing the topology on V can then be defined as above.

The most important example of Fréchet space, is the vector space C(U), the space of smooth functions on the open set U ⊆ Rn or more generally the vector space C(M), where M is a differentiable manifold.

For each open set U ⊆ Rn (or U ⊂ M), for each K ⊂ U compact and for each multi-index I , we define

||ƒ||K,I := supx∈K |(∂|I|/∂xI (ƒ)) (x)|, ƒ ∈ C(U)

Each ||.||K,I defines a seminorm. The family of seminorms obtained by considering all of the multi-indices I and the (countable number of) compact subsets K covering U satisfies the properties (1) and (1) detailed above, hence makes C(U) into a Fréchet space. The sets of the form

|ƒ ∈ C(U)| ||ƒ – g||K,I < ε

with fixed g ∈ C(U), K ⊆ U compact, and multi-index I are open sets and together with their finite intersections form a basis for the topology.

All these constructions and results can be generalized to smooth manifolds. Let M be a smooth manifold and let U be an open subset of M. If K is a compact subset of U and D is a differential operator over U, then

pK,D(ƒ) := supx∈K|D(ƒ)|

is a seminorm. The family of all the seminorms  pK,D with K and D varying among all compact subsets and differential operators respectively is a separating family of seminorms endowing CM(U) with the structure of a complete locally convex vector space. Moreover there exists an equivalent countable family of seminorms, hence CM(U) is a Fréchet space. Let indeed {Vj} be a countable open cover of U by open coordinate subsets, and let, for each j, {Kj,i} be a countable family of compact subsets of Vj such that ∪i Kj,i = Vj. We have the countable family of seminorms

pK,I := supx∈K |(∂|I|/∂xI (ƒ)) (x)|, K ∈  {Kj,i}

inducing the topology. CM(U) is also an algebra: the product of two smooth functions being a smooth function.

A Fréchet space V is said to be a Fréchet algebra if its topology can be defined by a countable family of submultiplicative seminorms, i.e., a countable family {qi)i∈N of seminorms satisfying

qi(ƒg) ≤qi (ƒ) qi(g) ∀ i ∈ N

Let F be a sheaf of real vector spaces over a manifold M. F is a Fréchet sheaf if:

(1)  for each open set U ⊆ M, F(U) is a Fréchet space;

(2)  for each open set U ⊆ M and for each open cover {Ui} of U, the topology of F(U) is the initial topology with respect to the restriction maps F(U) → F(Ui), that is, the coarsest topology making the restriction morphisms continuous.

As a consequence, we have the restriction map F(U) → F(V) (V ⊆ U) as continuous. A morphism of sheaves ψ: F → F’ is said to be continuous if the map F(U) → F'(U) is open for each open subset U ⊆ M.


Complete Manifolds’ Pure Logical Necessity as the Totality of Possible Formations. Thought of the Day 124.0


In Logical Investigations, Husserl called his theory of complete manifolds the key to the only possible solution to how in the realm of numbers impossible, non-existent, meaningless concepts might be dealt with as real ones. In Ideas, he wrote that his chief purpose in developing his theory of manifolds had been to find a theoretical solution to the problem of imaginary quantities (Ideas Pertaining to a Pure Phenomenology and to a Phenomenological Philosophy).

Husserl saw how questions regarding imaginary numbers come up in mathematical contexts in which formalization yields constructions which arithmetically speaking are nonsense, but can be used in calculations. When formal reasoning is carried out mechanically as if these symbols have meaning, if the ordinary rules are observed, and the results do not contain any imaginary components, these symbols might be legitimately used. And this could be empirically verified (Philosophy of Arithmetic_ Psychological and Logical Investigations with Supplementary Texts).

In a letter to Carl Stumpf in the early 1890s, Husserl explained how, in trying to understand how operating with contradictory concepts could lead to correct theorems, he had found that for imaginary numbers like √2 and √-1, it was not a matter of the possibility or impossibility of concepts. Through the calculation itself and its rules, as defined for those fictive numbers, the impossible fell away, and a genuine equation remained. One could calculate again with the same signs, but referring to valid concepts, and the result was again correct. Even if one mistakenly imagined that what was contradictory existed, or held the most absurd theories about the content of the corresponding concepts of number, the calculation remained correct if it followed the rules. He concluded that this must be a result of the signs and their rules (Early Writings in the Philosophy of Logic and Mathematics). The fact that one can generalize, produce variations of formal arithmetic that lead outside the quantitative domain without essentially altering formal arithmetic’s theoretical nature and calculational methods brought Husserl to realize that there was more to the mathematical or formal sciences, or the mathematical method of calculation than could be captured in purely quantitative analyses.

Understanding the nature of theory forms, shows how reference to impossible objects can be justified. According to his theory of manifolds, one could operate freely within a manifold with imaginary concepts and be sure that what one deduced was correct when the axiomatic system completely and unequivocally determined the body of all the configurations possible in a domain by a purely analytical procedure. It was the completeness of the axiomatic system that gave one the right to operate in that free way. A domain was complete when each grammatically constructed proposition exclusively using the language of the domain was determined from the outset to be true or false in virtue of the axioms, i.e., necessarily followed from the axioms or did not. In that case, calculating with expressions without reference could never lead to contradictions. Complete manifolds have the

distinctive feature that a finite number of concepts and propositions – to be drawn as occasion requires from the essential nature of the domain under consideration –  determines completely and unambiguously on the lines of pure logical necessity the totality of all possible formations in the domain, so that in principle, therefore, nothing further remains open within it.

In such complete manifolds, he stressed, “the concepts true and formal implication of the axioms are equivalent (Ideas).

Husserl pointed out that there may be two valid discipline forms that stand in relation to one another in such a way that the axiom system of one may be a formal limitation of that of the other. It is then clear that everything deducible in the narrower axiom system is included in what is deducible in the expanded system, he explained. In the arithmetic of cardinal numbers, Husserl explained, there are no negative numbers, for the meaning of the axioms is so restrictive as to make subtracting 4 from 3 nonsense. Fractions are meaningless there. So are irrational numbers, √–1, and so on. Yet in practice, all the calculations of the arithmetic of cardinal numbers can be carried out as if the rules governing the operations are unrestrictedly valid and meaningful. One can disregard the limitations imposed in a narrower domain of deduction and act as if the axiom system were a more extended one. We cannot arbitrarily expand the concept of cardinal number, Husserl reasoned. But we can abandon it and define a new, pure formal concept of positive whole number with the formal system of definitions and operations valid for cardinal numbers. And, as set out in our definition, this formal concept of positive numbers can be expanded by new definitions while remaining free of contradiction. Fractions do not acquire any genuine meaning through our holding onto the concept of cardinal number and assuming that units are divisible, he theorized, but rather through our abandonment of the concept of cardinal number and our reliance on a new concept, that of divisible quantities. That leads to a system that partially coincides with that of cardinal numbers, but part of which is larger, meaning that it includes additional basic elements and axioms. And so in this way, with each new quantity, one also changes arithmetics. The different arithmetics do not have parts in common. They have totally different domains, but an analogous structure. They have forms of operation that are in part alike, but different concepts of operation.

For Husserl, formal constraints banning meaningless expressions, meaningless imaginary concepts, reference to non-existent and impossible objects restrict us in our theoretical, deductive work, but that resorting to the infinity of pure forms and transformations of forms frees us from such conditions and explains why having used imaginaries, what is meaningless, must lead, not to meaningless, but to true results.

How are Topological Equivalences of Structures Homeomorphic?


Given a first-order vocabulary 𝜏, 𝐿𝜔𝜔(𝜏) is the set of first-order sentences of type 𝜏. The elementary topology on the class 𝑆𝑡𝜏 of first-order structures type 𝜏 is obtained by taking the family of elementary classes

𝑀𝑜𝑑(𝜑) = {𝑀:𝑀 |= 𝜑}, 𝜑 ∈ 𝐿𝜔𝜔(𝜏)

as an open basis. Due to the presence of classical negation, this family is also a closed basis and thus the closed classes of 𝑆𝑡𝜏 are the first-order axiomatizable classes 𝑀𝑜𝑑(𝑇), 𝑇 ⊆ 𝐿𝜔𝜔(𝜏). Possible foundational problems due to the fact that the topology is a class of classes may be settled observing that it is indexed by a set, namely the set of theories of type 𝜏.

The main facts of model theory are reflected by the topological properties of these spaces. Thus, the downward Löwenheim-Skolem theorem for sentences amounts to topological density of the subclass of countable structures. Łoś theorem on ultraproducts grants that U-limits exist for any ultrafilter 𝑈, condition well known to be equivalent to topological compactness, and to model theoretic compactness in this case.

These spaces are not Hausdorff or T1, but having a clopen basis they are regular; that is, closed classes and exterior points may be separated by disjoint open classes. All properties or regular compact spaces are then available: normality, complete regularity, uniformizability, the Baire property, etc.

Many model theoretic properties are related to the continuity of natural operations between classes of structures, where operations are seen to be continuous and play an important role in abstract model theory.

A topological space is regular if closed sets and exterior points may be separated by open sets. It is normal if disjoint closed sets may be separated by disjoint open sets. Thus, normality does not imply regularity here. However, a regular compact space is normal. Actually, a regular Lindelöf space is already normal

Consider the following equivalence relation in a space 𝑋: 𝑥 ≡ 𝑦 ⇔ 𝑐𝑙{𝑥} = 𝑐𝑙{𝑦}

where 𝑐𝑙 denotes topological adherence. Clearly, 𝑥 ≡ 𝑦 iff 𝑥 and 𝑦 belong to the same closed (open) subsets (of a given basis). Let 𝑋/≡ be the quotient space and 𝜂 : 𝑋 → 𝑋/≡ the natural projection. Then 𝑋/≡ is T0 by construction but not necessarily Hausdorff. The following claims thus follow:

a) 𝜂 : 𝑋 → 𝑋/≡ induces an isomorphism between the respective lattices of Borel subsets of 𝑋 and 𝑋/≡. In particular, it is open and closed, preserves disjointedness, preserves and reflects compactness and normality.

b) The assignment 𝑋 → 𝑋/≡ is functorial, because ≡ is preserved by continuous functions and thus any continuous map 𝑓 : 𝑋 → 𝑌 induces a continuous assignment 𝑓/≡ : 𝑋/≡ → 𝑌/≡ which commutes with composition.

c) 𝑋 → 𝑋/≡ preserves products; that is, (𝛱𝑖𝑋𝑖)/≡ is canonically homeomorphic to 𝛱𝑖(𝑋𝑖/≡) with the product topology (monomorphisms are not preserved).

d) If 𝑋 is regular, the equivalence class of 𝑥 is 𝑐𝑙{𝑥} (this may fail in the non-regular case).

e) If 𝑋 is regular, 𝑋/≡ is Hausdorff : if 𝑥 ≢ 𝑦 then 𝑥 ∉ 𝑐𝑙{𝑦} by (d); thus there are disjoint open sets 𝑈, 𝑉 in 𝑋 such that 𝑥 ∈ 𝑈, 𝑐𝑙{𝑦} ⊆ 𝑉, and their images under 𝜂 provide an open separation of 𝜂𝑥 and 𝜂𝑦 in 𝑋/≡ by (a).

f) If 𝐾1 and 𝐾2 are disjoint compact subsets of a regular topological space 𝑋 that cannot be separated by open sets there exist 𝑥𝑖 ∈ 𝐾𝑖, 𝑖 = 1, 2, such that 𝑥1 ≡ 𝑥2. Indeed, 𝜂𝐾1 and 𝜂𝐾2 are compact in 𝑋/≡ by continuity and thus closed because 𝑋/≡ is Hausdorff by (e). They can not be disjoint; otherwise, they would be separated by open sets whose inverse images would separate 𝐾1 and 𝐾2. Pick 𝜂𝑥 = 𝜂𝑦 ∈ 𝜂𝐾1 ∩ 𝜂𝐾2 with 𝑥 ∈ 𝐾1, 𝑦 ∈ 𝐾2.

Clearly then, for the elementary topology on 𝑆𝑡𝜏, the relation ≡ coincides with elementary equivalence of structures and 𝑆𝑡𝜏/≡ is homeomorphic to the Stone space of complete theories.

Hypercoverings, or Fibrant Homotopies




Given that a Grothendieck topology is essentially about abstracting a notion of ‘covering’, it is not surprising that modified Čech methods can be applied. Artin and Mazur used Verdier’s idea of a hypercovering to get, for each Grothendieck topos, E, a pro-object in Ho(S) (i.e. an inverse system of simplicial sets), which they call the étale homotopy type of the topos E (which for them is ‘sheaves for the étale topology on a variety’). Applying homotopy group functors gives pro-groups πi(E) such that π1(E) is essentially the same as Grothendieck’s π1(E).

Grothendieck’s nice π1 has thus an interpretation as a limit of a Čech type, or shape theoretic, system of π1s of ‘hypercoverings’. Can shape theory be useful for studying ́etale homotopy type? Not without extra work, since the Artin-Mazur-Verdier approach leads one to look at inverse systems in proHo(S), i.e. inverse systems in a homotopy category not a homotopy category of inverse systems as in Strong Shape Theory.

One of the difficulties with this hypercovering approach is that ‘hypercovering’ is a difficult concept and to the ‘non-expert’ seem non-geometric and lacking in intuition. As the Grothendieck topos E ‘pretends to be’ the category of Sets, but with a strange logic, we can ‘do’ simplicial set theory in Simp(E) as long as we take care of the arguments we use. To see a bit of this in action we can note that the object [0] in Simp(E) will be the constant simplicial sheaf with value the ordinary [0], “constant” here taking on two meanings at the same time, (a) constant sheaf, i.e. not varying ‘over X’ if E is thought of as Sh(X), and (b) constant simplicial object, i.e. each Kn is the same and all face and degeneracy maps are identities. Thus [0] interpreted as an étale space is the identity map X → X as a space over X. Of course not all simplicial objects are constant and so Simp(E) can store a lot of information about the space (or site) X. One can look at the homotopy structure of Simp(E). Ken Brown showed it had a fibration category structure (i.e. more or less dual to the axioms) and if we look at those fibrant objects K in which the natural map

p : K → [0]

is a weak equivalence, we find that these K are exactly the hypercoverings. Global sections of p give a simplicial set, Γ(K) and varying K amongst the hypercoverings gives a pro-simplicial set (still in proHo(S) not in Hopro(S) unfortunately) which determines the Artin-Mazur pro-homotopy type of E.

This makes the link between shape theoretic methods and derived category theory more explicit. In the first, the ‘space’ is resolved using ‘coverings’ and these, in a sheaf theoretic setting, lead to simplicial objects in Sh(X) that are weakly equivalent to [0]; in the second, to evaluate the derived functor of some functor F : C → A, say, on an object C, one takes the ‘average’ of the values of F on objects weakly equivalent to G, i.e. one works with the functor

F′ : W(C) → A

(where W(C) has objects, α : C → C′, α a weak equivalence, and maps, the commuting ‘triangles’, and this has a ‘domain’ functor δ : W(C) → C, δ(α) = C′ and F′ is the composite Fδ). This is in many cases a pro-object in A – unfortunately standard derived functor theory interprets ‘commuting triangles’ in too weak a sense and thus corresponds to shape rather than strong shape theory – one thus, in some sense, arrives in proHo(A) instead of in Ho(proA).

Conjuncted: Indiscernibles – Philosophical Constructibility. Thought of the Day 48.1

Simulated Reality

Conjuncted here.

“Thought is nothing other than the desire to finish with the exorbitant excess of the state” (Being and Event). Since Cantor’s theorem implies that this excess cannot be removed or reduced to the situation itself, the only way left is to take control of it. A basic, paradigmatic strategy for achieving this goal is to subject the excess to the power of language. Its essence has been expressed by Leibniz in the form of the principle of indiscernibles: there cannot exist two things whose difference cannot be marked by a describable property. In this manner, language assumes the role of a “law of being”, postulating identity, where it cannot find a difference. Meanwhile – according to Badiou – the generic truth is indiscernible: there is no property expressible in the language of set theory that characterizes elements of the generic set. Truth is beyond the power of knowledge, only the subject can support a procedure of fidelity by deciding what belongs to a truth. This key thesis is established using purely formal means, so it should be regarded as one of the peak moments of the mathematical method employed by Badiou.

Badiou composes the indiscernible out of as many as three different mathematical notions. First of all, he decides that it corresponds to the concept of the inconstructible. Later, however, he writes that “a set δ is discernible (…) if there exists (…) an explicit formula λ(x) (…) such that ‘belong to δ’ and ‘have the property expressed by λ(x)’ coincide”. Finally, at the outset of the argument designed to demonstrate the indiscernibility of truth he brings in yet another definition: “let us suppose the contrary: the discernibility of G. A formula thus exists λ(x, a1,…, an) with parameters a1…, an belonging to M[G] such that for an inhabitant of M[G] it defines the multiple G”. In short, discernibility is understood as:

  1. constructibility
  2. definability by a formula F(y) with one free variable and no parameters. In this approach, a set a is definable if there exists a formula F(y) such that b is an element of a if F(b) holds.
  3. definability by a formula F (y, z1 . . . , zn) with parameters. This time, a set a is definable if there exists a formula F(y, z1,…, zn) and sets a1,…, an such that after substituting z1 = a1,…, zn = an, an element b belongs to a iff F(b, a1,…, an) holds.

Even though in “Being and Event” Badiou does not explain the reasons for this variation, it clearly follows from his other writings (Alain Badiou Conditions) that he is convinced that these notions are equivalent. It should be emphasized then that this is not true: a set may be discernible in one sense, but indiscernible in another. First of all, the last definition has been included probably by mistake because it is trivial. Every set in M[G] is discernible in this sense because for every set a the formula F(y, x) defined as y belongs to x defines a after substituting x = a. Accepting this version of indiscernibility would lead to the conclusion that truth is always discernible, while Badiou claims that it is not so.

Is it not possible to choose the second option and identify discernibility with definability by a formula with no parameters? After all, this notion is most similar to the original idea of Leibniz intuitively, the formula F(y) expresses a property characterizing elements of the set defined by it. Unfortunately, this solution does not warrant indiscernibility of the generic set either. As a matter of fact, assuming that in ontology, that is, in set theory, discernibility corresponds to constructibility, Badiou is right that the generic set is necessarily indiscernible. However, constructibility is a highly technical notion, and its philosophical interpretation seems very problematic. Let us take a closer look at it.

The class of constructible sets – usually denoted by the letter L – forms a hierarchy indexed or numbered by ordinal numbers. The lowest level L0 is simply the empty set. Assuming that some level – let us denote it by Lα – has already been

constructed, the next level Lα+1 is constructed by choosing all subsets of L that can be defined by a formula (possibly with parameters) bounded to the lower level Lα.

Bounding a formula to Lα means that its parameters must belong to Lα and that its quantifiers are restricted to elements of Lα. For instance, the formula ‘there exists z such that z is in y’ simply says that y is not empty. After bounding it to Lα this formula takes the form ‘there exists z in Lα such that z is in y’, so it says that y is not empty, and some element from Lα witnesses it. Accordingly, the set defined by it consists of precisely those sets in Lα that contain an element from Lα.

After constructing an infinite sequence of levels, the level directly above them all is simply the set of all elements constructed so far. For example, the first infinite level Lω consists of all elements constructed on levels L0, L1, L2,….

As a result of applying this inductive definition, on each level of the hierarchy all the formulas are used, so that two distinct sets may be defined by the same formula. On the other hand, only bounded formulas take part in the construction. The definition of constructibility offers too little and too much at the same time. This technical notion resembles the Leibnizian discernibility only in so far as it refers to formulas. In set theory there are more notions of this type though.

To realize difficulties involved in attempts to philosophically interpret constructibility, one may consider a slight, purely technical, extension of it. Let us also accept sets that can be defined by a formula F (y, z1, . . . , zn) with constructible parameters, that is, parameters coming from L. Such a step does not lead further away from the common understanding of Leibniz’s principle than constructibility itself: if parameters coming from lower levels of the hierarchy are admissible when constructing a new set, why not admit others as well, especially since this condition has no philosophical justification?

Actually, one can accept parameters coming from an even more restricted class, e.g., the class of ordinal numbers. Then we will obtain the notion of definability from ordinal numbers. This minor modification of the concept of constructibility – a relaxation of the requirement that the procedure of construction has to be restricted to lower levels of the hierarchy – results in drastic consequences.

Homotopies. Thought of the Day 35.0


One of the major innovations of Homotopy Type Theory is the alternative interpretation of types and tokens it provides using ideas from homotopy theory. Homotopies can be thought of as continuous distortions between functions, or between the images of functions. Facts about homotopy theory are therefore only given ‘up to continuous distortions’, and only facts that are preserved by all such distortions are well-defined. Homotopy is usually presented by starting with topological spaces. Given two such spaces X and Y , we say that continuous maps f, g : X → Y are homotopic, written ‘f ∼ g’, just if there is a continuous map h : [0, 1] × X → Y with h(0, x) = f(x) and h(1, x) = g(x) ∀ x ∈ X. Such a map is a homotopy between f and g. For example, any two curves between the same pair of points in the Euclidean plane are homotopic to one another, because they can be continuously deformed into one another. However, in a space with a hole in it (such as an annulus) there can be paths between two points that are not homotopic, since a path going one way around the hole cannot be continuously deformed into a path going the other way around the hole.

Two spaces X and Y are homotopy equivalent if there are maps f : X → Y and f′ : Y → X such that f′◦ f ∼ idX and f ◦ f′ ∼ idY. This is an equivalence relation between topological spaces, so we can define the equivalence class [X] of all topological spaces homotopy equivalent to X, called the homotopy type of X. Homotopy theory does not distinguish between spaces that are homotopy equivalent, and thus homotopy types, rather than the topological spaces themselves, are the basic objects of study in homotopy theory.

In the homotopy interpretation of the basic language of HoTT we interpret types as homotopy types or ‘spaces’. It is then natural to interpret tokens of a type as ‘points’ in a space. The points of topological space have what we might call absolute identity, being elements of the underlying set. But a homotopy equivalence will in general map a given point x ∈ X to some other x′ ∈ X, and so when we work with homotopy types the absolute identity of the points is lost. Rather, we must say that a token belonging to a type is interpreted as a function from a one-point space into the space.

Given two points a and b in a space X, a path between them is a function γ : [0, 1] → X with γ(0) = a and γ(1) = b. However, given any such path, X can be smoothly distorted by retracting the path along its length toward a. Thus a space containing two distinct points and a path between them is homotopic to a space in which both points coincide (and the path is just a constant path at this point). We may therefore interpret a path between points as an identification of those points. Thus the identity type IdX(a,b) corresponds to the path space of paths from a to b. This also gives a straightforward justification for the principle of path induction: since any path is homotopic to a constant path (which corresponds to a trivial self-identification), any property (that respects homotopy) that holds of all trivial self-identifications must hold of all identifications.