<p>Disclaimer: I've never actually implemented any variation of cubical type theories and I am not an expert in cubical type theory. I write this answer according to my own intuition. I welcome corrections and complementaries.</p>
<blockquote>
<p>How does this actually compute a path from a to d?</p>
</blockquote>
<p>The <code>comp</code> operator creates a term that has the following properties (in your case, not the general case):</p>
<ul>
<li>Reduces to <code>a</code> when <code>i</code> equals <code>0</code></li>
<li>Reduces to <code>d</code> when <code>i</code> equals <code>1</code></li>
</ul>
<p>That's how the path was created -- you can run the term (that has the above reduction rules) against the typing rule of path lambdas (the <code>&lt;i&gt; a</code> thing) in your head.</p>
<p>There is <em>no</em> primitive path composition in cubical type theory. It exists only in the model (or you can say the 'mathematical intuition'). The path composition <code>∘</code> we're talking about in cubical type theory is defined via <code>comp</code>, and <code>comp</code> <em>is</em> a primitive operator.
I personally think of <code>comp</code> as the eliminator of the 'system' structure -- I'm not sure if it's the right way to think about it, but it worked for me.</p>
<p>Here's a more formal and general description: <code>comp</code> takes an open cube of any dimension (without a <em>lid</em>, and is described using the 'system' structure and an extra term representing the bottom). This cube has to satisfy several properties, such as agreement on intersections (like the side faces have to share the same edge connecting them). Then, by providing this open shape, <code>comp</code> becomes a term that reduces like this: take the face as the system describes and return the proper side of the face.</p>
<p>In your case, the faces are <code>b2a</code> and <code>c2d</code> and the bottom face is <code>b2c</code>, and they agree obviously. That's why this application to <code>comp</code> type-checks. Then, the term satisfying the computational rules described above was created, and, as the body of a path, it satisfies the type <code>Path A a d</code>. That's just how it worked.</p>
<p>Edit: here's some extra mathematical intuition. Think about the world of types and terms in the HoTT-ish sense, where there are spaces, points, lines, squares, cubes, etc., and these shapes can change geometrically but not topologically. There is a fact about this world: if given a cube where all of its sides and its bottom are connected, then this cube is, in fact, filled. Then we make this theorem a primitive operator called filling, and by filling a shape we can take its lid. Maybe the cubical folks think the 'take lid' operator is more primitive than 'filling', so they built the 'take lid' operator into the type theory, but IIRC these two operations can encode each other. There's nothing to do with concatenating anything, they are <em>just</em> connected. Connected things are always connected (so I don't think it's a good idea to say that there exists an operator <code>∘</code> because it does nothing. In fact, <code>comp</code> does nothing too, but it is a good theorem to rely on (at least better than <code>∘</code>)), and composition happens to be such a good operator to implement in the type theory. If you want to read more, you may wanna search about 'kan condition'.</p>

CC BY-SA 4.0
2021-06-14T02:34:22.377Z
2021-06-14T02:45:05.217Z
2021-06-14T02:45:05.217Z
ice1000
<p>Consider the definition:</p>
<pre><code>--  a             d
--  ^             ^
--  |             |
--  |             |
--  b------------&gt;c
comp3Paths (A : U)
  (a b c d: A)
  (b2a : Path A b a)
  (b2c: Path A b c)
  (c2d: Path A c d) : Path A a d =
 &lt;i&gt; comp (&lt;_&gt; A) (b2c @ i)
   [ (i = 0) -&gt; b2a , (i = 1) -&gt; c2d ]
</code></pre>
<p>How does this actually compute a path from <code>a</code> to <code>d</code>? As best as I can tell, it will have to flip <code>b2a</code>, compose this with <code>b2c</code>, and finally compose this with <code>c2d</code>? In particular, if cubicaltt was equipped with a &quot;path composition operator&quot; <code>∘</code>, could I have written the above as <code>c2d ∘ b2c ∘(&lt;i&gt; b2a @ -i)</code>?</p>
<p>If that's wrong, then <em>what is the correct way</em> to think about what <code>comp</code> does in cubicalTT?</p>

<type-theory><dependent-type>
How to think about `comp` in cubical type theory
Siddharth Bhat
# How to think about `comp` in cubical type theory

(Asked by: username_0 on 2021-06-12)

Consider the definition:
--  a             d
--  ^             ^
--  |             |
--  |             |
--  b------------>c
comp3Paths (A : U)
  (a b c d: A)
  (b2a : Path A b a)
  (b2c: Path A b c)
  (c2d: Path A c d) : Path A a d =
  comp (<_> A) (b2c @ i)
   [ (i = 0) -> b2a , (i = 1) -> c2d ]

How does this actually compute a path from a to d? As best as I can tell, it will have to flip b2a, compose this with b2c, and finally compose this with c2d? In particular, if cubicaltt was equipped with a "path composition operator" ∘, could I have written the above as c2d ∘ b2c ∘( b2a @ -i)?
If that's wrong, then what is the correct way to think about what comp does in cubicalTT?

**Tags:** type-theory, dependent-type


---

## 1 answers

### Answer by username_1 on 2021-06-14. Score: 4 | Accepted answer

Disclaimer: I've never actually implemented any variation of cubical type theories and I am not an expert in cubical type theory. I write this answer according to my own intuition. I welcome corrections and complementaries.

> How does this actually compute a path from a to d?

The `comp` operator creates a term that has the following properties (in your case, not the general case):

* Reduces to `a` when `i` equals `0`
* Reduces to `d` when `i` equals `1`

That's how the path was created -- you can run the term (that has the above reduction rules) against the typing rule of path lambdas (the  `a` thing) in your head.

There is *no* primitive path composition in cubical type theory. It exists only in the model (or you can say the 'mathematical intuition'). The path composition `∘` we're talking about in cubical type theory is defined via `comp`, and `comp` *is* a primitive operator.
I personally think of `comp` as the eliminator of the 'system' structure -- I'm not sure if it's the right way to think about it, but it worked for me.

Here's a more formal and general description: `comp` takes an open cube of any dimension (without a *lid*, and is described using the 'system' structure and an extra term representing the bottom). This cube has to satisfy several properties, such as agreement on intersections (like the side faces have to share the same edge connecting them). Then, by providing this open shape, `comp` becomes a term that reduces like this: take the face as the system describes and return the proper side of the face.

In your case, the faces are `b2a` and `c2d` and the bottom face is `b2c`, and they agree obviously. That's why this application to `comp` type-checks. Then, the term satisfying the computational rules described above was created, and, as the body of a path, it satisfies the type `Path A a d`. That's just how it worked.

Edit: here's some extra mathematical intuition. Think about the world of types and terms in the HoTT-ish sense, where there are spaces, points, lines, squares, cubes, etc., and these shapes can change geometrically but not topologically. There is a fact about this world: if given a cube where all of its sides and its bottom are connected, then this cube is, in fact, filled. Then we make this theorem a primitive operator called filling, and by filling a shape we can take its lid. Maybe the cubical folks think the 'take lid' operator is more primitive than 'filling', so they built the 'take lid' operator into the type theory, but IIRC these two operations can encode each other. There's nothing to do with concatenating anything, they are *just* connected. Connected things are always connected (so I don't think it's a good idea to say that there exists an operator `∘` because it does nothing. In fact, `comp` does nothing too, but it is a good theorem to rely on (at least better than `∘`)), and composition happens to be such a good operator to implement in the type theory. If you want to read more, you may wanna search about 'kan condition'.


---

