h-types and holology

 

In Martin-Löf type theory,  or more specifically standard dependent type theory (DTT),  there is an extrinsic and an intrinsic concept of equality.  The intrinsic concept (written $\Gamma \vdash  t : A = A$) is what we shall mainly consider here. It can be given a topological (and higher-categorical) interpretation which is of some interest to mereology.  Here we only give a rough description of some of the intuitions involved.  Think of a collection of points in the plane.   Internal 'equality' between two (externally unequal) points $a$ and $b$, written $a=b$,  is seen as being witnessed by there being a continuous path from $a$ to $b$.  In this way reflexivity, symmetry and transitivity have natural interpretations (in fact we obtain a 'groupoid' or more correctly a 1-groupoid). Note that there can be more than one path between two points.  For a space $C$ consisting of two disjoint 'chunks' $A$ and $B$ there is no path from a point of $A$ to a point of $B$.  There are two extreme situations. One is the discrete case in which no two externally distinct points can be connected by a path - this is the classical concept of a set. The other extreme is a connected (or 1-connected) space in which we can find a single point $p$ such that $p$ can be connected to any other point in the space.  Thus the discrete space has the minimum of internal unity and the contractible space the maximum of internal unity. In general we can have a space with a certain number of connected components ('chunks'). If we view internal equality as an equivalence relation (and thus the space as a setoid)  then the number of components is the number of equivalence classes.

But being connected is only the maximum of unity at the lowest level. Given two points $a$ and $b$ there is a space of all paths from $a$ to $b$, $Path(a,b)$. Only now that 'points' are paths and the 'paths' are deformations between paths (homotopies). So given two paths $p1,p2$ in $Path(a,b)$ we have that $p_1=p_2$ is witnessed by there being a 'path' (i.e. deformation/homotopy) between $p_1$ and $p_2$. Now the same story is repeated at a higher octave. $Path(a,b)$ itself can possess the extremes of being discrete (set-like) or connected or anything between.  Indeed from elementary algebraic topology we get examples of spaces which are connected but which for two points $a$ and $b$ there are paths $p_1$ and $p_2$ in $Path(a,b)$ which cannot be deformed into each other. In the case where $Path(a,b)$ is connected for every $a$ and $b$ the space is called contractible but we now see why we could also call it, for example, 2-connected. We note that there are also closed paths or 'loops', elements in $P(a,a)$, and there is no a priori reason why these could not be discrete, not mutually deformable into another. Thus we could add to our characterization of classical 'set'.  If we think of a set as a collection of points or atoms, then these will not have interesting internal structure or symmetries and thus we could add to the definition of classical set the condition that $Path(a,a)$ be connected for every $a$: that is, all loops are internally the same.  We have seen the recurring motifs: connected and discrete. To this we can add external notions: there being no elements whatsoever in the space(type), there being exactly one according to external equality (singleton) and there being exactly two (for instance the type of classical Boolean values).

We can now continue this process considering deformations of deformations and so forth. If a deformation is a path between paths in $Path(a,b)$, i.e. an element in $Path(p_1,p_2)$ where $p_1,p_2: Path(a,b)$, then now we are given for $d_1,d_2 : Path(p_1,p_2)$ elements of $Path(d_1,d_2)$, deformations of deformations.  A structure like what we have here, in which we can keep iterating the path construction, is called an $\infty$-groupoid (this is only a rough description).  We get thus a notion of $n$-connectivity for each level $n$. What kind of $\infty$-groupoid will have the maximum of connectivity or unity, i.e. how can we define a contractible $\infty$-groupoid ? Clearly by requiring at each level that $Path(x,y)$ for any $x$ and $y$ be connected, that is, that we have $n$-connectivity at each level $n$.

A main idea of   the Univalent Foundations of Mathematics (also called Homotopy Type Theory) is that mathematics is better done over $\infty$-groupoids rather than over sets and that this not only gives place to a profound unity between logic, category theory and geometry but is also the most natural way of developing computer software for formalizing and checking proofs  -  something which can be very useful when the proofs are very long and complex. The concept of 'h-type'  in the title of this post is directly related to what we called $n$-connectivity in this post.

This might have applications to ontology and metaphysics, in particular to the philosophy of biology and mind.  There is a lowest level of inorganic matter which corresponds to classical sets, thus to  0-discreteness. Then living beings have an organic unity which corresponds to 1-connectedness. Each part of a living body is connected to every other one on the lowest level, but can have quite distinct mode of connection.  We can also think of this as there being the same life present in every part but functionally  specialized. Next we come to mind which is a higher-order organism in that the same mind is present in every part in an essentially similar way (perhaps related to metacognition or self-luminosity), thus we would postulate  both 1- and 2-connectedness for instance. The failure of 3-connectivity could reflect the presence of time or sensation for instance. We could also follow ancient metaphysics such as Plotinus and characterize the nous (seen as a unified space of all forms) as being $n$-connected for all $n$, thus a contractible $\infty$-groupoid, the ontological maximum of unity.