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?

  • $\begingroup$ This question is more suitable to cstheory.stackexchange, HoTT is an active research field. $\endgroup$ Jun 2, 2017 at 19:14
  • $\begingroup$ cstheory is the wrong forum to ask this question, because the question is not research level. If anything, this could be migrated to math.stackexchange.com, but I think there's little point. $\endgroup$ Jun 2, 2017 at 20:42
  • $\begingroup$ @AndrejBauer Hmmm, I feel that this question is of a different calibre in comparison with the usual "help me prove that $\{ a^nb^n\ |\ n \in \mathbb{N}\}$ isn't regular" question that's the stable of the site. $\endgroup$ Jun 3, 2017 at 14:05
  • $\begingroup$ Surely you can't put "how do homotopies compose" on a research-level site? $\endgroup$ Jun 3, 2017 at 15:17

1 Answer 1


I recommend that in addition to watching videos you also read some material which actually explains homotopy type theory. Some good sources are:

  1. The HoTT book, which is "the bible".
  2. If you are philosophically minded you might like this primer by James Ladyman & Stuart Presnell.
  3. It might not hurt to read on some basic notions in topology, where it is explained how paths are composed (but that's not what happens in HoTT).

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.

I do not understand your setup for doing database queries, but let me just point out that there is HoTTSQL which is based on ideas from homotopy type theory.

  • $\begingroup$ Thanks! I had resolved to go slowly through the book until I understood each section, but I would have had to read further to clear up the misconception which I was stuck on in the introduction. Thanks for the link to HoTTSQL, it's an encouragement! It seems they model relations as functions from values to their cardinality in bags, and prove query rewrites. I think of relations as "slightly out of focus function types where you can't quite make out whether a parameter is an input or output until you get close" and I'm interested in compositions and decompositions thereof. $\endgroup$
    – Dennis
    Jun 2, 2017 at 22:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.