strict computation property for first-path-Sigma

[TashiWalde]

Let A : U and C : A -> U and s t : total-type A C. I observed that applying first-path-Sigma to a term of the form (eq-pair p q) : s = t (where p : first s = first t and q : s' = t is a path from the transported term) does not strictly compute to p.

See issue #61, where first-path-\Sigma-eq-pair cannot simply be implemented as refl.

It might be a bit unreasonable to ask such a strict computation rule for every pair (p,q), but I was expecting this to hold at least when p is refl. To my surprise, even this computation rule fails with the current implementations.

#def first-path-Σ-eq-pair-refl
-- does not type-check!
  ( A : U)
  ( B : A → U)
  ( a : A)
  ( b b' :  B a)
  ( q : b = b')
  : first-path-Σ A B (a,b) (a,b') (eq-pair A B (a,b) (a,b') (refl, q)) = refl
  :=
    refl

Is it possible to re-implement first-path-\Sigma satisfying at least strict computation for terms of the form (eq-pair refl q)?

[TashiWalde]

After some conversations with Emily and Egbert, I now think that this is probably impossible. I am thus closing the issue.