Paths vs Equivalences in cubical agda for specific computational behavior

Question

I'm working in Cubical agda and trying to build up some common utilities for later proofs. One of these is that for any type A it is the 'same' as the type Σ A (\_ -> Top) where Top is the type with one element. And the issue is how to best expose this 'sameness' from the utility library. I can expose it as an equivalence, a path or an isomorphism, and maybe multiple ones.

I originally exposed it as just a path: top-path : Path A (Σ A (\_ -> Top)) which is built up using glue types from an underlying top-equiv : A ≃ Σ A (\_ -> Top). But when trying to use this in later proofs I found out that transporting along this path did not compute as I expected. My expectation was that it composed with fst to the identity, but in practice I found that it sometimes left in transp and prim^unglue terms. This was not the case if I used a particular concrete type for A, or if I used a similar construction using the equivalence.

Example:

-- Working
compute-top-path-Bool : (a : Bool) -> fst (transport (top-path Bool) a) == a
compute-top-path-Bool a = refl

compute-top-equiv-Any : (a : Bool) -> fst (transport-equiv (top-equiv Bool) a) == a
compute-top-equiv-Any a = refl

-- Broken
compute-top-path-Any : (a : A) -> fst (transport (top-path A) a) == a
compute-top-path-Any a = refl

--
-- Checking test (/Users/endobson/tmp/agda/test.agda).
-- /Users/endobson/tmp/agda/test.agda:104,26-30
-- transp (λ i → A) i0 (fst (prim^unglue a)) != a of type A
-- when checking that the expression refl has type
-- fst (transport (top-path A) a) == a 
--

Self contained reproduction: https://gist.github.com/endobson/62605cfc15a92b9111391b459d03b548, and I'm using Agda version 2.6.1.3.

Thus my question is what is best solution for this problem? Am I somehow constructing my paths in a too complicated way and if I made them in a different way then the computational behavior would be better? Or is exposing the equivalence directly from my utility library expected? I find exposing the equivalence 'inelegant' as it seems that paths should be able to do this, but am not against doing so if they are known to be the better tool for this particular use case.

The Cubical library has pathToEquiv (ua e) ≡ e, can you use that? — Cactus
Such a path requires knowing where in the computation to use it which is not nearly as useful as just having it reduce as expected. — Eric Dobson

Saizan Saizan · Accepted Answer · 2021-04-08T06:41:28

In the agda/cubical library we do tend to export the equivalence (or the iso) along with the path, because of issues like the one you mention.

The reason for those extra transp calls is that transport for Glue has to work in the general case where they might actually be required.

fst (prim^unglue a) should reduce away if you ask for the normal form though.

Paths vs Equivalences in cubical agda for specific computational behavior

1 Answers