Is "path of path compositions" available?

[anqurvanillapy]

According to the introduction section in HoTT book:

The torus T² is generated by a single point, two paths p and q from that point to itself, and a two-dimensional path from p · q to q · p.

• Could the path of path compositions definable in RedTT?
• Is this kind of operations lower-level to the existing version of torus.red? In fact, I mean... is this necessary?

[jonsterling]

@anqurvanillapy You can certainly define a path between composed paths, but I think that maybe what you are asking is whether you can use this in a path constructor of a HIT. It is supported in the mathematical schema that underlies redtt's implementation, but I do not remember if we actually have implemented support for it yet.

[ecavallo]

It is indeed not yet implemented.

In cubical type theory, the definition of the torus in torus.red is more natural and direct than the one in the HoTT book. The two-dimensional constructor has the form of a square:

  q
p □ p
  q

which we can write directly as a cubical constructor with two dimension variables. In the HoTT book, HIT constructors must have iterated path types, so they can't put in a "square constructor" like this directly. Instead, they use that the type of such squares is equivalent to the type of equalities p · q = q · p, which is a legitimate type for a constructor.