# How do the unit intervals compose when generating higher order homotopies?

I’m trying to apply homotopy type theory as a theoretical foundation for describing how database query plans solve relational algebra queries. I’m modeling the problem as, given a set of input function types and constraints on composing them, and a goal function type, find a composition of the input functions which has an equivalent type to the goal function type. Because interactions between datasets of subqueries can be nonlocal and also circularly dependent, we cannot assume that the codomain type of any function is defintionally equal to the domain type of any other function. (That is, the domains and codomains are dependent types dependent on each other.) Instead, what can be done is that the function types can be projected into other spaces which can be made equal by the univalence axiom, as long as we also properly keep track of what structure was projected away and “put it back” when computing the full solution.

In order to do this, I need to understand the rules of when a homotopy is applicable between two functions, and what is happening in the derivation rules when higher order homotopies are composed.

I’ve watched videos of talks about homotopy type theory which mention that since a path between paths is also a path, we can extend homotopies into higher order homotopies. However I’m confused about how the details of this process work out algebraically. I’m also interested in understanding the minimum requirements two paths must have in common in order to participate in a higher-order path.

The HoTT book defines a homotopy introduces a classical homotopy (see Andrej Bauer’s answer) as a continuous map H between a pair of continuous maps $f:X \to Y$ and $g:X \to Y$ as $H:X \times [0,1] \to Y$. Let $I$ refer to the unit interval $[0,1]$ component of $H$ in the above definition.

My first difficulty is that $f$ and $g$ have a different “interface” (in programming terms) than $H$. In the definition, $f$ and $g$ were “functions of one argument” and $H$ was a “function of two arguments”. If I then compose two paths $H$ and $H'$, what happens to their unit interval “argument” $I$ when I substitute $H$ and $H'$ for $f$ and $g$ in the original definition?

I do understand that a product of two types $X \times I$ can in turn be viewed as the single “opaque” type $X'$ from the level of the higher order path. However I am also concerned with how terms of the types are constructed and how the $I$ hidden in the lower-order homotopy relates to the $I'$ of the higher-order homotopy.

I can think of two scenarios:

1. The entire space $[0,1]$ of the inner $I$ collapses down to a single point.
2. The higher-order homotopy $H''$ should be treated of as having two interval arguments, $I_1$ and $I_2$, where $\\H''(x,0,0)=f_1(x),\\H''(x,1,0)=g_1(x), \\H''(x,0,1)=f_2(x),\\H''(x,1,1)=g_2(x)$

Here’s what I think based on intuition:

Given functions $f_{1}:A \to B$ and $g_{1}:C \to D$, if $A \cap C = \emptyset$ and $B \cap D = \emptyset$, then both may be represented as loops attached to a single point, $f_{B^A \rightsquigarrow \circlearrowright}:* \to *$ and $g_{D^C \rightsquigarrow \circlearrowright}:* \to *$, where the subscripts by the function names represent encoding (somehow, somewhere) what was done to the function in collapsing it. Then, the homotopy is the trivial mapping of that point to itself. The “program” formed by the composition of all this might be summarized as $f_1 \curvearrowright * \curvearrowleft g_1$ which represents shrinking all of $f_1$ down to a singularity and then inflating it back up to all of $g1$ or vice versa. (Sounds like a description of The Big Bang.) The resulting program would compute a Cartesian product. The idea there is that if $f_1$ and $g_1$ are really unrelated to each other, but by fiat you declared that a homotopy exists between them, that’s the same as doing a CROSS JOIN between database tables with no common columns.

On the other hand if it is not the case that $A \cap C = \emptyset$ and $B \cap D = \emptyset$, then we cannot collapse them down to a singularity because the nonempty intersections of the input (co)domains represent an interaction between between $f_1$ and $g_1$ which potentially could represent holes in the space of the homotopy. That is, any pre-existing holes in the two input spaces could interact to produce a more complex hole in the homotopy. In the previous case we were able to ignore preexisting holes in the input spaces because the funny subscripting operation “preserved structure”. But each subscript only related a particular space “up to” the singularity; if it could relate two different spaces “within” the singularity (or across it) then it would amount to begging the question (it would amount to assuming the solution to the problem we are purporting to solve). Therefore, we can only collapse dimensions which are not part of the intersection of the input spaces. The dimensions which are in the intersection form the space where the homotopy is “interesting” and the dimensions which are not form the part which was projected-away-but-recorded. This corresponds to an INNER EQUIJOIN.

How that relates to the unit interval argument $I$ is that if the (co)domains of $f$ and $g$ have no natural intersection, then we can take scenario (1) when constructing higher-order homotopies; $I$ collapses to a single point and we can simplify $X \times I \Rightarrow X \times 1 \Rightarrow X$. However if $f$ and $g$ have a nonempty intersection of the spaces they operate in, we have to go with scenario (2) and instead of unit intervals go to unit squares, unit cubes, etc.

Do I have that right?

I see you refer to the HoTT book in your question, but you falsely claim that the HoTT book defined a homotopy as a map $H : X \times [0,1] \to Y$. This is not what the HoTT book does, it’s the classical definition of homotopy in topology. The HoTT definition is that a homotopy between $f, g : X \to Y$ is an element of $\prod_{x : X} f(x) = g(x)$. Paths in homotopy type theory are not continuous maps from the interval, that again is classical topology.