Pushing a path along a pair of paths originating from its endpoints

Question

Suppose I have, using the cubical-demo library, the following things in scope:

i : I

p0 : x ≡ y
p1 : x' ≡ y' 

q0 : x ≡ x'    
q1 : y ≡ y'

How do I then construct

q' : p0 i ≡ p1 i

?

score 1 · Answer 1 · answered Nov 05 '18 at 13:29

1

One way is by contracting singleton pairs with J, there might be simpler proofs though.

open import Cubical.PathPrelude

q' : ∀ {A : Set} (i : I) (x : A)
     x' (q0 : x ≡ x')
     y  (p0 : x ≡ y)
     y' (p1 : x' ≡ y')
     (q1 : y ≡ y') →  p0 i ≡ p1 i 
q' i x = pathJ _ (pathJ _ (pathJ _ (\ q1 → q1)))

answered Nov 05 '18 at 13:29

Saizan

1,391
8
4

Any idea why I can't eta-expand `q'`? – Cactus Nov 05 '18 at 14:59
I realize now that `q1` is completely redundant, since it is just the transport of `q0` along `p0`/`p1`. – Cactus Nov 06 '18 at 00:56
I've posted a follow-up question about this function's behaviour at `i0`: https://stackoverflow.com/q/53166153/477476 – Cactus Nov 06 '18 at 05:22
1

It should be possible to eta-expand `q'` as long as you first fill in the `_`. I would replace them by ? reload and then use C-c C-s to have agda fill them in, then eta-expand. – Saizan Nov 06 '18 at 16:14
1

Oh, and the reason is that if the extra variables are not in scope the unification problems coming from typechecking have a unique solution. – Saizan Nov 06 '18 at 16:16
I've switched over to using [this](https://stackoverflow.com/a/53199767/477476) because that one seems to be more.. space-filling? – Cactus Nov 08 '18 at 02:32

Cactus · Answer 2 · 2018-11-08T00:09:10.097

I've found another solution to this, which is more explicit that it is gluing together a prefix of p0 (flipped), q0, and a prefix of p1:

open import Cubical.PathPrelude

module _ {ℓ} {A : Set ℓ} where
  midPath : ∀ {a b c d : A} (p₀ : a ≡ b) (p₁ : c ≡ d) → (a ≡ c) → ∀ i → p₀ i ≡ p₁ i
  midPath {a = a} {c = c} p₀ p₁ q i = begin
    p₀ i ≡⟨ transp (λ j → p₀ (i ∧ j) ≡ a) refl ⟩
    a    ≡⟨ q ⟩
    c    ≡⟨ transp (λ j → c ≡ p₁ (i ∧ j)) refl ⟩
    p₁ i ∎

score 1 · Accepted Answer · answered Nov 08 '18 at 00:08

Another one I've come up with is I think closer to the spirit of the original problem instead of going around:

slidingLid : ∀ (p₀ : a ≡ b) (p₁ : c ≡ d) (q : a ≡ c) → ∀ i → p₀ i ≡ p₁ i
slidingLid p₀ p₁ q i j = comp (λ _ → A)
  (λ{ k (i = i0) → q j
    ; k (j = i0) → p₀ (i ∧ k)
    ; k (j = i1) → p₁ (i ∧ k)
    })
  (inc (q j))

This one has the very nice property that it degenerates to q at i = i0 definitionally:

slidingLid₀ : ∀ p₀ p₁ q → slidingLid p₀ p₁ q i0 ≡ q
slidingLid₀ p₀ p₁ q = refl

Pushing a path along a pair of paths originating from its endpoints

3 Answers3

Linked