沿着源自其端点的一对路径推送路径答案

【问题标题】：Pushing a path along a pair of paths originating from its endpoints沿着源自其端点的一对路径推送路径
【发布时间】：2019-04-08 14:08:08
【问题描述】：

假设我有，使用cubical-demo 库，范围内有以下内容：

i : I

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

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

然后我该如何构造

q' : p0 i ≡ p1 i

【问题讨论】：

标签： agda cubical-type-theory

【解决方案1】：

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

【讨论】：

知道为什么我不能 eta-expand q'？
我现在意识到q1 是完全多余的，因为它只是q0 沿p0/p1 的传输。
我已在i0:stackoverflow.com/q/53166153/477476 发布了关于此函数行为的后续问题
只要先填写_，应该可以对q'进行eta-expand。我会用 ?重新加载，然后使用 C-c C-s 让 agda 填充它们，然后 eta-expand。
哦，原因是如果额外的变量不在范围内，那么来自类型检查的统一问题就有一个独特的解决方案。

【解决方案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))

这个有一个非常好的属性，它在i = i0定义上退化为q：

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

【讨论】：

【解决方案3】：

我找到了另一种解决方案，更明确地说，它将前缀 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 ∎

【讨论】：