沿着从其端点开始的一对路径推送路径

一种方法是用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)))

我想到的另一个问题是,我认为更接近于原始问题的精神,而不是走来走去:

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

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 ∎