Проталкивание пути по паре путей, исходящих из его конечных точек

Question

Предположим, у меня есть, используя библиотеку cubical-demo, следующие вещи в области действия:

i : I

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

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

Как мне тогда построить

q' : p0 i ≡ p1 i

Answer 1

Я нашел другое решение для этого, которое является более явным, поскольку он склеивает префикс p0 (перевернутый), q0 и префикс 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 ∎

Answer 2

Еще один вопрос, который я придумал, - я думаю, что он ближе к духу исходной проблемы, чем обходить:

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))

Этот обладает очень хорошим свойством, которое вырождается до q в i = i0 определенно:

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

Answer 3

Одним из способов является сжатие одиночных пар с J, хотя могут быть и более простые доказательства.

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)))