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→Y and g:X→Y as H:X×[0,1]→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×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:

- The entire space [0,1] of the inner I collapses down to a single point.
- The higher-order homotopy H″ should be treated of as having
twointerval 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

interactionbetween between f_1 and g_1 which potentially could representholesin 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 arenotpart of the intersection of the input spaces. The dimensions whicharein 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?

**Answer**

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

- The HoTT book, which is “the bible”.
- If you are philosophically minded you might like this primer by James Ladyman & Stuart Presnell.
- 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.

**Attribution***Source : Link , Question Author : Dennis , Answer Author : Andrej Bauer*