agda - 如何使用身份消除(在 agda 中)来证明 Eckmann Hilton 在 HoTT 中的高维路径？

Question

我试图复制 HoTT 书(第 70 页)中的主要引理以证明 Eckmann Hilton 定理，仅使用 J(无模式匹配)。

它说:“但是，一般来说，定义水平组合的两种方式是一致的，α ⋆ β = α ⋆' β，正如我们可以通过对 α 和 β 以及剩下的两个 1 路径的归纳所看到的，将所有东西减少到反射性……”

我很困惑 E类型签名正确 - 应该 r'和 s有不同的路径？ d不会改进，所以我认为 E 有问题?我也不太明白我应该引入哪两条路径来完成证明，它们是 r'和 s ?如果是这样，我不明白这些最终的动机应该是什么？不会将“β”减少到 r消除对 1 路径进一步归纳的需要？

欢迎任何答案/解决方案，更重要的是，欢迎思考问题的方式。

_⋆≡⋆'_ : {A : Set} → {a b c : A} {p q : a ≡ b} {r' s : b ≡ c} (α : p ≡ q) (β : r' ≡ s) → (α ⋆ β) ≡ (α ⋆' β)
_⋆≡⋆'_ {A} {a} {b} {c} {p} {q} {r'} {s} α β = J D d p q α c r' s β
  where
    D : (p q : a ≡ b) → p ≡ q → Set
    D p q α = (c : A) (r' s : b ≡ c) (β : r' ≡ s) → (α ⋆ β) ≡ (α ⋆' β)
    E : (r' s : b ≡ c) → r' ≡ s → Set
    -- E p q β = (r ⋆ β) ≡ (r ⋆' β) 
    E r' s β = (_⋆_ {A} {b = b} {c} {r} {r} {r' = r'} {s = s} r β) ≡ (r ⋆' β)
    e : ((s : b ≡ c) → E s s r)
    e r = r --this is for testing purposes
    d : ((p : a ≡ b) → D p p r)
    d p c r' s β = {!J E e  !}

下面是到达这里的其余代码。

module q where

data _≡_ {A : Set} (a : A) : A → Set where
  r : a ≡ a

infix 20 _≡_

J : {A : Set}
    → (D : (x y : A) → (x ≡ y) →  Set)
    -- → (d : (a : A) → (D a a r ))
    → ((a : A) → (D a a r ))
    → (x y : A)
    → (p : x ≡ y)
    ------------------------------------
    → D x y p
J D d x .x r = d x

_∙_ : {A : Set} → {x y : A} → (p : x ≡ y) → {z : A} → (q : y ≡ z) → x ≡ z
_∙_ {A} {x} {y} p {z} q = J D d x y p z q
    where
    D : (x₁ y₁ : A) → x₁ ≡ y₁ → Set
    D x y p = (z : A) → (q : y ≡ z) → x ≡ z
    d : (z₁ : A) → D z₁ z₁ r
    d = λ v z q → q

infixl 40 _∙_

_⁻¹ : {A : Set} {x y : A} → x ≡ y → y ≡ x
-- _⁻¹ {A = A} {x} {y} p = J2 D d x y p
_⁻¹ {A} {x} {y} p = J D d x y p
  where
    D : (x y : A) → x ≡ y → Set
    D x y p = y ≡ x
    d : (a : A) → D a a r
    d a = r

infixr 50 _⁻¹

iₗ : {A : Set} {x y : A} (p : x ≡ y) → p ≡ r ∙ p
iₗ {A} {x} {y} p = J D d x y p 
  where
    D : (x y : A) → x ≡ y → Set
    D x y p = p ≡ r ∙ p
    d : (a : A) → D a a r
    d a = r

iᵣ : {A : Set} {x y : A} (p : x ≡ y) → p ≡ p ∙ r
iᵣ {A} {x} {y} p = J D d x y p 
  where
    D : (x y : A) → x ≡ y → Set
    D x y p = p ≡ p ∙ r
    d : (a : A) → D a a r
    d a = r

_∙ᵣ_ : {A : Set} → {b c : A} {a : A} {p q : a ≡ b} (α : p ≡ q) (r' : b ≡ c) → p ∙ r' ≡ q ∙ r'
_∙ᵣ_ {A} {b} {c} {a} {p} {q} α r' = J D d b c r' a α
  where
    D : (b c : A) → b ≡ c → Set
    D b c r' = (a : A) {p q : a ≡ b} (α : p ≡ q) → p ∙ r' ≡ q ∙ r'
    d : (a : A) → D a a r
    d a a' {p} {q} α = iᵣ p ⁻¹ ∙ α ∙ iᵣ q

-- iᵣ == ruₚ in the book

_∙ₗ_ : {A : Set} → {a b : A} (q : a ≡ b) {c : A} {r' s : b ≡ c} (β : r' ≡ s) → q ∙ r' ≡ q ∙ s
_∙ₗ_ {A} {a} {b} q {c} {r'} {s} β = J D d a b q c β
  where
    D : (a b : A) → a ≡ b → Set
    D a b q = (c : A) {r' s : b ≡ c} (β : r' ≡ s) → q ∙ r' ≡ q ∙ s
    d : (a : A) → D a a r
    d a a' {r'} {s} β = iₗ r' ⁻¹ ∙ β ∙ iₗ s

_⋆_ : {A : Set} → {a b c : A} {p q : a ≡ b} {r' s : b ≡ c} (α : p ≡ q) (β : r' ≡ s) → p ∙ r' ≡ q ∙ s
_⋆_ {A} {q = q} {r' = r'} α β = (α ∙ᵣ r') ∙ (q ∙ₗ β)

_⋆'_ : {A : Set} → {a b c : A} {p q : a ≡ b} {r' s : b ≡ c} (α : p ≡ q) (β : r' ≡ s) → p ∙ r' ≡ q ∙ s
_⋆'_ {A} {p = p} {s = s} α β =  (p ∙ₗ β) ∙ (α ∙ᵣ s)

Answer 1

在形式化中，基于路径归纳比双边版本方便得多。与基J ，我们基本上在目标类型中将路径的右端点重写为左路径，并将路径本身重写为自反性。与非基J ，我们将两个端点都重写为“新鲜”不透明变量，因此我们失去了左端点与作用域中其他结构的“连接”(因为左端点可能出现在作用域中的其他类型中)。

我还没有研究过你定义的确切问题，但我注意到基于 J这几乎是微不足道的。

data _≡_ {A : Set} (a : A) : A → Set where
  r : a ≡ a

infix 20 _≡_

J : {A : Set}{x : A}(P : ∀ y → x ≡ y → Set) → P x r → ∀ {y} p → P y p
J {A} {x} P pr r = pr

tr : {A : Set}(P : A → Set){x y : A} → x ≡ y → P x → P y
tr P p px = J (λ y _ → P y) px p

_∙_ : {A : Set} → {x y z : A} → (p : x ≡ y) → (q : y ≡ z) → x ≡ z
_∙_ {A} {x} {y} {z} p q = tr (x ≡_) q p

ap : {A B : Set}(f : A → B){x y : A} → x ≡ y → f x ≡ f y
ap f {x} {y} p = tr (λ y → f x ≡ f y) p r

infixl 40 _∙_

_∙ᵣ_ : {A : Set} → {b c : A} {a : A} {p q : a ≡ b} (α : p ≡ q) (r' : b ≡ c) → p ∙ r' ≡ q ∙ r'
α ∙ᵣ r' = ap (_∙ r') α

_∙ₗ_ : {A : Set} → {a b : A} (q : a ≡ b) {c : A} {r' s : b ≡ c} (β : r' ≡ s) → q ∙ r' ≡ q ∙ s
q ∙ₗ β = ap (q ∙_) β

_⋆_ : {A : Set} → {a b c : A} {p q : a ≡ b} {r' s : b ≡ c} (α : p ≡ q) (β : r' ≡ s) → p ∙ r' ≡ q ∙ s
_⋆_ {q = q} {r'} α β = (α ∙ᵣ r') ∙ (q ∙ₗ β)

_⋆'_ : {A : Set} → {a b c : A} {p q : a ≡ b} {r' s : b ≡ c} (α : p ≡ q) (β : r' ≡ s) → p ∙ r' ≡ q ∙ s
_⋆'_ {A} {p = p} {s = s} α β = (p ∙ₗ β) ∙ (α ∙ᵣ s)

_⋆≡⋆'_ : {A : Set} → {a b c : A} {p q : a ≡ b} {r' s : b ≡ c} (α : p ≡ q) (β : r' ≡ s) → (α ⋆ β) ≡ (α ⋆' β)
_⋆≡⋆'_ {A} {a} {b} {c} {p} {q} {r'} {s} α β =
  J (λ s β → (α ⋆ β) ≡ (α ⋆' β))
    (J (λ q α → (α ⋆ r) ≡ (α ⋆' r))
       r
       α)   -- induction on α
    β       -- induction on β