1
$\begingroup$

I'm still a bit confused about the transp operator in Agda:

transp : ∀ {ℓ} (A : I → Set ℓ) (r : I) (a : A i0) → A i1

Is found this paper and I wonder if there is a relation?

As far as I understand, the $\mathsf{comp}^i$ operator lets you transport an $n$-dimensional cube along $i$ and if you already know how some of the faces in the resulting $n+1$-dimensional cube should look like, you can specify them. So for example, $\mathsf{comp}^i A\ [(j=0)\mapsto q\ i]\ (p\ j)$ would only respect $q\ i$ but at $j=1$, the resulting face would not necessarily equal $r\ i$, is that correct?

They also define $\mathsf{transport}^i\ A\ u_0$ as $\mathsf{comp}^i\ A\ []\ u_0$ which I read as composition with no constraints and which looks a little bit like Agda's transport:

transport : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B
transport p a = transp (λ i → p i) i0 a

Could it be that transp is something like $\mathsf{comp}^i$ but where all constraints (like $q\ i$ and $r\ i$ in the example above) are constant (in $i$) and $r$ specifies at which faces the constant constraints are introduced?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
4
$\begingroup$

$\newcommand{\comp}{\mathsf{comp}}$ $\newcommand{\hcomp}{\mathsf{hcomp}}$ $\newcommand{\transp}{\mathsf{transp}}$ $\newcommand{\transport}{\mathsf{transport}}$

Compared to the paper you're reading, Agda divides $\comp$ into two distinct operations:

  1. $\hcomp$ is like $\comp$, but the $A$ parameter is not allowed to vary in $i$. This is "homogeneous composition."
  2. $\transp$ is the part of $\comp$ that allows $A$ to vary. It strictly deals with transporting along a path between types.

If you put these two components together, you can regain $\comp$ (by transporting things and doing the composition part in a homogeneous context), but it has been divided into orthogonal pieces that are easier to manage individually (although I don't have the expertise to explain exactly what about it is easier).

There is one important difference between $\transp$ and the $\transport$ defined in the paper you're reading (and in Agda). $\transp$ has the extra second argument $φ$, which specifies when it's allowed to reduce away. The side condition required is that when $φ$ holds, $A$ is constant in $i$. In that case, we have that $\transp\ A\ φ\ x = x$. So, $\transp$ doesn't strictly correspond to an empty $\comp$, but rather to something like:

$$\comp^i A\ [φ \mapsto u_0]\ u_0$$

which only makes sense when $A$ is the type of $u_0$ (which cannot depend on $i$) whenever $φ$ holds. Then $\transport$ is defined with $φ = 0$, which reduces to an empty $\comp$.

Improve this answer
$\endgroup$

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.